프로그램 합성: 기계 속의 λ
코드 생성에 적용된 인공지능에 관한 “주류” 논의의 대부분은 더 큰 언어 모델로 규모를 키우고 테스트 시점 연산(test-time compute)을 활용하여 코딩 벤치마크(SWE-bench, LiveCodeBench 등)에서 모델 성능을 끌어올린다는 발상이 압도적으로 지배하고 있습니다. 그리고 그러한 접근은 실제로 매우 흥미로운 결과를 몇 가지 만들어 냈습니다. 다만 그 열매에서 짜낼 즙이 얼마나 더 남아 있는지는 잘 모르겠습니다.
실제로 최전선의 모델들은 확률적 모방에 있어 놀라운 능력을 보여 주었으며, 학습 말뭉치에서 얻은 코드 템플릿을 창발적이고 유용한 방식으로 엮어 내고 합성하는 능력도 보여 주었습니다. 그러나 이 모델들은 여전히 토큰 시퀀스를 예측하는 방식으로 동작하며, 사람이 작성한 코드와 흔히 닮은, 구문적으로 그럴듯한 산출물을 생성합니다. 이 모델들이 추론과 비슷한 무언가라도 하고 있는지는 논란의 여지가 매우 큰 열린 질문이며, 저는 정말로 알지 못하기 때문에 이에 대해 내놓을 만한 흥미로운 의견이 없습니다. 현재의 시스템이 일부 경우에 제한적으로나마 유용하다는 것은 분명히 알고 있으며, 그 정도는 부인할 수 없는 사실로 보입니다.
그럼에도 저는 이 정교한 패턴 매칭을 진정한 프로그램 구성으로 오인하는 것은 심각한 범주 오류라고 주장하고 싶습니다. 통계적 사전 분포를 사용하여 코드를 텍스트 토큰의 시퀀스로 생성하는 것은, 프로그램 동역학의 공간에서 직접 탐색하여 프로그램을 생성하는 것과는 근본적으로 다른 작업입니다. 전자는 언어의 표면을 조작하는 행위이고, 후자는 논리적이고 의미론적인 발견의 행위입니다. 그리고 현재의 모델이 후자를 수행할 수 있는지는 제게 분명하지 않습니다.
하지만 잠시만 제 이야기에 장단을 맞춰 주시고, 어쩌면 AI 지원 개발의 미래가 오늘날의 모델을 다듬는 데 있는 것이 아니라 더 험난하고 사람들이 덜 다닌 프로그램 합성의 길을 추구하는 데 있을지도 모른다는 점을 생각해 보십시오. 이 길의 현대적 형태는 함수형 프로그래밍과 타입 이론의 발전에 가장 깊은 뿌리를 두고 있습니다. 프로그램 합성이 지향하는 바는 정확해 보이는 코드를 만들어 내는 것이 아니라, 바로 그 구성 방식 자체에 의해 명세에 대해 정확함이 증명된 프로그램을 구성하는 것입니다. 이는 활동의 중심을 자연어 프롬프트라는 지저분하고 모호한 영역에서 논리 명제라는 정밀하고 검증 가능한 영역으로 옮겨 놓습니다. 이러한 시도는 역사적으로 계산적으로 다루기 어려운 탐색 공간 때문에 발목이 잡혀 왔지만, 함수형 프로그래밍의 성숙, 특히 의존 타입의 등장은 필요한 이론적 토대의 상당 부분을 제공해 주었습니다.
의존 타입의 언어에서는 명세를 타입 시스템 안에 직접 인코딩할 수 있으며, 이를 통해 타입 검사는 일종의 부분적인 프로그램 검증이 됩니다. 바로 여기에서 **구멍 방식 개발(hole-style development)**이라는 개념이 이 새로운 패러다임의 핵심적인 사용자 인터페이스가 됩니다. 프로그래머는 속성을 타입으로 표현하면서 상위 수준의 구조를 설계하되, 구체적인 구현 세부 사항은 코드 안에 명시적인 “구멍“으로 남겨 둡니다. 이 구멍들은 올바른 형태를 갖춘 프로그램 안에 있는 일급(first-class)의, 타입이 지정된 틈이며, 합성기의 역할은 그 문맥의 엄격한 제약을 만족하는 항(term)을 찾는 것입니다.
두 벡터를 이어 붙이는 의존 타입의 의사 코드를 생각해 보십시오. 여기서 타입 시스템은 결과 벡터의 길이를 보장합니다. 프로그래머는 구현 로직을 ?로 표시되는 구멍으로 남겨 둔 채 초기 스케치를 작성할 수 있습니다.
data Vect : (Nat) -> (Type) -> Type where
Nil : Vect 0 a
Cons : a -> Vect n a -> Vect (S n) a
append : (n m : Nat) -> Vect n a -> Vect m a -> Vect (n + m) a
append 0 m Nil ys = ys
append (S n) m (Cons x xs) ys = Cons x ?
타입 검사기는 이 구멍이 Vect (n + m) a 타입의 항으로 채워져야 한다고 추론합니다. 이제 합성기의 작업은 엄청나게 단순해집니다. 합성기는 이어 붙이기라는 “개념“을 이해할 필요가 없습니다. 합성기는 사용 가능한 항(Vect n a 타입의 xs와 Vect m a 타입의 ys)을 요구되는 출력 타입으로 변환할 수 있는 연산의 조합만 탐색하면 됩니다. 유도된 탐색을 통해 합성기는 재귀 호출 append n m xs ys가 해당 타입을 만족한다는 것을 발견하게 되며, 이로써 타입 수준의 명세에 대해 정확함이 보장되는 방식으로 프로그램이 완성됩니다. Agda, Coq, Lean과 같은 시스템을 사용해 보신 적이 있다면 이 접근 방식의 위력을 아마 직접 보셨을 것입니다.
이러한 협업적 합성(비록 동적 타입이기는 하지만)의 비전은 DreamCoder와 같은 시스템에서 적어도 부분적으로 실현되었으며, 이는 기호적 추론과 신경망 학습을 잇는 데 있어 중요한 진전입니다. DreamCoder는 각성-수면 베이즈 학습 주기를 통해 작동합니다. “깨어 있는(wake)” 단계에서 DreamCoder는 귀납적 프로그램 합성 문제 코퍼스를 적극적으로 풀려고 시도하며, 주어진 입력-출력 예제를 만족하는 프로그램을 탐색합니다. “수면” 단계에서는 일종의 계산적 자기 성찰을 수행합니다. 즉, 찾아낸 해답을 분석하고, 공통 패턴을 리팩터링하고 압축하여 재사용 가능한 고수준 추상화로 이루어진 학습된 라이브러리로 만듭니다. 동시에 향후 탐색을 안내하는 신경망을 훈련시켜 합성 과정을 훨씬 더 효율적으로 만듭니다. 문제를 풀고 그 해답에서 학습하기를 번갈아 반복하는 이 과정을 통해 시스템은 스스로 전문성을 부트스트랩할 수 있으며, 점점 더 강력해지는 도메인 특화 언어와 그 구조에 맞게 조정된 탐색 정책을 구축합니다.
DreamCoder가 개척한 신경망 유도 접근법은 한층 더 흥미로운 연구 분야를 열어 줍니다. 바로 타입 주도 합성을 강화 학습 문제로 구성하는 것입니다. PPO와 같은 알고리즘으로 구동되며, 부분 프로그램을 귀납적으로 구성하고 프로그램의 구멍을 채우는 임무를 맡은 에이전트를 상상해 볼 수 있습니다. 환경은 불완전한 프로그램이고, 상태는 타입이 지정된 구멍과 그 지역 문맥이며, 사용 가능한 행동은 현재 라이브러리의 프리미티브들인데, 이 라이브러리 자체도 학습된 것일 수 있습니다. 타입이 올바른 항을 만들어 내는 모든 행동에 보상이 주어지며, 프로그램을 완성하면 상당한 최종 보상이 주어집니다. 에이전트의 정책 네트워크는 의미론적 사전 분포를 학습하여, 다음에 어떤 토큰이 올 가능성이 높은지가 아니라, 어떤 분기나 삽입이 주어진 지역 타입 시그니처와, 명세와의 일관성을 극대화하는 보상 함수를 향해 최적화한다는 전역 목표를 만족할 가능성이 가장 높은지를 예측하게 될 것입니다. 이는 표면 구문에 대한 패턴 매칭을 넘어 문제 도메인의 논리적 구조를 학습하는 방향으로 나아가는 것이며, DeepSynth, LambdaBeam 및 기타 신경망 유도 연역적 탐색 방법과 같은 시스템에 대한 연구에서 탐구된 방향입니다.
이런 종류의 추측은 재미있으며, 매우 흥미롭고 열려 있는 연구 문제입니다. 하지만 냉철한 현실 인식이 필요합니다. 프로그램 합성이라는 아이디어가 지적으로 우아함에도 불구하고, 그 미래는 결코 보장되어 있지 않습니다. 이러한 합성기를 개발하는 일은 개발자가 얻을 단기적 경제적 이익이 거의 없는 엄청난 엔지니어링 과제가 될 것이며, 아마도 어떤 전통적인 모델로도 자금을 조달하기 어려울 것입니다. 합성기가 효과적으로 작동하려면 각 도메인, 각 라이브러리, 각 API마다 형식 명세나 잘 선별된 문제 집합이 갖추어져야 합니다. 이는 NPM이나 PyPI 같은 기존 생태계의 혼란스럽고, 문서화되지 않았으며, 일관성 없이 뻗어 나간 코드를 받아들이고도 비록 취약하지만 유용한 사용 패턴을 추출해 낼 수 있는 통계적 모델과 극명한 대조를 이룹니다.
기존 프로그래밍 생태계의 네트워크 효과는 기술적 순수성이 일관되게 극복하지 못해 온 자연의 힘과 같습니다. 이것이 지난 40년간 Lisp와 함수형 프로그래밍 커뮤니티가 얻은 쓰라린 교훈이었습니다. 그들은 깨끗하고, 강력하며, 자기 일관적인 거품 세계를 구축했지만, 결국 C, Java, Python의 실용적인 분비와 축적에 밀려났습니다. 이 언어들의 가치는 내부적 일관성이 아니라 이를 둘러싼 라이브러리의 압도적인 규모와 경제적 유인에서 비롯되었습니다. 따라서 저는 가까운 미래에는 업계가 통계적 토큰 예측이라는 피상적으로 효과적인 접근법에 지배될 것이라는 점을 아마도 인정해야 할 것입니다. 인간과 기계 사이의 형식적 대화를 통해 합성되는, 증명 가능하게 올바른 프로그램이라는 꿈은 앞으로도 영감을 주는 비전으로 남겠지만, 코드 재사용이라는 거대한 중력과, 이전에 작성된 것을 그저 모방하는 데서 오는 최소 저항의 경로 앞에서 왜소해질지도 모릅니다. 그래도 우리는 여전히 DreamCoder의 미래를 꿈꿀 수 있습니다.