코드 생성에서 대형 언어 모델의 토큰 예측을 넘어, 의존 타입과 타입 주도 탐색을 바탕으로 한 프로그램 합성의 가능성과 한계를 살펴본다.
많은 "주류" 논의에서 코드 생성에 적용되는 인공지능 이야기는 더 큰 언어 모델을 스케일업하고 테스트-타임 컴퓨트를 사용해 코딩 벤치마크(SWE-bench, LiveCodeBench 등)에서의 모델 성능을 끌어올린다는 아이디어가 압도적으로 지배하고 있다. 그리고 그 과정에서 실제로 꽤 흥미로운 결과들이 나오기도 했다. 다만 그 과일에서 더 짜낼 수 있는 즙이 얼마나 남았는지는 잘 모르겠다.
실제로 최전선의 모델들은 확률적 모방에서 놀라운 능력과, 학습 코퍼스에서 코드 템플릿을 꿰매어(emergent하게) 유용한 방식으로 이어 붙이고 합성하는 능력을 보여주었다. 하지만 그것들은 여전히 토큰 시퀀스를 예측하는 방식으로 동작하며, 종종 사람이 쓴 코드처럼 보이는 문법적으로 그럴듯한 산출물을 생성한다. 그것들이 추론과 비슷한 무언가를 하고 있는지 여부는 매우 논쟁적이고, 내가 정말로 모르기 때문에 흥미로운 의견도 없는 열린 질문이다. 다만 현재 시스템들이 어떤 경우에는 제한적으로 유용하다는 점은 부정하기 어렵다고는 생각한다.
그럼에도 나는 이 정교한 패턴 매칭을 진정한 프로그램 구성으로 착각하는 것은 심각한 범주 오류라고 주장하고 싶다. 통계적 사전분포를 이용해 텍스트 토큰의 시퀀스로 _코드_를 생성하는 일은, 프로그램의 동역학 공간에서 직접 탐색하며 _프로그램_을 생성하는 일과 근본적으로 다른 과제다. 전자는 언어적 표면 조작의 행위이고, 후자는 논리적·의미론적 발견의 행위다. 그리고 현재의 모델들이 후자를 할 수 있는지는 내게 분명하지 않다.
하지만 잠시 내 말에 맞장구를 쳐 주며, 어쩌면 AI 보조 개발의 미래가 오늘날의 모델을 다듬는 데 있지 않고, 더 험하고 덜 밟힌 길인 프로그램 합성을 추구하는 데 있을지도 모른다고 생각해 보자. 이 길의 현대적 형태는 함수형 프로그래밍과 타입 이론의 진화에 가장 깊은 뿌리를 두고 있다. 프로그램 합성의 야망은 올바르게 보이는 코드를 만들어내는 것이 아니라, 구성 그 자체로 명세에 대해 올바름이 증명되는 프로그램을 구축하는 데 있다. 이는 활동의 중심을 지저분하고 모호한 자연어 프롬프트의 영역에서, 정밀하고 검증 가능한 논리 명제의 영역으로 옮긴다. 이 추구는 역사적으로 계산적으로 다루기 어려운 탐색 공간에 의해 발목 잡혀 왔지만, 함수형 프로그래밍의 성숙, 특히 의존 타입의 등장으로 많은 필수 이론적 비계가 제공되었다.
의존 타입 언어는 명세를 타입 시스템 안에 직접 인코딩할 수 있게 해 주며, 타입 검사(type-checking)를 부분 프로그램 검증의 한 형태로 변환한다. 여기서 구멍(hole) 스타일 개발이라는 개념이 이 새로운 패러다임의 핵심 사용자 인터페이스가 된다. 프로그래머는 상위 수준 구조를 설계하고, 속성을 타입으로 표현하되, 구체 구현의 세부는 코드 안에 명시적인 "구멍"으로 남긴다. 이것들은 잘 형성된 프로그램 안에서 일급(first-class)이며 타입이 붙은 개구부이고, 합성기의 역할은 그 문맥의 엄격한 제약을 만족하는 항을 찾는 것이다.
두 벡터를 이어 붙이는 의존 타입 의사코드를 생각해 보자. 여기서는 타입 시스템이 결과 벡터의 길이를 보장한다. 프로그래머는 초기 스케치를 쓰고, 구현 로직은 ?로 표기되는 구멍으로 남길 수 있다.
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-sleep 베이지안 학습 사이클을 통해 동작한다. "wake" 단계에서는 주어진 입력-출력 예시를 만족하는 프로그램을 찾기 위해 탐색하며 귀납적 프로그램 합성 문제들의 코퍼스를 적극적으로 풀려고 시도한다. "sleep" 단계에서는 일종의 계산적 자기성찰을 수행한다. 즉, 찾은 해법들을 분석하고, 공통 패턴을 리팩터링하고 압축하여 재사용 가능한 더 높은 수준의 추상화 라이브러리로 학습한다. 동시에, 미래의 탐색을 안내하기 위한 신경망을 학습하여 합성 과정을 훨씬 더 효율적으로 만든다. 문제를 번갈아 풀고 그 해법에서 학습하는 이 반복 과정은 시스템이 스스로의 전문성을 부트스트랩하도록 하며, 점점 더 강력한 도메인 특화 언어와 그 구조에 맞게 조율된 탐색 정책을 구축하게 한다.
DreamCoder가 개척한 신경망-가이드 접근은 더 매력적인 연구 전선을 연다. 즉, 타입 주도 합성을 강화학습 문제로 정식화하는 것이다. PPO 같은 알고리즘으로 구동되는 에이전트가 부분 프로그램을 귀납적으로 구성하고 프로그램의 구멍을 채우는 일을 맡는 모습을 상상할 수 있다. 환경은 미완성 프로그램이고, 상태는 타입이 붙은 구멍과 그 지역 문맥이며, 가능한 행동은 현재 라이브러리의 프리미티브들(그 자체가 학습되었을 수도 있다)이다. 타입-정합적인(type-correct) 항을 만들어내는 어떤 행동에도 보상이 주어지고, 프로그램을 완성하면 큰 최종 보상이 주어진다. 에이전트의 정책 네트워크는 의미론적 사전분포를 학습하게 되는데, 다음에 올 _토큰_이 무엇인지 예측하는 것이 아니라, 주어진 지역 타입 시그니처와 전역 목표(명세와의 정합성을 최대화하는 보상 함수를 최적화하는 것)를 만족할 가능성이 가장 큰 분기(branch) 또는 _삽입(insert)_이 무엇인지 예측한다. 이는 표면 문법의 패턴 매칭을 넘어 문제 도메인의 논리 구조를 학습하는 방향으로 나아가며, DeepSynth, LambdaBeam 같은 시스템과 다른 신경망-가이드 연역적 탐색 방법에 대한 연구에서 탐구되고 있다.
이런 종류의 즐거운 추측은 즐겁고, 매우 흥미로우며 열린 연구 문제다. 하지만 냉정한 현실 감각도 필요하다. 프로그램 합성이라는 아이디어의 지적 우아함에도 불구하고, 그 미래가 보장된 것은 전혀 아니다. 이런 합성기들을 개발하는 일은 엄청난 엔지니어링 과업이 될 것이고, 개발자에게 단기적으로 돌아오는 경제적 이익이 거의 없어서, 전통적인 어떤 모델로도 아마 자금 조달이 어려울 것이다. 각 도메인, 각 라이브러리, 각 API는 합성기가 효과적으로 동작하기 위해 형식 명세 또는 잘 큐레이션된 문제 집합을 갖추어야 한다. 이는 NPM이나 PyPI 같은 기존 생태계의 혼란스럽고 문서화되지 않았으며 일관성도 없는 광범위한 스프롤을 그대로 흡수하고도, 비록 취약하긴 하지만 유용한 사용 패턴을 뽑아낼 수 있는 통계적 모델과는 극명한 대조를 이룬다.
기존 프로그래밍 생태계의 네트워크 효과는 기술적 순수성이 꾸준히 극복하지 못해 온 자연의 힘이다. 이는 지난 40년 동안 Lisp와 함수형 프로그래밍 공동체가 배운 쓰라린 교훈이었다. 그들은 깨끗하고 강력하며 자기일관적인 버블 월드를 구축했지만, 결국 내부적 일관성이 아니라 주변 라이브러리의 압도적 규모와 경제적 유인에서 가치가 나오는 C, Java, Python의 실용적 분비와 축적에 의해 경쟁에서 밀려났다. 따라서 가까운 미래에 산업은 겉으로는 효과적인 통계적 토큰 예측 접근이 지배하게 되리라는 점을 나는 아마도 인정해야 할 것 같다. 인간과 기계 사이의 형식적 대화를 통해 [합성된, 증명 가능하게 올바른 프로그램]이라는 꿈은 계속해서 영감을 주는 비전으로 남겠지만, 코드 재사용의 거대한 중력과, 이미 써 있던 것을 흉내 내기만 하면 되는 최소 저항의 경로가 제공하는 끌림에 의해 왜소해질지도 모른다. 그래도 우리는 DreamCoder 같은 미래를 꿈꿀 수는 있다.