[Program Synthesis #3] CEGIS: 반례로 프로그램을 찾아가는 방법

들어가며

앞선 글에서 우리는 Program Synthesis 문제를
논리식(SAT/SMT), 그리고 grammar 기반 문제(SyGuS)로 바꾸는 방법을 살펴봤다.

이제 진짜 중요한 질문이 남는다.

“그래서 프로그램은 어떻게 찾는가?”

이 질문에 대한 가장 핵심적인 답이 바로 CEGIS다.

CEGIS는 CounterExample-Guided Inductive Synthesis의 약자로,
이름 그대로 “반례(counterexample)를 이용해서 프로그램을 점점 개선해 나가는 방법”이다.

이 방식은 단순한 brute-force가 아니라,
틀린 프로그램을 빠르게 제거하면서 정답으로 수렴하는 구조를 가진다.

이 글에서는 다음을 다룬다:

• Program Synthesis를 푸는 기본 루프
• CEGIS 알고리즘의 구조
• 왜 이 방식이 효과적인지
• 실제로 어떻게 동작하는지

이 글을 이해하면, 이후 나오는 대부분의 synthesis 기법들은
전부 “CEGIS의 변형”이라는 걸 보게 될 것이다.

---

CEGIS의 핵심 아이디어

Program Synthesis 문제를 다시 생각해보자.

우리는 다음과 같은 문제를 풀고 있다:

\[\exists f.\ \forall x.\ P(f, x)\]

즉,

• 어떤 프로그램 \(f\)를 찾아서
• 모든 입력 \(x\)에 대해
• 원하는 조건 \(P(f, x)\)를 만족하게 해야 한다

---

이 문제는 직접 풀기 어렵다.

왜냐하면:

• \(f\)는 프로그램 전체 (거대한 공간)
• \(x\)는 모든 가능한 입력 (무한 공간)

---

그래서 CEGIS는 이걸 이렇게 바꾼다:

“모든 입력을 한 번에 보지 말고,
일부 입력만 보고 프로그램을 만들고 → 틀리면 고친다”

---

이걸 일상적인 비유로 보면:

1. 대충 프로그램 하나 만든다 (guess)
2. 테스트를 돌린다
3. 틀린 입력을 발견한다 (counterexample)
4. 그 입력을 반영해서 다시 만든다

이 과정을 반복한다.

---

즉, CEGIS는 이렇게 요약된다:

“프로그램을 만들고 → 반례로 깨고 → 다시 만든다”

---

CEGIS 알고리즘 구조

앞에서 본 직관을 조금 더 정식화해보자.

CEGIS는 Program Synthesis 문제

\[\exists f.\ \forall x.\ P(f, x)\]

를 다음과 같은 반복 구조로 푼다:

---

1. 두 개의 문제로 나누기

CEGIS의 핵심은 문제를 두 개로 분리하는 것이다.

• Synthesis 문제 (Generator)
• Verification 문제 (Checker)

---

Generator (프로그램 생성)

현재까지 알려진 입력 집합 \(E\)에 대해:

\[\exists f.\ \forall x \in E.\ P(f, x)\]

즉,

“지금까지 발견된 입력들에서는 맞는 프로그램을 하나 만들어라”

---

Checker (검증)

이제 그 프로그램이 진짜 맞는지 확인한다:

\[\exists x.\ \neg P(f, x)\]

즉,

“이 프로그램을 틀리게 만드는 입력이 존재하는가?”

---

• 존재하면 → counterexample 발견
• 없으면 → 정답 프로그램

---

2. 전체 루프

이걸 합치면 CEGIS는 다음과 같은 반복이 된다:

E = {}  # counterexample set

while True:
    f = synthesize(E)   # Generator
    
    x = verify(f)       # Checker
    
    if x is None:
        return f        # 정답 발견
    
    E = E ∪ {x}         # 반례 추가

---

3. 핵심 포인트

이 구조에서 중요한 점은 딱 세 가지다:

---

(1) 전체 입력을 보지 않는다

처음에는 \(E = \emptyset\) 이다.

즉, 프로그램은 아무 제약 없이 생성된다.

→ 그래서 매우 빠르게 후보가 나온다

---

(2) 틀린 부분만 학습한다

Checker는 전체를 검사하는 대신,

“딱 하나 틀리는 입력”만 찾아준다

→ search space를 효율적으로 줄인다

---

(3) 점점 정확해진다

\[E = \{x_1, x_2, x_3, ...\}\]

이렇게 반례가 쌓일수록,

• Generator는 더 많은 조건을 만족해야 하고
• 프로그램은 점점 정답에 가까워진다

---

4. 구조적으로 보면

CEGIS는 사실 이렇게 볼 수 있다:

Induction + Counterexample

• Induction: 일부 데이터로 일반화된 프로그램 생성
• Counterexample: 잘못된 일반화를 깨는 증거

---

즉,

“틀릴 수 있는 자유를 주고 → 틀리면 바로 고친다”

이게 CEGIS의 본질이다.

---

간단한 예제로 보는 CEGIS

이제 CEGIS가 실제로 어떻게 동작하는지 간단한 예제로 살펴보자.

---

문제 정의

다음과 같은 프로그램을 찾고 싶다고 하자:

입력 \(x\)에 대해 \(x + 1\)을 반환하는 함수 \(f(x)\)

즉, 우리가 원하는 조건은:

\[P(f, x) := f(x) = x + 1\]

---

그리고 우리는 다음과 같은 매우 제한된 grammar를 사용한다고 가정하자:

f(x) ::= x
       | x + 1
       | x + 2

---

Step 1 — 초기 상태

처음에는 counterexample 집합이 비어 있다:

\[E = \emptyset\]

---

Generator는 다음 문제를 푼다:

\[\exists f.\ \forall x \in \emptyset.\ P(f, x)\]

이건 항상 참이다.

→ 즉, 아무 프로그램이나 선택해도 된다.

---

그래서 Generator는 임의로 다음을 선택할 수 있다:

f(x) = x

---

Step 2 — Verification

이제 Checker가 등장한다.

우리는 다음을 검사한다:

\[\exists x.\ f(x) \neq x + 1\]

---

간단히 보면:

• \(x = 0\)일 때
• \[f(0) = 0\]
• 하지만 \(0 + 1 = 1\)

→ 틀렸다

---

그래서 counterexample:

\[x = 0\]

---

이제:

\[E = \{0\}\]

---

Step 3 — 다시 Synthesis

이제 Generator는 다음을 만족해야 한다:

\[\exists f.\ P(f, 0)\]

즉,

\[f(0) = 1\]

---

가능한 후보들을 보면:

• \(f(x) = x\) → \(f(0)=0\) ❌
• \(f(x) = x + 1\) → \(f(0)=1\) ✅
• \(f(x) = x + 2\) → \(f(0)=2\) ❌

---

그래서 Generator는:

f(x) = x + 1

을 선택한다.

---

Step 4 — 다시 Verification

이제 다시 검사한다:

\[\exists x.\ f(x) \neq x + 1\]

---

이번에는?

• 어떤 \(x\)를 넣어도
• \[f(x) = x + 1\]

→ 반례 없음

---

즉,

검증 성공 → synthesis 종료

---

전체 흐름 요약

1. 틀린 프로그램 \(f(x)=x\) 생성
2. 반례 \(x=0\) 발견
3. 조건 강화
4. 올바른 프로그램 \(f(x)=x+1\) 도출

---

중요한 관찰

이 예제에서 핵심은 이것이다:

처음부터 완벽한 프로그램을 찾지 않는다

대신:

• “대충 맞는 프로그램”을 만들고
• “틀린 부분만 수정”한다

---

이 방식 덕분에:

• 전체 입력 공간을 다 보지 않아도 되고
• 빠르게 정답으로 수렴할 수 있다

---

왜 CEGIS는 잘 동작하는가

앞의 예제는 단순했지만, 중요한 질문이 하나 남는다.

왜 이런 방식이 실제로도 잘 동작할까?

CEGIS는 겉보기에는 단순한 반복처럼 보이지만,
그 안에는 매우 중요한 구조적 이유가 있다.

---

1. 문제를 “어려운 것 → 쉬운 것”으로 바꾼다

원래 우리가 풀고 싶은 문제는 이것이다:

\[\exists f.\ \forall x.\ P(f, x)\]

이건 매우 어렵다.

• \(f\)는 프로그램 전체
• \(x\)는 모든 입력

---

CEGIS는 이걸 이렇게 바꾼다:

\[\exists f.\ \forall x \in E.\ P(f, x)\]

즉,

“일부 입력만 맞추는 문제”로 축소한다

---

이건 훨씬 쉽다.

• 입력이 finite set \(E\)로 제한됨
• constraint solving이 가능해짐 (SMT로 풀 수 있음)

---

2. Verification이 “틀린 부분만 알려준다”

Checker는 전체 correctness를 증명하지 않는다.

대신:

\[\exists x.\ \neg P(f, x)\]

이걸 푼다.

---

즉,

“이 프로그램을 깨는 입력 하나만 찾아라”

---

이게 중요한 이유는:

• 전체 검증보다 훨씬 쉽고
• 실패 원인을 정확히 pinpoint 한다

---

3. Search space를 빠르게 줄인다

각 iteration에서 우리는 하나의 constraint를 추가한다:

\[P(f, x_1),\ P(f, x_2),\ \dots\]

---

즉 프로그램은 점점 더 많은 조건을 만족해야 한다.

이건 곧:

가능한 프로그램 후보가 계속 줄어든다는 뜻이다

---

직관적으로 보면:

• 처음: 거의 모든 프로그램 가능
• 중간: 일부만 가능
• 마지막: 정답만 남음

---

4. Overfitting을 방지한다

Inductive synthesis에서 가장 큰 문제는 이것이다:

주어진 예제에는 맞지만, 실제로는 틀린 프로그램

---

CEGIS는 이 문제를 이렇게 해결한다:

• 잘못된 일반화 → counterexample로 깨짐
• 그 입력이 다음 학습에 반영됨

---

즉,

“틀린 일반화는 반드시 반례로 제거된다”

---

5. Lazy solving과의 유사성

이 구조는 앞에서 본 SMT의 Lazy 방식과 매우 닮아 있다.

Recall:

\[\text{Guess} \rightarrow \text{Check} \rightarrow \text{Refine}\]

---

CEGIS도 동일하다:

\[\text{Program} \rightarrow \text{Counterexample} \rightarrow \text{Refine}\]

---

즉,

CEGIS는 synthesis 버전의 Lazy solving이다

---

핵심 정리

CEGIS가 잘 동작하는 이유는 다음 세 가지로 요약된다:

• 전체 문제를 작은 문제로 쪼갠다
• 틀린 부분만 정확히 수정한다
• 반복하면서 탐색 공간을 빠르게 줄인다

---

그래서 CEGIS는 단순한 알고리즘이 아니라,

Program Synthesis의 “기본 구조”

라고 볼 수 있다.

---

SyGuS와 SMT에서의 CEGIS

지금까지 CEGIS를 하나의 알고리즘으로 이해했다.
이제 중요한 질문이 남는다.

이 구조가 실제 SyGuS solver에서는 어떻게 사용될까?

---

1. 역할 분담: Generator vs SMT Solver

CEGIS를 다시 보면 두 개의 역할이 있었다:

• Generator: 프로그램을 만든다
• Checker: 프로그램이 맞는지 검사한다

---

SyGuS에서는 이 역할이 다음처럼 나뉜다:

• Generator → synthesis engine
• Checker → SMT solver

---

즉,

SMT solver는 “프로그램이 틀렸는지 찾는 역할”을 한다

---

2. Verification은 SMT 문제다

Checker 단계는 다음 문제를 푸는 것이다:

\[\exists x.\ \neg P(f, x)\]

---

이건 정확히 SMT 문제다.

예를 들어:

\[f(x) = x + 1\]

이고,

\[P(f, x) := f(x) = x + 1\]

라면 SMT solver는 이런 질문을 받는다:

“이 식을 깨는 \(x\)가 존재하는가?”

---

• 존재하면 → 모델 (counterexample) 반환
• 없으면 → UNSAT (정답)

---

즉,

counterexample은 SMT solver가 생성하는 모델이다

---

3. 전체 구조를 다시 보면

SyGuS solver는 내부적으로 다음 구조를 가진다:

\[\text{Generate} \rightarrow \text{SMT Check} \rightarrow \text{Refine}\]

---

조금 더 구체적으로 쓰면:

E = {}

while True:
    f = generate_from_grammar(E)
    
    x = SMT_solve(∃x. ¬P(f, x))
    
    if UNSAT:
        return f
    
    E.add(x)

---

4. Grammar와의 연결

여기서 중요한 점 하나:

Generator는 아무 프로그램이나 만드는 것이 아니다

---

항상 다음 조건을 만족해야 한다:

\[f \in L(G)\]

즉,

• Grammar가 허용하는 프로그램만 생성 가능
• search space는 이미 제한되어 있음

---

그래서 전체 구조는 이렇게 된다:

\[\text{Grammar} + \text{CEGIS} + \text{SMT}\]

---

• Grammar → 어디까지 탐색할지
• CEGIS → 어떻게 탐색할지
• SMT → 맞는지 검사

---

5. 핵심 통합 구조

이제 SyGuS 전체를 한 줄로 정리하면 이렇게 된다:

\[\text{Synthesis} = \text{Search (Grammar)} + \text{Verification (SMT)} + \text{Loop (CEGIS)}\]

---

이게 바로 실제 synthesis system의 기본 구조다.

---

중요한 관점

이제 관점이 완전히 바뀐다.

우리는 더 이상:

“프로그램을 만든다”

가 아니라,

“프로그램 후보를 만들고, SMT로 틀린 걸 제거한다”

를 하고 있다.

---

즉 Program Synthesis는 본질적으로:

탐색 + 반례 기반 필터링 과정

이다.

---

다음 글

이제 전체 구조는 완성됐다.

다음 글에서는 이 구조의 첫 번째 핵심 구성 요소인

Enumerative Synthesis

를 다룬다.

• Grammar에서 프로그램을 실제로 어떻게 생성하는지
• bottom-up vs top-down
• 왜 naive enumeration이 터지는지

를 구체적으로 살펴보게 된다.