코드를 사람이 직접 짜는 대신, 원하는 동작을 명세로 주면 그것을 만족하는 프로그램을 기계가 찾아내도록 하는 기법을 프로그램 합성(program synthesis)이라 부른다. 이 아이디어의 가장 큰 걸림돌은 탐색 공간이다. 크기가 n인 프로그램의 개수는 n이 커질수록 기하급수적으로 늘어나기 때문에, 크기 1부터 시작해 모든 프로그램을 하나씩 만들어 명세를 만족하는지 확인하는 단순 열거 방식은 곧 한계에 부딪힌다. 그럼에도 이 분야가 실용 영역으로 넘어온 배경에는 탐색 공간을 영리하게 잘라내는 기법, SMT 솔버의 성능 향상, 그리고 문제 범위를 적절히 좁히는 전략이 있다. fitzgen의 2020년 글은 Gulwani 등의 논문 'Synthesis of Loop-Free Programs'에 기반해 이 흐름을 Rust 구현과 Z3 솔버로 풀어 설명한다.
왜 프로그램이 프로그램을 짜게 하나
사람이 손으로 짜기 까다로운 코드일수록 합성기의 가치가 크다. 글이 예시로 드는 문제는 '워드에서 가장 오른쪽 0 비트만 남기기'를 단 세 개의 비트 조작 명령으로 구현하는 것인데, not·add1·and 세 명령의 조합이 그 답이다. 사람이 이걸 떠올리려면 꽤 시간이 걸리지만, 합성기는 1초 안에 해를 찾고 최소 길이 해도 1분 남짓이면 찾아낸다. 또 다른 강력한 동기는 '많이 만들어야 할 때'다. 컴파일러의 피프홀 최적화기는 명령어 시퀀스를 보고 더 빠르거나 작은 등가 시퀀스로 바꾸는 패턴-치환 규칙의 묶음인데, LLVM의 InstCombine은 이런 쌍이 1,000개가 넘는다. 이 미니 프로그램들을 손으로 다 짜는 대신 원본 시퀀스를 명세로 넣고 합성기에 최적 시퀀스를 찾게 하면 피프홀 최적화기를 자동으로 구성할 수 있다. Bansal 등이 2006년 논문에서 제안한 방향인데, 글쓴이는 John Regehr의 지적을 인용해 이 발상 자체는 1980년 Davidson 등의 연구까지 거슬러 올라가는 오래된 것임을 덧붙인다.
두 가지 제약: 루프 없음과 컴포넌트 기반
문제를 다루기 쉽게 만들기 위해 두 가지로 범위를 좁힌다. 첫째는 루프가 없는 프로그램만 합성한다는 것이다. 피프홀 최적화기처럼 루프 경계를 넘나드는 시퀀스를 고려하지 않는 용도에서는 이 제약이 크게 불편하지 않다. 둘째는 컴포넌트 기반이다. 언어의 모든 표현식을 자유롭게 조합하는 대신, 주어진 컴포넌트 라이브러리의 각 컴포넌트를 정확히 한 번씩만 사용해 프로그램을 구성한다. 합성기는 컴포넌트들의 입력과 출력을 다시 연결하고 순서를 바꿔가며 명세를 만족하는 배치를 찾는다. 각 컴포넌트의 입력은 앞서 정의된 임시 변수이거나 원래의 입력값이어야 한다.
이 방식은 선택의 부담을 사용자에게 넘긴다. 어떤 컴포넌트를 라이브러리에 넣을지 매번 정해야 하기 때문이다. 덧셈을 두 번 하는 프로그램을 원하면 add 컴포넌트를 두 개 넣어야 한다. 컴포넌트가 너무 적으면 해를 찾지 못하고, 너무 많으면 합성이 느려지는 데다 죽은 코드가 섞인 비최적 프로그램이 나올 수 있다. 앞의 오른쪽 0 비트 예시에서 해를 보존하는 최소 라이브러리는 not, add1, and 각 하나씩으로 이뤄진 셋이다. 이 합성기에서 컴포넌트는 고정 비트폭 정수(SMT 용어로 비트벡터)에 대한 함수이며 add, and, xor 같은 가상 명령어 하나에 대응하지만, 원리상 더 고수준 함수도 SMT 질의로 인코딩할 수 있다면 컴포넌트가 될 수 있다.
존재-전칭 문제와 CEGIS
프로그램 합성은 본질적으로 존재-전칭(exists-forall) 문제다. '모든 입력에 대해 명세를 만족하는 어떤 프로그램 P가 존재하는가'를 묻기 때문이다. 문제는 Z3 같은 기성 SMT 솔버가 잘 푸는 것은 자유 변수를 포함하고 중첩된 한정자가 없는 일차식, 즉 암묵적 존재 질의라는 점이다. 솔버는 명세를 SMT-LIB2라는 Lisp 계열 언어로 받아 만족 가능(변수 할당과 모델을 함께 제시)인지 불만족(어떤 할당으로도 참이 될 수 없음)인지를 판정한다. 명시적인 전칭·존재 한정자를 중첩한 고차식도 일부 지원하지만 훨씬 느리고 불완전하다.
이 간극을 메우는 것이 반례 유도 반복 합성(CEGIS)이다. CEGIS는 어려운 이차 존재-전칭 질의를 여러 개의 일차 존재 질의로 분해한다. 먼저 유한한 입력 집합을 임의로 하나 고른 뒤 루프를 돈다. 유한 합성 단계에서는 그 입력 집합에 대해서만이라도 올바른 후보 프로그램을 만들고, 검증 단계에서는 그 후보가 모든 입력에 대해 옳은지 확인한다. 옳으면 완료이고, 틀린 입력(반례)이 나오면 그것을 입력 집합에 추가해 다시 합성하는 식으로 수렴시켜 간다. 글쓴이의 구현이 바로 이 형식화를 거의 그대로 Z3에 질의하는 구조다.
실무적 의미와 한계
한국의 컴파일러·런타임·보안 실무자에게 이 접근이 주는 시사점은 분명하다. 최적화 규칙, 비트 트릭, 명세가 명확한 소규모 변환 코드처럼 '정답 여부를 기계적으로 판정할 수 있는' 영역이라면 사람의 직관보다 합성기가 더 짧고 정확한 해를 낼 여지가 있다. 특히 규칙 수가 수백~수천 개에 이르는 최적화기를 손으로 관리하는 대신 명세로부터 자동 생성하는 파이프라인은 유지보수 부담을 크게 줄일 수 있다.
다만 이 글은 성공담만 담고 있지 않다는 점이 오히려 실무적으로 중요하다. 글쓴이 스스로 구현의 성능 문제를 인정하며, 더 어려운 벤치마크에서는 인내심이 바닥날 때까지도 해를 찾지 못해 문헌에 보고된 합성 결과를 재현하지 못했다고 밝힌다. 즉 컴포넌트 기반·루프 프리라는 제약과 CEGIS의 반복 구조에도 불구하고, 문제 규모가 커지면 탐색 비용은 여전히 실전에서 발목을 잡는다. 라이브러리 구성이라는 사람의 사전 판단이 결과 품질과 속도를 좌우한다는 점도 완전한 자동화와는 거리가 있다. 프로그램 합성은 좁고 잘 정의된 문제에서 이미 실용적이지만, 범용 코드 생성으로 확장하려면 탐색 효율이라는 벽을 넘어야 한다는 것이 이 글이 남기는 현실적인 결론이다.