[Program Synthesis #11] 실제 시스템으로 보는 Synthesis: FlashFill, Sketch, STOKE
Program Synthesis 시리즈 11편 – FlashFill, Sketch, STOKE를 통해 실제 시스템이 다양한 synthesis 기법을 어떻게 결합하는지 이해하기
들어가며 — 이론이 실제 시스템이 되는 순간
지금까지 우리는 Program Synthesis를 다양한 관점에서 살펴봤다.
- Search → 어떤 프로그램을 탐색할 것인가
- Representation → 프로그램 공간을 어떻게 표현할 것인가
- Stochastic → 확률적으로 탐색하는 방법
- Constraint → 논리적으로 문제를 해결하는 방법
이 모든 접근은 각각 강력하지만,
실제 시스템은 하나의 방법만 사용하지 않는다
현실의 Program Synthesis 시스템은
이 모든 요소를 조합해서 만들어진다.
- 구조를 제한하고 (Sketch / Grammar)
- 공간을 압축하고 (VSA / DAG)
- 탐색을 최적화하고 (Search strategy)
- constraint로 검증한다 (SMT / CEGIS)
즉 synthesis는 이제
하나의 알고리즘이 아니라 시스템 설계 문제
다.
이 글에서는 대표적인 세 가지 시스템을 통해
이 아이디어가 실제로 어떻게 구현되는지 살펴본다.
- FlashFill → PBE 기반 synthesis
- Sketch → constraint-based synthesis
- STOKE → stochastic superoptimization
이 시스템들을 비교하면,
각 접근이 어디서 강하고, 어떻게 결합되는지
명확하게 드러난다.
FlashFill — Programming by Example의 대표 시스템
FlashFill은 Microsoft Excel에 실제로 들어간
가장 유명한 Program Synthesis 시스템 중 하나다.
문제 설정
FlashFill은 다음과 같은 문제를 해결한다.
몇 개의 input-output 예제가 주어졌을 때,
그 변환을 수행하는 프로그램을 생성하라
예:
1
2
input: "john doe"
output: "J. Doe"
사용자는 몇 개의 예제만 제공하고,
나머지는 시스템이 자동으로 채운다.
핵심 아이디어
FlashFill의 핵심은 다음 세 가지의 결합이다.
- DSL (도메인 특화 언어)
- VSA (Version Space Algebra)
- Ranking (우선순위 모델)
DSL — 구조 제한
FlashFill은 일반적인 프로그램이 아니라
문자열 변환에 특화된 DSL을 사용한다.
예:
1
Concat(Substring(...), Constant(...))
이렇게 구조를 제한하면
search space가 크게 줄어든다
VSA — 공간 압축
FlashFill은 가능한 프로그램을 하나씩 나열하지 않는다.
대신:
가능한 프로그램 집합을 VSA로 압축해서 표현한다
즉:
- 수많은 프로그램을 하나의 DAG로 표현
- 공통 구조 공유
Ranking — 가장 자연스러운 프로그램 선택
여러 후보가 있을 때, FlashFill은 ranking을 사용한다.
예:
- 더 짧은 프로그램
- 더 일반적인 패턴
- 더 “자연스러운” 구조
즉,
확률적 모델 + 휴리스틱
전체 구조
FlashFill은 다음과 같이 동작한다.
- DSL로 search space 제한
- VSA로 후보 압축
- ranking으로 최종 선택
즉,
Representation + Search + Heuristic의 결합
Sketch — Constraint-Based Synthesis의 대표 시스템
Sketch는 Constraint-Based Synthesis를 대표하는 시스템이다.
문제 설정
Sketch는 다음과 같은 형태의 문제를 푼다.
일부가 비어있는 프로그램을 완성하라
예:
1
f(x) = x + ??
여기서 ??는 hole이다.
핵심 아이디어
Sketch의 핵심은 다음과 같다.
- 프로그램 구조는 사용자가 제공
- hole을 변수로 변환
- constraint solving으로 값 결정
Constraint Encoding
Sketch는 프로그램을 constraint로 변환한다.
예:
1
f(x) = x + c
그리고 specification:
1
2
f(1) = 2
f(2) = 3
→ constraint:
\[c = 1\]CEGIS Loop
Sketch는 단순 solver 호출로 끝나지 않는다.
다음 과정을 반복한다.
- 예제 기반 constraint 생성
- solver로 후보 생성
- counterexample로 refinement
즉,
Constraint + Iteration (CEGIS)
특징
- 강한 correctness 보장
- search 대신 solving
- sketch 품질에 의존
전체 구조
Sketch는 다음과 같이 볼 수 있다.
- Structure → 사람이 제공
- Constraint → 문제 정의
- Solver → 해 결정
즉,
논리 기반 synthesis
Sketch — Constraint-Based Synthesis의 대표 시스템
Sketch는 Constraint-Based Synthesis를 대표하는 시스템이다.
문제 설정
Sketch는 다음과 같은 형태의 문제를 푼다.
일부가 비어있는 프로그램을 완성하라
예:
1
f(x) = x + ??
여기서 ??는 hole이다.
핵심 아이디어
Sketch의 핵심은 다음과 같다.
- 프로그램 구조는 사용자가 제공
- hole을 변수로 변환
- constraint solving으로 값 결정
Constraint Encoding
Sketch는 프로그램을 constraint로 변환한다.
예:
1
f(x) = x + c
그리고 specification:
1
2
f(1) = 2
f(2) = 3
→ constraint:
\[c = 1\]CEGIS Loop
Sketch는 단순 solver 호출로 끝나지 않는다.
다음 과정을 반복한다.
- 예제 기반 constraint 생성
- solver로 후보 생성
- counterexample로 refinement
즉,
Constraint + Iteration (CEGIS)
특징
- 강한 correctness 보장
- search 대신 solving
- sketch 품질에 의존
전체 구조
Sketch는 다음과 같이 볼 수 있다.
- Structure → 사람이 제공
- Constraint → 문제 정의
- Solver → 해 결정
즉,
논리 기반 synthesis
세 시스템의 비교 — 서로 다른 설계 철학
이제 세 시스템을 비교해보자.
접근 방식
- FlashFill → PBE + VSA + Ranking
- Sketch → Constraint + Solver + CEGIS
- STOKE → Stochastic Search
핵심 차이
- FlashFill → 구조적 압축 + 휴리스틱
- Sketch → 논리 기반 해결
- STOKE → 확률적 탐색
문제 유형
- FlashFill → 문자열 변환
- Sketch → 일반적인 synthesis
- STOKE → 성능 최적화
중요한 관점
이 세 시스템은 서로 경쟁하는 것이 아니다.
서로 다른 문제를 해결하기 위해 설계된 것
즉,
representation + search + constraint의 조합이 다르다
정리 — Program Synthesis는 시스템 설계다
지금까지 FlashFill, Sketch, STOKE를 통해
실제 Program Synthesis 시스템을 살펴봤다.
이 시스템들은 겉으로는 다르지만,
공통된 구조를 가진다.
- search를 어떻게 할 것인가
- representation을 어떻게 할 것인가
- constraint를 어떻게 적용할 것인가
즉 synthesis는 더 이상
하나의 알고리즘 문제가 아니다
대신 다음과 같은 문제다.
여러 요소를 어떻게 결합할 것인가
이 관점에서 보면,
- FlashFill은 representation 중심
- Sketch는 constraint 중심
- STOKE는 search 중심
각각 다른 축을 강조한다.
전체 시리즈를 돌아보며
이 시리즈를 통해 우리는 다음을 살펴봤다.
- brute-force 탐색에서 시작해
- 구조와 확률을 도입하고
- 표현 방식을 바꾸며
- 논리와 결합하고
- 실제 시스템으로 확장했다
이 흐름은 하나의 메시지를 보여준다.
Program Synthesis는 점점 더
구조화된 문제 해결 방식으로 발전하고 있다
마지막 관점
이제 synthesis는 다음과 같이 볼 수 있다.
- 프로그램을 작성하는 것이 아니라
- 프로그램을 정의하고, 탐색하고, 구성하는 과정
즉,
Programming → Synthesis
이 시리즈는 여기서 마무리되지만,
이 분야는 여전히 빠르게 발전하고 있다.
- ML 기반 synthesis
- LLM과의 결합
- 실제 산업 적용
이제 남은 것은 하나다.
이 아이디어들을 직접 구현해보는 것