프로그램 합성·CEGIS·반례로 후보 좁히기

합성에는 문법·명세·검증기가 필요하다

프로그램이 예제에 맞고 타입 검사를 통과해도 원하는 함수를 구현하지 않을 수 있습니다. 프로그램 합성은 명시한 언어 안에서 명세를 만족하는 프로그램을 찾는 문제입니다. 여기서는 후보 생성과 검증을 나누고, 반례를 다음 후보 선택에 사용하는 CEGIS를 살펴봅니다.

실습 언어는 계수를 고르는 작은 다항식 DSL입니다.

$$G_k=\{p(x)=ax^2+bx+c:\ a,b,c\in\mathbb Z,\ -k\le a,b,c\le k\}.$$

k=1,2,3이면 각각 27,125,343개 프로그램이 있습니다. 명세는 2x+1, x², abs(x), 3x+1 중 하나입니다. 검증기는 다음의 유한한 정수 영역만 검사합니다.

$$D_r=\{-r,-r+1,\ldots,r\},\qquad r\in\{0,1,2\}.$$

r=0도 입력 0 하나를 포함합니다. 합성 주장은 한정된 문법 안의 어떤 프로그램이 이 유한 영역의 모든 점에서 맞는다는 뜻입니다. 모든 정수나 실수에 대한 주장이 아닙니다.

예제가 남아 있는 후보 공간을 정의한다

이미 올바른 출력을 알려준 입력 집합을 E라고 합시다.

$$V(E)=\{p\in G_k:\ \forall x\in E,\ p(x)=\operatorname{spec}(x)\}.$$

합성기는 이 후보들을 열거해 정해진 순서의 첫 프로그램을 선택합니다. 계수 비용 |a|+|b|+|c|가 작을수록 먼저, 동률이면 (a,b,c)의 사전순입니다. 작은 계수를 선호하는 규칙이지 E 밖에서 맞는다는 보장이나 소스 코드 길이의 최적화는 아닙니다. 명세의 계수를 직접 복사하지 않고 저장된 예제의 출력만 이용합니다.

초기 예제 비트 1,2,4,8,16은 입력 −2,−1,0,1,2입니다. D 밖의 요청 예제는 무시하고 별도로 표시합니다. −3부터 3까지의 독립 조회 입력은 진단용이므로 바꿔도 E나 합성한 프로그램에 영향을 주지 않습니다.

검증은 실제 실패 입력을 반환한다

유한 검증기는 D의 입력을 작은 순서부터 모두 살펴봅니다. 현재 프로그램이 명세와 다른 첫 점 z를 반환합니다.

$$z\in D,\qquad p(z)\ne\operatorname{spec}(z).$$

이는 실패의 증거인 반례입니다. 두 출력값을 함께 보면 왜 잘못되었는지 확인할 수 있습니다. z는 다음 단계의 E에만 추가합니다. 현재 프로그램은 이미 E 전체에 맞으므로 z가 기존 E에 들어 있을 수 없습니다. 따라서 다음 후보 공간은 엄격히 작아집니다.

$$V(E\cup\{z\})\subsetneq V(E).$$

반례 하나는 현재 프로그램뿐 아니라 같은 입력에서 실수하는 다른 후보들도 함께 제거합니다. 단순히 한 프로그램에 낮은 점수를 주는 것보다 후보 집합 전체에 정보를 주는 셈입니다.

후보가 사라지면 한정 문법 안에서는 저장 예제와 전체 유한 명세를 만족할 프로그램이 없습니다. 원하는 함수가 다른 문법에는 있을 수 있으므로 명세 자체가 모순이라는 뜻은 아닙니다. D에서 반례가 없으면 그 영역에서 검증된 결과입니다. 여기서는 문법과 영역을 모두 열거하므로 두 종료 결과를 정확히 구분할 수 있습니다.

두 그림을 읽는 방법

계수 격자는 c를 고정한 단면입니다. 열은 a, 행은 b입니다. ○는 현재 E에 맞고, !는 아직 E에 맞지만 현재 반례를 추가하면 제외될 후보입니다. *는 현재 프로그램, ×는 E로 이미 제외한 후보입니다. 전체 후보 수에는 보이지 않는 c 층도 포함됩니다. 프로그램이 없을 때는 c=0 단면을 조회용으로 표시할 뿐 후보를 만들어내지 않습니다.

흐름 그림은 현재 예제·후보·유한 검증을 보여줍니다. 반례는 다음 단계에 반영하므로 이전 단계를 조회할 때 미래의 프로그램이나 반례를 가져오지 않습니다. 마지막보다 큰 요청 단계는 실제 이력의 끝으로 제한합니다.

비교 그림은 −3부터 3까지 일곱 정수 조회점에서 파란 프로그램과 주황 명세를 평가합니다. 연속적인 증명 곡선이 아닙니다. 그 중 일부 점은 D 밖일 수 있습니다. 후보가 없으면 파란 곡선도 출력값도 없으며, 실제 값이 0인 영 프로그램과 다릅니다.

손계산: 예제 하나는 완전한 명세가 아니다

명세 2x+1, k=2, 반경 2, 초기 mask 4를 사용합니다. 알려진 입력은 x=0뿐입니다. 0단계에서 최소 비용의 일치 후보는 상수 1이고 총 25개 프로그램이 이 예제에 맞습니다. 하지만 x=−2에서 프로그램은 1, 명세는 −3을 주므로 검증기가 −2를 반환합니다.

1단계의 E={−2,0}에는 후보가 세 개 남습니다. 먼저 고른 1−x²는 두 점에 맞지만 −1에서는 0을 반환하여 명세 −1과 다릅니다. 2단계의 E={−2,−1,0}에는 계수 (0,2,1) 하나가 남고 다섯 검증 입력을 모두 만족합니다.

계수 그림의 c=1 단면에서 살아 있는 후보가 25개에서 세 개, 한 개로 줄어듭니다. 처음 반례는 현재 상수 프로그램을 포함한 22개 후보를 제거합니다. 실제 제거는 1단계로 넘어간 뒤에 표시됩니다.

손계산: 유한 검증 성공과 범위 밖 실패

명세를 abs(x), k=2, 반경을 1로 놓습니다. x=0에서 시작하면 후보는 0, −x, x²로 바뀝니다. 마지막 프로그램은 −1,0,1에서 맞으므로 유한 영역의 인증은 유효합니다. 독립 조회 x=2에서는 프로그램이 4, 명세가 2입니다. 범위 밖 실패가 원래의 유한 인증을 무효로 만드는 것이 아니라 그 인증을 범위 밖으로 확대할 수 없음을 보여줍니다.

반경을 2로 확장하면 다섯 점을 모두 만족하는 한정 다항식 후보가 사라집니다. 그렇다고 절댓값 함수가 모순인 것은 아닙니다. abs 연산을 가진 다른 언어는 그대로 표현할 수 있습니다.

손계산: 목표 대신 문법을 바꾸기

3x+1도 잘 정의된 함수입니다. k=2, 반경 2의 문법에는 다섯 점을 만족하는 프로그램이 없습니다. k를 3으로 늘리면 (0,3,1)을 표현할 수 있고 같은 반례 루프가 그 프로그램을 찾습니다. 목표는 고정하고 문법만 바꾸어 실패의 원인을 살펴보세요.

처음 문법은 125개에서 343개 후보로 커집니다. 더 큰 시스템에서 문법 확장이 실행 시간의 모든 측면을 개선한다는 뜻은 아닙니다. 후보 순서, 검증 비용, 표현력은 서로 영향을 줍니다. 이 화면은 실제 실행 시간 벤치마크 대신 정확한 후보 수와 단계를 보여줍니다.

이 유한 루프가 종료하는 이유

성공적인 정제마다 D의 새 입력 하나가 E에 추가됩니다. 정제는 많아야 |D|−|E_initial|회이며 마지막 제안 상태까지 많아야 한 번 더 필요합니다. 실습에서는 최대 여섯 상태입니다. 유한 검증 성공 또는 후보 공간 소진으로 끝납니다. 예제를 많이 주면 이력이 줄어들 수 있지만 개수만으로 의도한 함수를 유일하게 정했다고 증명할 수는 없습니다.

유한 영역이라는 가정을 기억해야 합니다. 실습 밖에서 모든 정수 x와 다른 정수 상수 c를 합성한다고 합시다. 그런 c는 없지만 유한한 예제 집합에는 그 밖의 c를 계속 고를 수 있습니다. 반례마다 일부 후보를 제거한다는 이유만으로 무한 문법의 CEGIS가 종료하지는 않습니다. 실제 검증기의 unknown이나 시간 초과도 반례가 없다는 증명과 구분해야 합니다.

연습 문제와 해설: 일반화에는 어떤 추가 추론이 필요할까?

문제: 후보와 명세가 모두 차수 2 이하의 다항식임을 안다면, 서로 다른 세 점에서 일치하는 것으로 무엇을 알 수 있나요? x²를 abs(x)의 전체 구현이라고 말하는 데도 같은 논리를 쓸 수 있을까요?

해설: 두 다항식의 차이도 차수 2 이하입니다. 영이 아닌 그런 다항식은 서로 다른 근을 세 개 가질 수 없으므로 차이가 항등적으로 0입니다. 이 추가 수학적 가정과 논증은 모든 실수 입력에 대한 결론을 줍니다. abs(x)는 차수 2 이하의 다항식이라는 가정을 만족하지 않으므로 같은 논리를 적용할 수 없습니다. 화면은 그런 가정을 몰래 적용하지 않고 유한 검증 결과를 표시합니다.

추가 문제: 명세 2x+1에서 반경 0, 초기 mask 0을 사용하세요. 빈 E에는 영 프로그램이 먼저 맞지만 반례 입력은 0입니다. 숫자 0을 “반례 없음”과 혼동하면 안 됩니다. 이를 추가하면 상수 1이 단일점 영역에서 검증됩니다. 반경 0에서 다섯 초기 예제를 모두 요청해도 0만 사용하고 나머지 네 점은 무시 목록에 보입니다.

AI 연구와 연결하기

언어 모델이 후보를 제안하거나 문법의 우선순위를 정하면서 검증기는 반례를 줄 수 있습니다. 타입이 맞는 프로그램도 동작 명세를 만족하는지 따로 확인해야 합니다. 유한한 시험의 성공, 한정 문법 소진, 무한 영역의 증명은 서로 다른 결과입니다. 생성 프로그램을 연구 증거로 사용할 때는 그 범위를 명확히 기록해야 합니다.

Armando Solar-Lezama의 MIT 프로그램 합성 17강은 명세·검사·반례에 의한 정제의 관계를 설명합니다. 정수 계수 문법과 비용 순서, 영역 조작, 위 예제는 교재를 위해 직접 구성했습니다.