[Program Synthesis #2] SyGuS 심화: SMT와 Grammar로 프로그램 합성 이해하기

들어가며

앞 글에서는 프로그램 합성을 논리 문제로 바꾸는 과정,
그리고 그 출발점인 SAT까지 살펴봤다.

핵심 질문은 다음이었다.

\[\text{“이 조건을 만족하는 해가 존재하는가?”}\]

하지만 SAT에는 분명한 한계가 있다.

모든 것을 True/False로만 표현해야 한다

현실의 프로그램은 그렇지 않다.

• 숫자를 다루고
• 배열을 다루고
• 함수와 연산을 사용한다

따라서 SAT만으로는 실제 프로그램의 의미를 표현하기 어렵다.

이 글에서는 그 한계를 넘어서기 위해 등장하는 개념들,
즉 First-Order Logic → SMT → Grammar → SyGuS로 이어지는 흐름을 살펴본다.

---

First-Order Logic — 더 현실적인 조건을 표현하는 논리

SAT까지 오면 한 가지 한계가 분명하게 보인다.
Boolean 논리는 강력하지만, 현실의 프로그램을 표현하기에는 너무 단순하다.

명제 논리에서는 모든 변수가 오직 다음 두 값만 가진다.

\[p, q, r \in \{T, F\}\]

하지만 실제 프로그램은 그렇지 않다.

• 숫자를 더하고
• 배열을 읽고
• 함수를 계산하고
• 모든 입력에 대한 성질을 말해야 한다

즉, 프로그램의 의미를 다루려면 True/False만으로는 부족하다.
이 한계를 넘어서는 것이 바로 First-Order Logic(1차 논리) 다.

왜 1차 논리가 필요한가

우리는 실제로 이런 조건을 표현하고 싶다.

\[x + y = 10\] \[A[i] \le A[i+1]\] \[f(x) = x + 1\]

이런 식은 명제 논리만으로는 자연스럽게 표현할 수 없다.
그래서 더 풍부한 표현력을 가진 논리가 필요하다.

1차 논리에서는 무엇이 추가되나

가장 큰 변화는 세 가지다.

첫째, 변수는 이제 단순 Boolean이 아니라 다양한 값을 가질 수 있다.

\[x, y \in \mathbb{Z}\]

둘째, 함수와 관계를 표현할 수 있다.

\[f(x), \quad g(x, y)\]

셋째, 가장 중요한 요소로 양화사가 등장한다.

\[\forall \quad \text{(for all)}\] \[\exists \quad \text{(there exists)}\]

덕분에 우리는 “모든 입력에 대해” 혹은 “어떤 값이 존재해서” 같은 문장을 직접 쓸 수 있다.

예제로 보면 더 분명하다

다음 식은 숫자 범위를 표현한다.

\[x \le 3 \land 0 \le x\]

즉 \(x\)는 0 이상 3 이하라는 뜻이다.

다음은 비트 연산 예시다.

\[\exists x.\; x \gg 0x01 = 0x02\]

그리고 프로그램 검증과 직접 연결되는 중요한 예시는 다음과 같다.

\[\forall k.\; 0 \le k < n \Rightarrow A[k] \le A[k+1]\]

이 식은 배열 \(A\)가 정렬되어 있음을 표현한다.

이쯤 되면 명제 논리와 1차 논리의 차이가 분명해진다.

• 명제 논리 → 스위치 문제
• 1차 논리 → 프로그램 문제

왜 SyGuS에서 중요한가

Program synthesis에서는 보통 이런 질문을 한다.

\[\text{“이 프로그램이 모든 입력에서 올바르게 동작하는가?”}\]

이 질문을 형식적으로 표현하려면 자연스럽게 이런 형태가 필요하다.

\[\forall x.\; \text{condition}(x)\]

즉 1차 논리는 단순히 표현력이 좋은 논리가 아니라,
프로그램의 의미와 명세를 담기 위한 기본 언어다.

SMT — SAT를 더 풍부한 세계로 확장하기

이제 SAT의 한계를 넘어서야 한다.
SAT는 “만족하는 해가 존재하는가”를 묻지만, 모든 변수가 Boolean이라는 제한이 있다.

하지만 실제로 우리가 다루고 싶은 식은 이런 것들이다.

\[x + y = 10 \land x > 0\] \[A[i] = A[j]\] \[(x \mathbin{\&} 1) = 0\]

이런 식을 다루기 위해 등장하는 것이 SMT (Satisfiability Modulo Theories) 다.

SMT — SAT를 더 현실적인 세계로 확장한 문제

SAT까지 이해하고 나면 자연스럽게 한 가지 한계가 보인다.
SAT는 분명 강력하지만, 모든 변수를 오직 True/False로만 다룬다는 제약이 있다.

즉, SAT에서는 기본적으로 이런 형태의 문제를 푼다.

\[p, q, r \in \{T, F\}\]

이 방식은 논리 구조를 이해하는 데는 매우 유용하지만, 실제 프로그램을 다루기에는 너무 단순하다.
우리가 진짜 표현하고 싶은 조건은 보통 이런 것들이다.

\[x + y = 10 \land x > 0\] \[A[i] \le A[i+1]\] \[(x \gg 1) = 2\]

이런 식은 단순 Boolean 조합만으로는 자연스럽게 표현하기 어렵다.
바로 이 지점에서 SMT (Satisfiability Modulo Theories) 가 등장한다.

SMT란 무엇인가

SMT의 핵심은 한 문장으로 정리할 수 있다.

SMT = SAT + Theory

즉, SAT의 기본 질문은 그대로 유지하되,
그 질문을 더 풍부한 구조와 규칙을 가진 세계로 확장한 것이다.

조금 더 수식적으로 표현하면 다음처럼 이해할 수 있다.

\[\text{SMT} = \text{Satisfiability over richer domains}\]

핵심 질문도 아주 명확하다.

이 논리식을 특정 이론 아래에서 만족할 수 있는가?

SAT가 “Boolean 식을 만족하는 값이 존재하는가?”를 묻는다면,
SMT는 “정수, 배열, 비트벡터 같은 실제 도메인을 포함한 식을 만족하는 값이 존재하는가?”를 묻는다.

Theory는 무엇인가

여기서 말하는 Theory(이론) 는 복잡한 철학적 개념이 아니다.
그냥 특정 도메인에서 허용되는 연산과 규칙의 묶음이라고 보면 된다.

즉,

Theory = 특정 분야의 규칙 집합

이다.

예를 들어 정수 이론에서는 덧셈, 뺄셈, 비교 같은 연산을 다룬다.
배열 이론에서는 배열의 읽기와 쓰기를 다룬다.
비트벡터 이론에서는 shift, and, or 같은 비트 연산을 다룬다.
문자열 이론에서는 길이, 연결, substring 같은 연산을 다룬다.

조금 더 구체적으로 보면 다음과 같다.

• 정수 이론:
  \(x + y = y + x\) 같은 산술 관계를 다룬다.

• 배열 이론:
  \(A[i]\) 처럼 특정 인덱스의 값을 읽거나, 배열에 값을 쓰는 연산을 다룬다.

• 비트벡터 이론:
  shift, and, or 같은 비트 수준 연산을 표현할 수 있다.

• 문자열 이론:
  문자열 길이, 부분 문자열, 연결 등을 표현할 수 있다.

즉 SMT는 단순히 논리식만 보는 것이 아니라,
그 식이 어떤 세계의 규칙 아래에서 해석되는지까지 함께 본다.

SAT와 SMT는 무엇이 다른가

SAT와 SMT의 차이를 한 번에 보면 더 분명하다.

구분	SAT	SMT
변수	Boolean	다양한 타입
표현력	낮음	높음
예시	\(p \land q\)	\(x + y = 10\)

직관적으로 말하면 이렇다.

• SAT는 스위치 ON/OFF를 맞추는 문제에 가깝다.
• SMT는 실제 수학 문제나 프로그램 조건을 푸는 문제에 가깝다.

즉 SAT가 “형식적인 논리 조합”을 다룬다면,
SMT는 “현실적인 구조를 가진 논리 문제”를 다룬다.

Interpretation도 달라진다

앞에서 SAT를 설명할 때 Interpretation은 변수에 True/False를 넣는 것이라고 했다.
SMT에서는 그 Interpretation의 의미 자체가 더 풍부해진다.

SAT에서는 보통 이렇게 생각하면 된다.

\[\text{variables} \rightarrow \{T, F\}\]

즉 각 변수는 True 아니면 False다.

하지만 SMT에서는 이렇게 바뀐다.

\[\text{variables} \rightarrow \text{domain}\]

여기서 domain은 정수일 수도 있고, 비트벡터일 수도 있고, 배열일 수도 있다.

예를 들면:

\[x = 3,\quad y = 10\]

처럼 실제 값을 해석에 넣는다.

즉 SMT에서 변수는 더 이상 단순 스위치가 아니다.
실제 의미를 가진 값이다.

SMT 문제를 다시 쓰면

이제 SMT를 한 문장으로 다시 정리하면 이렇게 된다.

\[\text{“이 논리식을 이론 } T \text{ 하에서 만족할 수 있는가?”}\]

결과는 SAT 때와 마찬가지로 두 가지다.

• SAT: 가능한 해가 존재한다
• UNSAT: 가능한 해가 존재하지 않는다

다만 이제 그 “해”는 True/False 조합이 아니라
정수, 배열, 비트벡터 같은 실제 값을 포함할 수 있다.

SyGuS와 연결하면

Program synthesis에서는 계속 이런 질문을 던지게 된다.

\[\text{“이 프로그램이 조건을 만족하는가?”}\]

이 질문은 결국 논리식의 만족 가능성 검사로 바뀐다.
그런데 그 논리식은 숫자, 함수, 배열, 비트 연산 등을 포함한다.
즉 실제 합성 문제를 다루려면 SAT만으로는 부족하고 SMT가 필요하다.

그래서 다음처럼 이해하면 된다.

SMT solver는 프로그램이 정말 맞는지 검사하는 엔진이다.

즉 SyGuS에서 SMT는 단순 보조 도구가 아니라,
후보 프로그램의 의미를 검증하는 핵심 장치다.

핵심만 정리하면

SMT는 이렇게 기억하면 된다.

\[\text{SMT} = \text{SAT} + \text{Theory}\]

• SAT는 Boolean만 다룬다.
• SMT는 더 풍부한 도메인과 규칙을 다룬다.

즉 SMT는 SAT를 현실적인 프로그램 세계로 확장한 형태다.

SMT는 실제로 어떻게 풀까? — Eager vs Lazy

SMT가 무엇인지는 알겠다.
그런데 여기서 자연스럽게 다음 질문이 나온다.

그래서 컴퓨터는 이런 SMT 문제를 실제로 어떻게 푸는가?

이 질문에 대한 대표적인 답이 바로 Eager 방식과 Lazy 방식이다.

둘 다 SMT 문제를 푸는 방법이지만,
문제를 다루는 태도는 꽤 다르다.

SMT solver는 두 개의 추론이 함께 움직인다

SMT를 이해할 때 가장 중요한 감각은 이것이다.

SMT solver는 사실 하나의 solver가 아니라, 두 종류의 추론이 협력하는 구조에 가깝다.

• 하나는 SAT solver
• 하나는 Theory solver

SAT solver는 Boolean 구조를 본다.
즉 “논리적으로 이 조합이 가능하냐?”를 다룬다.

Theory solver는 실제 도메인 규칙을 본다.
즉 “그 조합이 정수, 배열, 비트벡터 규칙까지 고려해도 정말 가능한가?”를 검사한다.

조금 더 직관적으로 말하면,

• SAT solver는
  논리적으로 말이 되냐를 본다.

• Theory solver는
  근데 그게 실제 값으로도 가능하냐를 본다.

SMT 문제는 이 둘이 계속 정보를 주고받으면서 풀린다.

Eager 방식 — 처음부터 SAT 문제로 바꾸는 방법

Eager 방식의 아이디어는 생각보다 단순하다.

복잡한 SMT 문제를 처음부터 SAT 문제로 바꿔서 한 번에 풀자

즉 풍부한 구조를 가진 식을 가능한 한 전부 Boolean 형태로 인코딩한 뒤,
그 결과를 SAT solver에 넘긴다.

예를 들어 어떤 함수 항들이 있다고 하자.

\[g(a), \quad g(b), \quad g(c)\]

Eager 방식에서는 이런 항들을 새로운 기호로 바꾼다.

\[g(a) \rightarrow A,\quad g(b) \rightarrow B,\quad g(c) \rightarrow C\]

그런 다음 함수의 성질을 유지하기 위한 제약도 함께 추가한다.
예를 들어 입력이 같으면 출력도 같아야 하므로:

\[a = b \Rightarrow A = B\]

라는 조건을 넣는다.

즉,

입력이 같으면 결과도 같아야 한다

는 성질까지 Boolean 수준에서 반영하려는 것이다.

이렇게 모든 것을 SAT 형태로 바꾼 뒤에는
그냥 SAT solver에 던져서 문제를 푼다.

Eager 방식의 장단점

Eager 방식은 개념상 깔끔하다.

• 복잡한 구조를 미리 다 풀어헤친다
• 최종적으로는 SAT solver 하나로 처리한다

하지만 단점도 분명하다.

• 변환 과정이 복잡하다
• 식의 크기가 매우 커질 수 있다
• 실제로는 인코딩 비용이 커서 비효율적일 수 있다

즉, “처음부터 완벽하게 다 바꿔서 풀자”는 생각은 직관적이지만,
문제가 커지면 그 대가도 커진다.

Lazy 방식 — 틀리면서 점점 맞춰가는 방법

실제로 더 중요한 것은 Lazy 방식이다.

Lazy 방식의 핵심은 다음 한 줄로 요약된다.

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

즉,

1. 일단 하나의 후보를 만든다
2. 그 후보가 실제로 가능한지 검사한다
3. 틀렸으면 그 실수를 금지한다
4. 다시 시도한다

처음 들으면 조금 무식해 보일 수 있다.
하지만 실제로는 이 방식이 훨씬 효율적이다.

Lazy 방식의 흐름

먼저 SAT solver가 어떤 조합을 하나 제안한다고 해보자.

예를 들어:

\[\{1, 2, 4\}\]

SAT solver 입장에서는
“논리적으로는 이 조합이면 될 것 같다”라고 본 것이다.

그런데 이제 Theory solver가 이 후보를 검사한다.
그리고 이런 식으로 말할 수 있다.

근데 1이랑 2는 동시에 참일 수 없는데?

즉 Boolean 수준에서는 가능해 보여도,
실제 이론 규칙 아래에서는 불가능한 조합이라는 뜻이다.

그러면 solver는 그 조합을 다시 금지하는 제약을 추가한다.

\[\neg (1 \land 2 \land 4)\]

이제 SAT solver는 방금 조합을 제외하고
새로운 후보를 다시 찾는다.

예를 들어 다음 같은 조합을 낼 수 있다.

\[\{1, \neg 2, 3, 4\}\]

그다음 또 Theory solver가 검사하고,
불가능하면 다시 금지 제약을 추가한다.

이 과정을 계속 반복한다.

즉 Lazy 방식은 처음부터 모든 것을 완벽하게 반영하지 않는다.
대신 틀린 조합을 하나씩 제거해가며 점점 정답에 가까워진다.

왜 Lazy 방식이 중요한가

여기서 핵심 직관은 이것이다.

처음부터 완벽하게 맞추는 건 어렵다.
대신 틀린 것을 하나씩 제거하는 편이 훨씬 쉽다.

이게 Lazy 방식의 본질이다.

비유하자면 시험 문제를 푸는 과정과 비슷하다.

1. 답을 하나 찍는다
2. 틀렸다고 한다
3. 왜 틀렸는지 알려준다
4. 같은 실수를 다시 하지 않게 만든다
5. 다시 시도한다

즉 Lazy 방식은 일종의 오답노트 기반 탐색이다.

Eager와 Lazy를 한 번에 비교하면

두 방식을 직관적으로 나누면 이렇다.

• Eager는
  처음부터 완벽하게 바꿔서 한 번에 풀려는 방식이다.

• Lazy는
  대충 시작한 뒤, 틀린 후보를 제거하면서 점점 정확하게 만드는 방식이다.

그리고 실제 SMT solving에서는 대체로 Lazy 방식이 훨씬 중요하다.
현대 solver들의 핵심 감각도 여기에 가깝다.

SyGuS와 연결되는 지점

이제 이 구조가 왜 중요한지 보인다.
Program synthesis도 사실 거의 똑같은 흐름을 따른다.

1. 프로그램 후보 하나를 만든다
2. 조건을 만족하는지 검사한다
3. 틀리면 버리거나 제약을 추가한다
4. 다시 후보를 만든다

즉,

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

이 구조는 SMT의 Lazy solving과 매우 닮아 있다.

그래서 다음처럼 이해해도 된다.

SMT solver는 후보 프로그램이 맞는지 검사하는 엔진이고,
합성은 그 검사 결과를 이용해 후보를 계속 정제하는 과정이다.

핵심만 정리하면

• Eager: 처음부터 전부 SAT로 바꿔 해결하려는 방식
• Lazy: 틀린 후보를 하나씩 제거하며 정답에 가까워지는 방식

그리고 실전에서는 대체로 Lazy 방식이 훨씬 더 중요하다.

Grammar — 어떤 프로그램을 만들 수 있는가를 정하는 규칙

지금까지 우리는 계속 이런 질문을 던졌다.

이 프로그램이 맞는가?

그런데 프로그램 합성에는 그보다 앞선 질문이 하나 더 있다.

애초에 어떤 프로그램을 만들 수 있는가?

이 질문에 답하는 것이 바로 Grammar(문법) 다.

SyGuS에서 Grammar는 단순한 부가 정보가 아니다.
오히려 탐색 공간 전체를 결정하는 핵심 장치다.

Grammar는 왜 필요한가

Program synthesis를 아무 제한 없이 생각해보면 문제가 바로 생긴다.

가능한 프로그램의 수는 사실상 무한하다

예를 들어 변수 \(x\) 하나만 있어도 다음 같은 식을 끝없이 만들 수 있다.

\[x\] \[x + 1\] \[x + x\] \[(x + 1) \times (x + 2)\]

그리고 그보다 더 복잡한 식도 계속 만들 수 있다.

이 상태에서 “조건을 만족하는 프로그램을 찾아라”라고 하면
탐색 공간이 너무 커서 사실상 다룰 수 없다.

그래서 Grammar가 필요해진다.

이 문제는 이런 형태의 프로그램만 만들어라

즉 문법은 프로그램 후보의 모양을 제한한다.

간단한 예제로 보면

문자열 문법 예시를 하나 보자.

\[S \rightarrow aSb\] \[S \rightarrow ba\]

이 문법은 시작 기호 \(S\)에서 출발해 규칙을 적용하면서 문자열을 만든다.

가장 간단한 경우는:

\[S \rightarrow ba\]

이므로 결과는:

\[ba\]

이다.

한 번 더 확장하면:

\[S \rightarrow aSb \rightarrow a(ba)b\]

즉 결과는:

\[abab\]

이 된다.

조금 더 확장하면:

\[S \rightarrow aSb \rightarrow aaSbb \rightarrow aababb\]

이처럼 Grammar는 하나의 결과를 만드는 것이 아니라,
만들 수 있는 결과들의 집합을 정의한다.

즉,

\[L(G) = \{ ba,\; abab,\; aababb,\; \dots \}\]

처럼 생각할 수 있다.

Grammar의 구성 요소

Grammar는 보통 다음 네 가지 요소로 이해하면 된다.

• Nonterminal: 아직 완성되지 않은 기호
  예: \(S\)

• Terminal: 최종 결과에 실제로 등장하는 기호
  예: \(a, b\)

• Production Rule: 기호를 어떻게 바꿀 수 있는지 나타내는 규칙
  예: \(S \rightarrow aSb\)

• Derivation: 규칙을 적용해 실제 결과를 만드는 과정
  예: \(S \rightarrow aSb \rightarrow abab\)

직관적으로 보면,

• nonterminal은 아직 더 만들어야 하는 상태이고
• terminal은 이미 완성된 결과이며
• production rule은 만드는 방법이다.

Context-Free Grammar

슬라이드에서 자주 등장하는 문법은 Context-Free Grammar(CFG) 다.

기본 형태는 다음과 같다.

\[A \rightarrow \alpha\]

여기서 \(A\)는 nonterminal이고,
\(\alpha\)는 terminal과 nonterminal의 조합이다.

예를 들어 올바른 괄호 문자열을 만드는 문법은 다음처럼 줄 수 있다.

\[S \rightarrow SS\] \[S \rightarrow (S)\] \[S \rightarrow ()\]

이 문법은 균형 잡힌 괄호 문자열만 생성한다.

즉 Grammar는 “허용되는 문장 구조”를 정의하는 장치라고 볼 수 있다.

SyGuS에서 Grammar는 무슨 역할을 하나

이제 다시 프로그램 합성으로 돌아오자.

SyGuS에서는 보통 이런 식의 문법을 준다.

\[S \rightarrow x \mid S + S \mid S \times S \mid 1\]

이 문법이 의미하는 것은 다음과 같다.

• 변수 \(x\)를 사용할 수 있다
• 덧셈을 사용할 수 있다
• 곱셈을 사용할 수 있다
• 상수 \(1\)을 사용할 수 있다

반대로 말하면 다음은 불가능하다.

• if문 없음
• 나눗셈 없음
• 그 외 허용되지 않은 연산 없음

즉 Grammar는 “무엇을 사용할 수 있는가”와 동시에
“무엇을 사용할 수 없는가”를 함께 정의한다.

왜 이게 중요한가

Program synthesis는 결국 탐색 문제다.
그런데 Grammar가 없으면 탐색 공간이 사실상 무한하다.

• Grammar가 없으면 → 무한 탐색
• Grammar가 있으면 → 제한된 탐색

그래서 SyGuS는 항상 이런 관점을 가진다.

정해진 Grammar 안에서만 프로그램을 만들어라

이것이 바로 “Syntax-Guided”라는 이름의 핵심이다.
단순히 조건만 맞는 프로그램을 찾는 것이 아니라,
문법이 허용하는 형태 안에서 답을 찾아야 한다.

한 줄로 정리하면

Grammar는 이렇게 기억하면 된다.

\[\text{Grammar} = \text{가능한 프로그램의 집합을 정의하는 규칙}\]

그리고 SyGuS에서는 이 집합이 바로 탐색 공간이 된다.

\[\text{Search Space} = L(G)\]

SyGuS Problem — 조건을 만족하는 프로그램을 찾는 문제

이제 필요한 조각들은 모두 모였다.

• 논리: 조건을 형식적으로 표현하는 도구
• SAT / SMT: 그 조건을 만족하는 해가 존재하는지 판단하는 도구
• Grammar: 만들 수 있는 프로그램의 범위를 제한하는 도구

이것들이 전부 합쳐지면 마침내 SyGuS 문제가 된다.

SyGuS를 한 문장으로 정의하면

SyGuS는 다음과 같은 문제다.

주어진 문법 안에서 만들 수 있는 프로그램 중,
조건을 만족하는 것을 찾아라

형식적으로 쓰면 다음과 같다.

\[\text{Find } e \in L(G) \text{ such that } \varphi[e/f] \text{ is valid}\]

처음 보면 조금 딱딱해 보이지만,
사실 지금까지 배운 내용을 압축한 식이다.

이 식을 하나씩 뜯어보면

먼저

\[e \in L(G)\]

는 후보 프로그램 \(e\)가 Grammar \(G\)로부터 생성될 수 있어야 한다는 뜻이다.
즉 아무 프로그램이나 되는 것이 아니라,
정해진 문법 안에서만 후보를 만든다는 의미다.

여기서 \(f\)는 우리가 만들고 싶은 미정의 함수다.
예를 들면:

\[f(x), \quad f(x, y)\]

같은 형태다.

그리고 \(\varphi\)는 우리가 원하는 성질, 즉 Specification(명세) 이다.
예를 들면 다음처럼 쓸 수 있다.

\[f(1) = 2 \land f(3) = 6\]

또는

\[\forall x.\; f(x) \ge x\]

처럼 더 일반적인 조건일 수도 있다.

이제

\[\varphi[e/f]\]

는 명세 \(\varphi\) 안에 등장하는 함수 \(f\)를
후보 프로그램 \(e\)로 치환한 식을 뜻한다.

예를 들어 후보 프로그램이

\[e(x) = 2x\]

라면, 명세 안의 \(f\) 대신 \(e\)를 넣어서 검사하는 것이다.

그리고 마지막 조건인

\[\varphi[e/f] \text{ is valid}\]

는 치환된 식이 모든 입력에서 항상 참이어야 한다는 뜻이다.

즉 테스트 몇 개를 통과하는 정도가 아니라,
조건이 일반적으로 성립해야 한다.

결국 SyGuS를 자연어로 풀면

이 수식을 자연어로 다시 쓰면 이렇게 된다.

Grammar로 만들 수 있는 프로그램 \(e\) 중에서,
명세의 미정의 함수 \(f\) 자리에 \(e\)를 넣었을 때
그 명세가 항상 참이 되는 프로그램을 찾아라

이것이 바로 SyGuS의 핵심 정의다.

입력과 출력을 다시 보면

프로그래밍 관점에서 보면 SyGuS의 구조는 분명하다.

입력은 두 가지다.

• 사용할 수 있는 프로그램 형태를 정의하는 Grammar
• 만족해야 하는 성질을 정의하는 Specification

출력은 하나다.

• 조건을 만족하는 Program

즉 구조적으로 보면:

\[\text{Grammar} + \text{Specification} \rightarrow \text{Program}\]

이라고 정리할 수 있다.

감각적으로 보면

이 문제는 비유하자면 요리 문제와 비슷하다.

• 재료 제한이 있다 → Grammar
• 맛 조건이 있다 → Specification

목표는 단순하다.

주어진 재료만 써서, 원하는 맛을 만족하는 요리를 하나 만들어라

이 비유가 좋은 이유는 SyGuS의 두 축을 정확히 보여주기 때문이다.

• 문법은 탐색 공간을 제한하고
• 명세는 정답의 의미를 정의한다

둘 중 하나라도 맞지 않으면 정답이 아니다.

중요한 디테일 몇 가지

SyGuS를 볼 때 놓치면 안 되는 포인트가 있다.

첫째, 명세는 보통 모든 입력에 대해 성립해야 한다.
즉 많은 경우 변수는 기본적으로 전칭적으로 해석된다.

\[\forall x.\; \varphi(x)\]

따라서 특정 입력 몇 개에서만 맞는 프로그램은 충분하지 않다.

둘째, Grammar는 보통 적당히 제한된다.
문법이 너무 자유로우면 탐색 공간이 폭발해서 계산이 어려워지기 때문이다.

슬라이드나 논문에서는 CFG보다 더 제한된 형태의 문법,
예를 들어 regular tree grammar 같은 표현이 등장하기도 한다.
핵심은 언제나 같다.

탐색 공간을 통제하지 않으면 합성이 너무 어려워진다

실제로는 어떻게 푸는가

SyGuS solver의 큰 흐름은 보통 다음과 같다.

1. Grammar를 이용해 후보 프로그램을 만든다
2. SMT로 그 후보가 명세를 만족하는지 검사한다
3. 맞으면 채택하고, 아니면 버린다
4. 정답이 나올 때까지 반복한다

즉 구조적으로는 다음과 같다.

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

이제 앞에서 본 내용이 한 번에 연결된다.

• 탐색은 Grammar가 담당하고
• 검증은 SMT가 담당한다

즉 SyGuS는 본질적으로 탐색 + 검증 문제다.

왜 어려운가

SyGuS는 겉보기에는 단순해 보인다.
하지만 실제로는 매우 어려운 문제다.

이유는 두 가지가 동시에 존재하기 때문이다.

• 가능한 프로그램 후보가 너무 많다 → 탐색이 어렵다
• 각 후보가 모든 입력에서 맞는지 검사해야 한다 → 검증이 어렵다

그래서 이론적으로도 난도가 높고,
실제로는 Grammar 제한, SMT 최적화, Lazy한 탐색 전략 등이 모두 필요하다.

슬라이드나 이론적 논의에서는
SyGuS 문제가 매우 높은 복잡도를 가진다고 설명되기도 한다.
즉 단순한 자동완성 문제가 아니라,
아주 본격적인 형식적 탐색 문제다.

최종 요약

SyGuS는 다음처럼 정리할 수 있다.

\[\text{SyGuS} = \text{Grammar} + \text{Specification} + \text{Search}\]

그리고 더 직관적으로 말하면:

조건을 만족하는 프로그램을 자동으로 찾는 문제

다만 여기서 중요한 것은
아무 프로그램이 아니라 문법이 허용하는 프로그램이어야 하고,
대충 맞는 프로그램이 아니라 명세를 만족하는 프로그램이어야 한다는 점이다.

마무리

여기까지 오면 SyGuS의 전체 구조가 한 번에 정리된다.

• SAT / SMT 는 조건을 형식적으로 표현하고 검사하는 도구다.
• Grammar 는 탐색할 수 있는 프로그램의 범위를 제한한다.
• SyGuS 는 이 둘을 결합해, 문법 안에서 명세를 만족하는 프로그램을 찾는 문제다.

즉 SyGuS는 결국 다음 한 문장으로 정리된다.

주어진 문법 안에서 만들 수 있는 프로그램 중, 명세를 만족하는 것을 찾아라

이번 글에서는 그 문제를 이해하기 위해 필요한 기초 재료들을 정리했다.
SAT에서 시작해 SMT로 확장하고, Grammar로 탐색 공간을 제한한 뒤,
마지막에 그것들이 SyGuS라는 하나의 문제로 결합되는 흐름을 본 셈이다.

다음 글에서는 여기서 한 걸음 더 나아가,

• 실제 SyGuS 예제가 어떻게 생겼는지
• solver가 후보 프로그램을 어떻게 만들고
• 왜 CEGIS (Counterexample-Guided Inductive Synthesis) 가 중요한지

를 본격적으로 다루게 된다.