이 논문은 LTL 반응형 합성, 구문 유도 합성, 분산 프로토콜 합성, 재귀 함수 합성 등 여러 도메인에서 최신 심볼릭 도구들이 320 억 파라미터 Qwen 과 GPT-5 와 같은 LLM 보다 더 많은 벤치마크를 해결하고 실행 시간 측면에서도 우월하거나 동등한 성능을 보인다고 결론짓습니다.
이 논문은 **"인공지능 (LLM) 이 정말로 복잡한 프로그램을 스스로 만들어낼 수 있을까?"**라는 질문에 답하기 위해 진행된 실험 결과입니다.
저희는 최신 AI 모델 (Qwen, GPT-5) 과 전통적인 '수학적 도구' (Symbolic Tools) 를 서로 비교했습니다. 마치 **재능 있는 요리사 (AI)**와 **정밀한 자동화 로봇 (수학적 도구)**이 어떤 상황에서 더 맛있는 요리를 잘 만들어내는지 경쟁시켜 본 셈이죠.
이 연구의 핵심 내용을 쉬운 비유로 설명해 드릴게요.
🍳 실험 상황: "요리 대회"
연구자들은 4 가지 다른 종류의 '요리 (프로그램 만들기)' 대회를 열었습니다.
LTL 반응형 합성: "이 신호가 오면 저렇게 반응해"라는 복잡한 규칙을 지키는 자동화 기계 만들기.
구문 유도 합성 (SyGuS): 정해진 문법 (레시피) 을 꼭 지키면서 특정 기능을 하는 함수 만들기.
분산 프로토콜 합성: 여러 컴퓨터가 서로 소통할 때 생길 수 있는 오류를 막는 통신 규칙 만들기.
재귀 함수 합성: 자기 자신을 호출하며 문제를 해결하는 복잡한 알고리즘 만들기.
이 대회에는 두 팀이 참여했습니다.
팀 AI (Qwen, GPT-5): 창의적이고 빠르지만, 실수를 할 수도 있는 '재능 있는 요리사'.
팀 로봇 (Symbolic Tools): 느릴 수 있지만, 절대 실수하지 않고 수학적으로 완벽함을 보장하는 '정밀한 자동화 로봇'.
🏆 경쟁 결과: 누가 이겼을까?
결과는 상황에 따라 달랐지만, 전반적으로 '로봇 (수학적 도구)'이 더 강력했습니다.
1. 정확도 (얼마나 많은 문제를 해결했나?)
로봇의 승리: 모든 분야에서 로봇이 더 많은 문제를 해결했습니다. 특히 1 번 (LTL) 분야에서는 로봇이 AI 를 압도적으로 이겼습니다. 로봇은 "수학적으로 증명된 정답"만 내놓기 때문입니다.
AI 의 활약: 로봇이 해결하지 못한 몇몇 어려운 문제들을 AI 가 해결하기도 했습니다. AI 는 때로 로봇이 생각지 못한 창의적인 방법을 찾아내기도 했습니다.
결론: 로봇이 더 많았지만, AI 가 로봇이 못 한 일을 해낸 경우도 있어 둘을 같이 쓰는 것이 가장 좋습니다. (예: 로봇이 먼저 시도하고, 안 되면 AI 에게 맡기는 식)
2. 속도 (얼마나 빨리 요리했나?)
로봇의 압도적 승리: 로봇은 AI 보다 훨씬 빨랐습니다.
비유: AI 는 "생각을 많이 해서" (Token 을 많이 쓰며) 정답을 찾다가 시간이 걸립니다. 반면 로봇은 "계산기처럼" 정해진 경로를 따라 빠르게 정답을 찾아냅니다.
흥미로운 점은 AI 가 더 강력한 컴퓨터 (GPU) 에서 돌아갔음에도 불구하고, 로봇이 CPU 에서 돌아갔는데도 속도가 더 빨랐다는 것입니다.
3. AI 의 약점: "같은 실수를 반복하다"
AI 의 버릇: AI 는 틀린 답을 내면, 다시 물어봐도 똑같은 틀린 답을 반복해서 내놓는 경우가 많았습니다. 마치 "이제야 알았어!"라고 외치며 같은 실수를 반복하는 사람처럼요.
로봇의 장점: 로봇은 같은 답을 두 번 내지 않도록 설계되어 있어, 실수 없이 모든 가능성을 체계적으로 탐색합니다.
4. 문법과 형식 (레시피 지키기)
AI 의 고민: AI 는 내용은 잘 만들어내지만, 정해진 문법 (코드 형식) 을 지키지 못해 실패하는 경우가 많았습니다. 마치 요리는 맛있는데 접시에 담는 법을 몰라 바닥에 흘리는 경우죠.
로봇의 강점: 로봇은 처음부터 문법 오류가 없는 코드를 만들어냅니다.
💡 핵심 교훈: "AI vs 로봇, 둘 다 필요해!"
이 연구는 AI 가 프로그램 합성 (자동으로 코드 만들기) 을 할 수 있다고 말하지만, 아직은 완벽하지 않다는 것을 보여줍니다.
AI 는 "창의적인 아이디어"를 줍니다. 로봇이 못 찾는 새로운 길을 찾아낼 수 있습니다.
로봇은 "확실한 정답"을 줍니다. 빠르고 정확하며, 실수가 없습니다.
최선의 전략은? 이 두 기술을 섞어서 쓰는 것입니다. AI 가 여러 가지 아이디어를 내면, 로봇이 그중에서 맞는 것을 골라 검증하는 방식입니다. 이를 '하이브리드 (Hybrid)' 또는 '뉴로심볼릭 (Neurosymbolic)' 접근법이라고 합니다.
📝 한 줄 요약
"AI 는 재능 있는 예술가지만, 아직은 실수가 많고 느립니다. 반면 수학적 도구는 느릴 수 있지만 절대 실수하지 않는 정밀한 장인입니다. 가장 완벽한 프로그램을 만들려면, 이 두 사람을 한 팀으로 묶어야 합니다."
논문 요약: Can LLMs Perform Synthesis? (LLM 은 합성 (Synthesis) 을 수행할 수 있는가?)
이 논문은 대형 언어 모델 (LLM) 이 형식 명세 (formal specifications) 에서 프로그램을 자동 생성하는 '프로그램 합성 (Program Synthesis)' 작업에서 기존의 심볼릭 (symbolic) 도구들과 어떻게 비교되는지 평가한 연구입니다. 저자들은 LLM 이 합성 문제를 해결할 수 있는지, 그리고 그 성능이 기존 도구들을 대체할 수 있을지, 아니면 보완할 수 있을지 분석했습니다.
1. 연구 문제 (Problem)
프로그램 합성의 목표는 주어진 정합성 명세 (correctness specification) 를 만족하는 시스템을 자동으로 생성하는 것입니다. 최근 LLM 이 코드 생성 분야에서 큰 성과를 거두면서, **"LLM 이 형식 명세 기반의 프로그램 합성 작업을 수행할 수 있는가?"**라는 질문이 제기되었습니다. 저자들은 LLM 이 단순히 코드를 작성하는 것을 넘어, 논리 명세 (LTL, TLA+, SyGuS 등) 를 입력받아 이를 만족하는 정확한 프로그램을 생성할 수 있는지, 그리고 기존에 개발된 최첨단 심볼릭 합성 도구들과 비교하여 어떤 위치를 차지하는지 실증적으로 평가하고자 했습니다.
2. 방법론 (Methodology)
2.1 평가 영역 (Synthesis Domains)
연구는 네 가지 주요 합성 도메인에서 수행되었습니다:
LTL 반응형 합성 (LTL Reactive Synthesis): 선형 시간 논리 (LTL) 명세를 만족하는 유한 상태 기계 (FSM) 를 생성.
구문 유도 합성 (Syntax-Guided Synthesis, SyGuS): 주어진 문법 (Grammar) 과 명세를 만족하는 프로그램 생성.
분산 프로토콜 합성 (Distributed Protocol Synthesis): TLA+ 스케치 (Sketch) 를 기반으로 프로토콜 완성.
재귀 함수 합성 (Recursive Program Synthesis): ACL2s 언어로 재귀 함수 스케치를 완성하여 명세 만족.
Qwen-2.5-Coder-32B: 오픈소스 모델 (NVIDIA H200 GPU 에서 실행).
GPT-5: 폐쇄형 최첨단 모델 (OpenAI API 사용).
2.3 실험 설정 및 공정성 (Fairness)
검증기 결합 (Verifier Coupling): LLM 은 확률적 출력을 생성하므로, 생성된 코드가 명세를 만족하는지 확인하기 위해 심볼릭 검증기 (Model Checker, SMT Solver 등) 를 결합했습니다.
반복 시도 (Iterate-LLM-until-solution-or-timeout, ILST):
Qwen: 10 분 (또는 15 분) 타임아웃 내에 정답을 찾을 때까지 검증기를 통해 검증하고 실패 시 다시 요청 (Reprompt) 하는 루프를 실행합니다. 단, 이전 실패에 대한 피드백 (Counterexample) 은 제공하지 않습니다 (Neurosymbolic 접근이 아닌 'LLM 자체 능력' 평가 목적).
GPT-5: 각 벤치마크당 단 한 번만 쿼리합니다. (GPT-5 의 강력한 성능과 하드웨어를 고려하여 반복 실행을 제한하고, 심볼릭 도구 및 Qwen 과의 공정한 시간 자원 배분을 위해 단일 시도 방식을 채택했습니다.)
하드웨어: 심볼릭 도구는 CPU 에서, LLM 은 GPU (Qwen) 또는 클라우드 API (GPT-5) 에서 실행되었습니다.
3. 주요 결과 (Key Results)
3.1 벤치마크 해결 능력 (Solved Benchmarks)
전체적인 경향: 모든 도메인에서 심볼릭 도구가 Qwen 보다 더 많은 벤치마크를 해결했습니다.
LTL 합성: 심볼릭 도구 (ltlsynt) 가 압도적으로 성능이 좋았습니다. GPT-5 는 심볼릭 도구와 비슷하거나 약간 못 미치는 수준이었으나, Qwen 은 크게 뒤처졌습니다.
SyGuS 및 기타 도메인: GPT-5 는 심볼릭 도구 (cvc5 등) 와 거의 동등하거나 일부 벤치마크에서 더 좋은 성능을 보였습니다. Qwen 은 GPT-5 보다 성능이 낮았습니다.
상호 보완성: LLM 이 해결하고 심볼릭 도구가 실패한 경우, 그리고 그 반대의 경우가 모두 존재했습니다. 이는 두 접근법을 병렬로 실행하는 '포트폴리오 (Portfolio)' 방식의 필요성을 시사합니다.
3.2 실행 시간 (Execution Time)
심볼릭 도구의 우위: 모든 도메인에서 심볼릭 도구가 GPT-5 보다 매우 빠르거나 (LTL, SyGuS 에서 1~2 차수 이상 빠름), 최소한 동등한 수준이었습니다.
하드웨어 역설: LLM 은 훨씬 더 강력한 하드웨어 (GPU, 클라우드) 에서 실행되었음에도 불구하고, 심볼릭 도구의 CPU 기반 실행 시간보다 느렸습니다. 이는 LLM 이 합성 문제를 해결하는 데 있어 계산 효율성이 낮음을 의미합니다.
3.3 LLM 의 한계 및 특징
반복 오류: Qwen 은 ILST 루프 내에서 동일한 잘못된 솔루션을 반복적으로 생성하는 경향이 있었습니다 (피드백이 없기 때문).
구문 오류: GPT-5 는 대부분의 도메인에서 구문 (Syntax) 과 문법 (Grammar) 준수를 잘 지켰으나, Qwen 은 구문 오류가 빈번했습니다. 특히 재귀 프로그램 합성 도메인에서 Qwen 의 실패 사례 중 절반 이상이 구문 문제였습니다.
비용: GPT-5 실험은 토큰 비용이 발생했으나, 전체적으로 합리적인 수준이었습니다.
4. 주요 기여 (Key Contributions)
포괄적인 비교 평가: LLM 과 심볼릭 도구를 네 가지 서로 다른 합성 도메인에서 체계적으로 비교한 최초의 연구 중 하나입니다.
공정한 실험 설계: 하드웨어 차이와 LLM 의 반복 실행 전략을 고려하여, 가능한 한 공정한 비교 기준 (타임아웃, 검증 프로세스) 을 마련했습니다.
실용적 통찰: LLM 이 'Out-of-the-box' 상태로 합성 문제를 해결하는 데 한계가 있음을 보여주었으며, 심볼릭 도구의 정확성과 효율성을 대체하기보다는 보조 도구나 포트폴리오 접근법의 일부로 통합되어야 함을 시사했습니다.
데이터 및 벤치마크: 다양한 도메인에서의 상세한 성능 데이터 (해결 수, 시간, 토큰 비용, 반복 횟수 등) 를 공개했습니다.
5. 의의 및 결론 (Significance & Conclusion)
이 논문은 **"LLM 은 현재로서는 심볼릭 합성 도구를 완전히 대체할 수 없다"**는 결론을 내립니다.
정확성과 속도: 심볼릭 도구는 'Correctness by Construction'을 보장하며, 합성 문제 해결 속도와 성공률 면에서 LLM 을 압도합니다.
LLM 의 역할: LLM 은 심볼릭 도구가 실패하는 일부 난이도 높은 벤치마크를 해결할 수 있는 잠재력을 보였으나, 구문 오류와 반복적인 실패로 인해 신뢰성이 떨어집니다.
미래 방향: LLM 을 합성 파이프라인에 통합할 때는 단순한 코드 생성자가 아니라, **검증기를 통한 반복 검증 (Iterative Verification)**이나 심볼릭 도구를 보조하는 하이브리드 (Neurosymbolic) 접근법이 필수적입니다.
결론적으로, LLM 은 프로그램 합성 분야에서 유망한 도구이지만, 형식적 정확성과 효율성이 요구되는 엄격한 합성 작업에서는 여전히 심볼릭 도구가 주류이며, LLM 은 이를 보완하는 역할을 해야 함을 시사합니다.