[Program Synthesis #1] SyGuS 입문: 프로그램을 자동으로 만드는 방법
Program Synthesis 시리즈 1편 – SyGuS를 이해하기 위한 논리와 SAT(Satisfiability) 개념 정리
들어가며
프로그램을 만드는 일은 보통 사람이 직접 한다.
문제를 이해하고, 알고리즘을 떠올리고, 코드를 작성하는 식이다.
그런데 프로그램 합성은 이 흐름을 뒤집는다.
원하는 동작만 설명하면, 그 조건을 만족하는 프로그램을 자동으로 찾아낸다.
처음 들으면 꽤 강한 주장처럼 보이지만, SyGuS를 이해하고 나면 이 말이 생각보다 구조적인 문제라는 걸 알게 된다.
핵심은 결국 이것이다.
- 사람은 무엇을 원하는지 설명하고
- 시스템은 그 조건을 만족하는 후보를 찾는다
이 시리즈 1편에서는 그 출발점이 되는 개념들을 먼저 정리한다.
특히 프로그램 합성을 왜 논리 문제로 볼 수 있는지, 그리고 그 논리 문제를 이해하기 위한 가장 기본 개념인 명제 논리와 SAT까지 다룬다.
즉 이번 글의 중심 질문은 이것이다.
프로그램 합성을 왜 “조건을 만족하는 해를 찾는 문제”로 볼 수 있을까?
프로그램 합성 (Program Synthesis) — SyGuS를 이해하기 위한 첫걸음
프로그램 합성(Program Synthesis)은 한 문장으로 정리하면 이렇다.
“원하는 동작을 설명하면, 그걸 만족하는 프로그램을 자동으로 만들어주는 기술”
우리는 보통 코드를 직접 작성한다. 하지만 프로그램 합성에서는 역할이 조금 다르다.
- 사람은 무엇을 원하는지 (Specification) 정의하고
- 컴퓨터는 그걸 만족하는 코드 (Program) 를 만들어낸다
즉, 입력은 문제 설명이고, 출력은 코드다.
왜 이게 중요한가?
이 개념이 흥미로운 이유는 단순하다. 우리가 항상 하던 작업을 뒤집기 때문이다.
보통은 이렇게 한다:
- 문제를 이해하고
- 알고리즘을 생각하고
- 코드를 작성한다
하지만 프로그램 합성에서는:
- 문제 조건만 주면
- 컴퓨터가 알아서 코드를 찾는다
이건 단순 자동화가 아니라, “문제를 푸는 과정 자체를 자동화하는 것”에 가깝다.
SyGuS란 무엇인가?
이제 프로그램 합성 중에서도 가장 중요한 프레임워크 하나를 보자. 바로 SyGuS (Syntax-Guided Synthesis)다.
SyGuS는 프로그램 합성을 이렇게 정의한다:
“주어진 조건을 만족하는 프로그램을 자동으로 찾아라”
조금 더 구조적으로 보면 다음과 같다:
\[\text{Specification} \rightarrow \text{Synthesizer} \rightarrow \text{Program}\]- Specification: 우리가 원하는 조건
- Synthesizer: 프로그램을 찾는 엔진
- Program: 결과 코드
여기까지 보면 단순해 보이지만, 실제로는 한 가지 핵심 질문이 숨어 있다.
“아무 프로그램이나 다 후보로 보면, 이걸 어떻게 찾지?”
이 질문 때문에 SyGuS에는 아주 중요한 아이디어가 들어간다.
SyGuS의 핵심: 두 가지 제약
SyGuS는 단순히 “조건을 만족해라”가 아니라 두 가지 제약을 동시에 요구한다.
1) 어떤 형태로 만들 수 있는가 (Syntax)
먼저, 만들 수 있는 프로그램의 형태를 제한한다.
예를 들어 이런 문법이 있다고 하자:
\[S \rightarrow x \mid S \times S \mid 1 \mid 2 \mid \cdots\]이 말은 곧:
- 변수 x 사용 가능
- 상수 사용 가능
- 곱셈만 가능
- 덧셈, 조건문 등은 사용 불가
즉,
“이 문제는 이 재료로만 풀어라”
라고 제한을 거는 것이다.
이게 중요한 이유는 명확하다. 프로그램의 경우의 수는 사실상 무한하기 때문이다.
문법이 없으면:
- 탐색 공간 = 무한 → 해결 불가능
문법이 있으면:
- 탐색 공간 ↓ → 계산 가능
2) 무엇을 해야 하는가 (Semantics)
이제 프로그램이 어떤 동작을 해야 하는지를 정의한다.
예를 들어:
\[f(1) = 2 \land f(3) = 6\]이건 이렇게 읽으면 된다:
- 입력이 1이면 결과는 2
- 입력이 3이면 결과는 6
이건 단순한 예시처럼 보이지만, 실제로는
“이 프로그램이 반드시 만족해야 하는 조건”
이다.
두 제약을 같이 보면
이제 핵심을 한 번에 보면 이렇게 된다.
- Syntax → 만들 수 있는 프로그램의 범위를 제한
- Semantics → 그 중에서 정답을 고르는 기준
조금 더 직관적으로 보면:
- Syntax = 재료 제한
- Semantics = 맛 조건
둘 중 하나라도 만족 못 하면 실패다.
결국 SyGuS는 어떤 문제인가?
모든 걸 합치면 SyGuS는 이 한 문장으로 정리된다.
“주어진 문법 안에서 만들 수 있는 프로그램 중, 조건을 만족하는 것을 찾아라”
과정을 풀어보면:
- Grammar로 후보 프로그램을 만들고
- 조건을 만족하는지 검사하고
- 맞는 프로그램을 찾을 때까지 반복한다
즉,
1
Generate → Check → Refine
이 구조가 이후 모든 내용의 핵심이 된다.
한 줄 요약
\[\text{SyGuS} = \text{Syntax (형태)} + \text{Semantics (의미)}\]- Syntax는 “어디까지 탐색할지”를 정하고
- Semantics는 “무엇이 정답인지”를 정한다
이 두 개가 합쳐져야 프로그램 합성이 가능해진다.
논리(Logic) — 프로그램 합성의 출발점
SyGuS를 제대로 이해하려면 한 가지를 먼저 받아들여야 한다.
프로그램 합성은 결국 “논리 문제”로 바뀐다
우리는 “이 프로그램이 맞는가?”를 묻고 있지만, 컴퓨터는 이걸 이렇게 바꿔서 생각한다.
“이 조건을 만족하는 값이 존재하는가?”
이 질문을 다루기 위한 가장 기본 도구가 바로 논리(Logic)다. 그중에서도 출발점은 명제 논리(Propositional Logic)이다.
명제 논리란?
명제 논리는 아주 단순하다. 모든 것을 오직 두 가지 값으로만 표현한다.
\[\text{True}, \quad \text{False}\]그리고 이 두 값만 가지고 모든 판단을 한다.
어떻게 표현할까?
명제 논리는 몇 가지 간단한 재료로 이루어진다.
Boolean 변수
\[p, q, r, \dots\]각 변수는 True 또는 False 값을 가진다.
예를 들어:
\[p = \text{True}, \quad q = \text{False}\]논리 연산자
우리는 변수들을 조합해서 식을 만든다.
\[\neg \quad (\text{NOT}), \quad \land \quad (\text{AND}), \quad \lor \quad (\text{OR})\]예를 들어:
\[(\neg p \land T) \lor (q \Rightarrow F)\]이건 하나의 Boolean 식이다. 핵심은 “이 식이 True가 될 수 있냐”이다.
가장 중요한 연산: Implication
다음 연산은 반드시 익숙해져야 한다.
\[a \Rightarrow b\]이 의미는 다음과 같다.
“a가 참이면 b도 참이어야 한다”
언제 거짓이 될까?
이 식이 거짓이 되는 경우는 딱 하나다.
\[a = \text{True}, \quad b = \text{False}\]이 경우만 실패다.
핵심 변환 (매우 중요)
이 연산은 다음과 완전히 동일하다.
\[a \Rightarrow b \equiv \neg a \lor b\]이 식은 이후 SAT, SMT, SyGuS 전부에서 계속 등장한다.
직관적으로 보면:
- \(a\)가 False면 → 전체 True
- \(a\)가 True면 → \(b\)가 True여야 함
왜 논리가 필요한가?
다시 원래 질문으로 돌아가 보자.
“이 프로그램이 조건을 만족하는가?”
이걸 논리로 바꾸면 이렇게 된다.
\[\text{“이 논리식을 True로 만드는 값이 존재하는가?”}\]즉,
- 프로그램 조건 → 논리식
- 프로그램 찾기 → 값 찾기
로 바뀐다.
핵심 감각
명제 논리는 이렇게 이해하면 가장 쉽다.
- 변수 = 스위치 (ON / OFF)
- 논리식 = 스위치 조합 규칙
- 목표 = 조건을 만족하는 조합 찾기
한 줄 정리
\[\text{Propositional Logic} = \text{True/False 기반 논리 시스템}\]그리고 가장 중요한 공식:
\[a \Rightarrow b \equiv \neg a \lor b\]이제 자연스럽게 다음 질문이 나온다.
“그래서 이 논리식이 실제로 참인지 어떻게 판단하지?”
다음 섹션에서는 이 질문에 답하기 위해 Satisfiability (SAT) 개념으로 넘어간다.
SAT — “이 논리식을 참으로 만드는 해가 존재하는가?”
앞에서 명제 논리의 기본 재료를 봤다면, 이제 자연스럽게 이런 질문으로 넘어가게 된다.
그래서 이 논리식이 실제로 참인지 거짓인지는 어떻게 판단할까?
이 질문에 답하는 것이 바로 SAT (Boolean Satisfiability Problem) 이다.
SAT는 한 문장으로 요약하면 다음과 같다.
겉보기에는 짧은 질문이지만, 이 안에는 SAT를 이해하는 데 필요한 핵심 개념들이 모두 들어 있다.
바로 Interpretation, Satisfiability, Validity다.
논리식이 참인지 알려면, 먼저 값을 넣어야 한다
논리식은 그 자체만으로는 아직 참도 거짓도 아니다.
변수에 어떤 값을 넣느냐에 따라 결과가 달라진다.
예를 들어 다음 식을 보자.
\[Q \equiv (\neg p \land T) \lor (\neg q \lor F)\]이 식이 참인지 알려면 \(p, q\)에 값을 넣어봐야 한다.
이렇게 변수에 실제 값을 할당하는 것을 Interpretation(해석) 이라고 한다.
예를 들면,
\[I : \{\, p \mapsto T,\; q \mapsto F \,\}\]는 다음 뜻이다.
- \(p\)는 True
- \(q\)는 False
즉, Interpretation은 논리식을 시험해보기 위한 “값 넣기”라고 생각하면 된다.
식을 참으로 만드는 해석이 있으면 satisfiable 하다
이제 중요한 질문은 이것이다.
어떤 값을 넣었을 때 이 식이 True가 되는가?
논리식을 참으로 만드는 Interpretation을 satisfying interpretation이라고 한다.
수식으로는 이렇게 쓴다.
즉, “Interpretation \(I\)가 논리식 \(Q\)를 만족한다”는 뜻이다.
아까 식을 다시 보자.
\[Q \equiv (\neg p \land T) \lor (\neg q \lor F)\]이 식은 간단히 정리하면 다음과 같다.
\[Q = \neg p \lor \neg q\]이제 값을 넣어보자.
\(p = F,\; q = F\) 이면
\(\neg p = T,\; \neg q = T\) 이므로 전체는 True\(p = F,\; q = T\) 이면
\(\neg p = T\) 이므로 전체는 True\(p = T,\; q = F\) 이면
\(\neg q = T\) 이므로 전체는 True
즉, 이 식은 참이 되는 경우가 여러 개 있다.
이처럼 논리식을 True로 만드는 Interpretation이 하나라도 존재하면, 그 식은 satisfiable 하다고 한다.
수식으로 쓰면:
\[\exists I.\; I \models Q\]이게 바로 SAT의 핵심 질문이다.
“만족하는 해가 하나라도 존재하는가?”
반대로, 어떤 경우에도 참이 안 되면 unsatisfiable 이다
모든 논리식이 satisfiable 한 것은 아니다.
예를 들어 다음 식을 보자.
이 식은 절대 참이 될 수 없다.
- \(p=T\) 이면 \(\neg p=F\)
- \(p=F\) 이면 앞의 \(p=F\)
즉 어떤 값을 넣어도 전체는 False다.
이런 식을 unsatisfiable 하다고 한다.
수식으로 쓰면:
\[\nexists I.\; I \models Q\]즉, 만족하는 Interpretation이 존재하지 않는다.
항상 참인 식은 valid 하다
이번에는 반대로, 어떤 값을 넣어도 항상 참인 식을 보자.
\[Q = p \lor \neg p\]이 식은 \(p\)가 True든 False든 항상 True다.
이런 식을 valid 하다고 한다.
수식으로는:
\[\forall I.\; I \models Q\]즉, 모든 Interpretation에서 참이다.
이제 세 개념의 차이가 분명해진다.
| 개념 | 의미 |
|---|---|
| satisfiable | 참이 되는 경우가 하나라도 있음 |
| valid | 모든 경우에 항상 참 |
| unsatisfiable | 어떤 경우에도 참이 될 수 없음 |
직관적으로 보면 이렇게 이해하면 된다.
- satisfiable → 답이 하나 이상 있다
- valid → 무조건 맞다
- unsatisfiable → 답이 없다
valid와 unsat은 서로 연결된다
여기서 아주 중요한 관계가 하나 있다.
\[Q \text{ is valid } \iff \neg Q \text{ is unsatisfiable}\]이 말은 다음 뜻이다.
- \(Q\)가 항상 참이면
- \(\neg Q\)는 절대 참이 될 수 없다
예를 들어,
\[Q = p \lor \neg p\]는 valid 하다.
그러면 그 부정인
는 어떤 Interpretation에서도 참이 될 수 없으므로 unsatisfiable 이다.
이 관계는 이후 검증, SMT, 합성까지 계속 등장한다.
그래서 SAT는 정확히 무엇인가?
이제 SAT를 다시 정의하면 아주 깔끔해진다.
SAT는 다음 문제다.
주어진 Boolean 논리식 \(Q\)에 대해, \(Q\)를 참으로 만드는 Interpretation이 존재하는가?
수식으로는:
\[\exists I.\; I \models Q \; ?\]존재하면 SAT, 존재하지 않으면 UNSAT다.
즉 SAT는 결국 “조건을 만족하는 조합 찾기 문제”다.
변수들이 스위치처럼 있고, 각 스위치를 어떻게 켜고 꺼야 전체 식이 참이 되는지를 찾는 것이다.
SAT가 왜 중요한가
SAT는 단순한 논리 퍼즐이 아니다.
컴퓨터 과학에서 매우 중요한 문제다.
이유는 단순하다.
많은 문제들이 결국 SAT 형태로 바뀔 수 있기 때문이다.
하드웨어 검증, 소프트웨어 분석, 제약 해결, 자동 정리 증명, 프로그램 합성 같은 문제들이
결국 “조건을 만족하는 해가 존재하는가?”라는 질문으로 환원된다.
즉, SAT는 이후 등장할 더 복잡한 문제들의 출발점이다.
SyGuS와 연결해서 보면
Program synthesis도 겉으로는 “코드를 만드는 문제”처럼 보이지만,
안쪽에서는 결국 이런 질문을 하게 된다.
처음에는 그 후보가 단순한 True/False 값이고,
나중에는 식이나 프로그램 조각으로 확장될 뿐이다.
즉 SAT의 핵심 감각은 이후에도 그대로 유지된다.
- Interpretation → 값 대입
- satisfiable → 가능한 해 존재
- SAT → 그런 해를 찾는 문제
이 흐름을 이해하면 다음 단계인 First-Order Logic과 SMT도 훨씬 자연스럽게 받아들일 수 있다.
마무리
여기까지 오면 프로그램 합성을 바라보는 관점이 완전히 바뀐다.
겉으로는 “코드를 만드는 문제”처럼 보이지만,
실제로는 다음과 같은 형태로 바뀐다.
그리고 이 질문을 다루는 가장 기본적인 형태가 바로 SAT였다.
- 논리식으로 조건을 표현하고
- 그 식을 만족하는 해가 존재하는지 판단하는 것
즉 프로그램 합성의 출발점은
결국 논리와 satisfiability 문제다.
하지만 여기서 한 가지 한계가 분명해진다.
SAT는 True/False만 다룬다
현실의 프로그램은 숫자, 배열, 함수, 비트 연산 등을 포함한다.
즉 더 풍부한 표현력이 필요하다.
다음 글
다음 글에서는 이 한계를 넘어서기 위해 등장하는 개념들을 이어서 본다.
- First-Order Logic (1차 논리)
- SMT (SAT의 확장)
- SMT solver가 실제로 동작하는 방식 (Eager vs Lazy)
- Grammar (탐색 공간 제한)
- SyGuS 문제의 형식적 정의
즉,
SAT에서 시작해서 실제 프로그램 합성(SyGuS)으로 올라가는 과정
을 이어서 다룬다.