LLM2SMT: Building an SMT Solver with Zero Human-Written Code

이 논문은 인간이 작성한 코드가 전혀 없이 LLM 코딩 에이전트가 QF_UF 문제를 해결하는 완전한 SMT 솔버를 구축하고 벤치마크에서 경쟁력 있는 성능을 보였음을 보여주는 사례 연구입니다.

핵심

🤖 "코딩하는 AI 가 스스로 '논리 검사관'을 만들었다?"

(LLM2SMT: 인간이 한 줄의 코드도 쓰지 않은 SMT 솔버 개발 사례)

이 논문은 **"인간이 코딩을 전혀 하지 않았는데, AI 가 스스로 복잡한 논리 문제를 해결하는 소프트웨어를 만들 수 있을까?"**라는 흥미로운 실험에 대한 이야기입니다.

마치 인간이 요리사에게 "요리해 줘"라고만 말하고, 레시피도 주지 않은 채 주방에 내버려 둔 뒤, 그 요리사가 스스로 요리를 만들어내는 상황이라고 상상해 보세요. 이 논문은 바로 그 요리사가 '수학 논리'라는 요리를 완벽하게 해낸 사례입니다.

---

1. 이 실험은 무엇을 했나요? (배경)

일반적으로 AI 는 글을 쓰거나 그림을 그리는 데 능합니다. 하지만 이 연구팀은 AI 가 스스로 '논리 추론 도구 (SMT 솔버)'를 만들 수 있는지 궁금해했습니다.

• 목표: 인간이 코드를 한 줄도 쓰지 않고, AI 가 스스로 QF_UF(논리식과 함수에 대한 논리) 문제를 해결하는 프로그램을 만드는 것.
• 주인공: 'Claude Code'라는 AI 에이전트.
• 결과: AI 는 스스로 코드를 짜고, 버그를 고치고, 심지어 증명까지 하는 완전한 프로그램을 완성했습니다.

2. 어떻게 만들었나요? (과정과 비유)

AI 는 처음부터 완벽하지 않았습니다. 마치 새로 입사한 천재 신입 사원처럼, 큰 그림은 알지만 세부적인 실수를 반복했습니다. 연구팀은 다음과 같은 '코칭'을 해줬습니다.

① "너는 코딩만 하지 말고, '감시관'도 만들어줘"

AI 는 처음에 논리 연결詞 (AND, OR 등) 를 제대로 처리하지 못했습니다. 연구팀은 "논리 규칙을 잘 지켜야 해"라고 가르쳤고, AI 는 스스로 수정했습니다.

• 비유: 요리사가 소금과 설탕을 헷갈려서 요리를 망쳤을 때, "소금은 짠 거고 설탕은 단 거야"라고 알려주니 바로 고친 셈입니다.

② "자꾸 멈추는 게 아니라, '타임아웃'을 걸어줘"

AI 가 만든 프로그램은 가끔 무한 루프에 빠져 멈추지 않는 경우가 있었습니다. 연구팀은 AI 에게 "만약 180 초 안에 안 끝나면 강제로 멈춰!"라는 규칙을 세웠습니다.

• 비유: 요리사가 불을 끄지 않고 계속 끓이다가 냄비가 타버리는 것을 막기 위해, "30 분 지나면 자동으로 가스 밸브를 잠가"라고 설정한 것과 같습니다.

③ "복잡한 문제를 '미리 정리'해줘 (프리프로세싱)"

특히 어려운 문제 (다이아몬드 문제) 가 있었습니다. AI 는 이걸 해결하기 위해 스스로 새로운 전략을 생각해냈습니다.

• 상황: "A=B 이거나 B=C 이다"라는 식의 복잡한 조건이 있을 때, AI 는 "아, 그럼 A=C 라는 공통점을 미리 찾아서 문제 자체를 단순화하자!"라고 생각했습니다.
• 결과: 이 전략 덕분에 AI 는 인간이 만든 기존 프로그램들보다 훨씬 빠르게 문제를 해결했습니다.

3. 가장 어려운 부분: "증명서" 만들기

AI 가 문제를 풀고 "해결했다!"라고 말했을 때, 우리는 그 답이 맞는지 어떻게 알 수 있을까요? 연구팀은 AI 에게 **Lean(린)**이라는 언어로 '증명서'를 작성하게 했습니다.

• 도전: AI 는 논리 문제를 푸는 것은 잘했지만, 그 과정을 수학적으로 증명하는 것은 매우 어려워했습니다. 마치 수학 문제를 풀기는 잘하지만, 풀이 과정을 시험지 답안지에 깔끔하게 적어내는 데 서툰 학생과 같았습니다.
• 해결: 연구팀이 "이런 식으로 증명해"라고 구체적인 예시를 보여줬더니, AI 는 그 패턴을 학습해서 결국 증명서를 만들어냈습니다.

4. 결과는 어땠나요? (성능)

이 AI 가 만든 프로그램은 세계적인 유명 프로그램 (Z3, cvc5) 과 경쟁해 볼 만큼 매우 강력했습니다.

• 성공률: 수천 개의 테스트 문제 중 대부분을 해결했습니다.
• 특이점: AI 가 스스로 '예비 전략 (프리프로세싱)'을 추가했을 때 성능이 가장 좋았습니다.
• 한계: 증명서를 만들 때는 가끔 실패하거나 시간이 너무 오래 걸리기도 했지만, 틀린 증명을 내놓지는 않았습니다. (안전성 확보)

5. 이 실험이 우리에게 주는 교훈 (핵심 메시지)

이 논문은 AI 가 인간을 대체할 수 있다는 것보다, **"AI 가 인간과 함께 일할 때 얼마나 강력한 도구가 될 수 있는지"**를 보여줍니다.

1. 완벽하지 않아도 된다: AI 는 처음부터 완벽하지 않습니다. 하지만 실수를 지적해주고, 구체적인 예시를 보여주면 스스로 배우고 고칩니다.
2. 규칙이 중요하다: AI 에게 "시간 제한을 지켜라", "테스트를 해라" 같은 명확한 규칙을 주면 훨씬 안정적으로 일합니다.
3. 창의성은 AI 에게도 있다: AI 는 단순히 지시받은 대로만 하는 게 아니라, 복잡한 문제를 해결하기 위해 스스로 새로운 전략 (다이아몬드 문제 해결법) 을 고안해내기도 했습니다.

🎯 한 줄 요약

"인간이 코딩을 전혀 하지 않았는데, AI 가 스스로 '논리 검사관'이 되어 복잡한 수학 문제를 해결하고 증명까지 해낸 놀라운 실험. AI 는 아직 완벽하지 않지만, 적절한 가이드만 있다면 인간을 능가하는 도구가 될 수 있다."

이 연구는 미래에 소프트웨어 개발자가 AI 와 협력하여, 인간이 상상하지 못했던 복잡한 논리 도구들을 함께 만들어갈 수 있는 가능성을 보여줍니다.

기술 요약

1. 문제 정의 (Problem)

대형 언어 모델 (LLM) 이 소프트웨어를 작성할 수 있다는 사실은 널리 알려져 있지만, LLM 이 스스로 추론 (reasoning) 을 수행하는 소프트웨어를 작성할 수 있는가에 대한 연구는 거의 이루어지지 않았습니다. 특히, 자동 추론 (Automated Reasoning) 분야는 논리적 정확성이 매우 중요하며, 사소한 오류가 치명적인 결과로 이어질 수 있어 LLM 의 적용에 대한 회의론이 존재합니다.

이 논문은 다음과 같은 핵심 질문을 던집니다:

"인간이 작성한 코드가 전혀 없이, LLM 코딩 에이전트가 자동 추론 도구 (SMT 솔버) 를 개발할 수 있는가?"

2. 방법론 (Methodology)

저자들은 인간이 작성한 코드가 전혀 없는 상태에서, Claude Code(Sonnet 4.6 모델) 를 사용하여 QF_UF(Quantifier-Free Uninterpreted Functions, 정량화 없는 비해석 함수) 이론을 다루는 완전한 DPLL(T) 스타일의 SMT 솔버를 구축했습니다.

주요 개발 과정 및 기술적 접근 방식은 다음과 같습니다:

• 프로젝트 설정 및 아키텍처:

  • 언어: C++20, 빌드 도구: CMake.
  • 파싱: ANTLR 및 SMT-LIB2 문법 사용.
  • SAT 솔버: 초기에는 에이전트가 자체적으로 구현했으나, 이후 CaDiCaL을 IPASIR-UP 인터페이스를 통해 통합하도록 명시적 프롬프트로 지시.
  • 핵심 알고리즘: Nieuwenhuis-Oliveras 합동 폐쇄 (Congruence Closure) 알고리즘 구현.
  • 증명 생성: Lean (상호작용 정리 증명기) 을 사용하여 불만족 (Unsatisfiable) 인 인스턴스에 대한 증명을 생성.

• 디버깅 및 테스트 전략 (Human-in-the-loop):

  • 인간은 직접 코드를 작성하지 않았으나, 에이전트가 생성한 코드의 구조적 디버깅 지원을 제공했습니다.
  • 퍼징 (Fuzzing) 및 델타 디버깅 (Delta-debugging): 에이전트가 스스로 버그를 수정할 수 있도록 무작위 공식 생성기와 기준 솔버 (Reference Solver) 와의 차등 테스트 스크립트를 생성하도록 지시.
  • 타임아웃 관리: 에이전트가 무한 루프에 빠지는 것을 방지하기 위해 솔버 실행 시 항상 timeout 명령어를 사용하도록 영구 지시사항에 포함.
  • 구체적인 예시 제공: 에이전트가 논리적 오류 (예: 부울을 명제와 항으로 혼동하는 문제) 를 이해하지 못할 때, 구체적인 실패 사례와 수정 예시를 제공하여 성능을 개선.

• 전처리 (Preprocessing) 및 최적화:

  • 에이전트는 단위 전파 (unit propagation) 및 단순화 기법을 구현하도록 지시받았습니다.
  • 특히, Equational Diamond 문제 (지수적 복잡도를 유발하는 특정 형태의 논리식) 를 해결하기 위해 에이전트가 스스로 전처리 기법을 고안해냈습니다. 이는 분기별 합동 폐쇄를 계산하여 공통된 결과를 추출하는 방식이었습니다.

• 인증 (Certification):

  • 만족 가능한 (SAT) 경우: 생성된 모델을 SMT 문제로 인코딩하여 기준 솔버로 검증.
  • 불만족 가능한 (UNSAT) 경우: Lean으로 증명을 생성. grind (합동 폐쇄 검증) 와 bv_decide (명제 논리 검증) 도구를 활용하여 증명을 자동화했습니다.

3. 주요 기여 (Key Contributions)

1. Zero Human-Written Code SMT 솔버: 인간이 코드를 한 줄도 작성하지 않고, LLM 에이전트만으로 DPLL(T) 스타일의 SMT 솔버를 구축한 최초의 사례 중 하나입니다.
2. Nieuwenhuis-Oliveras 알고리즘 구현: QF_UF 이론을 위한 합동 폐쇄 알고리즘을 성공적으로 구현하고, 이를 Lean 증명으로 연결했습니다.
3. 자율적 전처리 기술 개발: 에이전트가 복잡한 "Diamond 문제"를 해결하기 위해 지수적 행동을 피하는 전처리 기법을 스스로 설계하고 구현했습니다.
4. LLM 기반 자동 추론 도구 개발의 가능성 입증: 체계적인 퍼징, 구체적인 예시, 리소스 제한 등의 '스캐폴딩 (Scaffolding)'이 있다면 LLM 이 복잡한 자동 추론 도구를 개발할 수 있음을 보여주었습니다.

4. 실험 결과 (Results)

저자들은 SMT-LIB 벤치마크 (QF_UF) 를 사용하여 개발된 솔버를 Z3 및 cvc5와 비교 평가했습니다.

• 성능 비교:

  • 해결된 인스턴스 수: LLM2SMT 는 7,468 개를 해결하여 Z3(7,500 개) 및 cvc5(7,494 개) 와 거의 유사한 성능을 보였습니다.
  • 속도: 이론 전파 (Theory Propagation) 를 비활성화한 버전이 오히려 벤치마크에서 더 빠른 경향을 보였으며, 이는 전파 오버헤드가 일부 문제에서 불필요했기 때문입니다.
  • 전처리 효과: 에이전트가 개발한 전처리 기법 (Diamond 문제 해결 등) 을 적용했을 때, 특정 문제에서 해결 시간이 획기적으로 단축되었습니다.

• 증명 생성 (Certification) 결과:

  • Lean 증명을 생성하는 과정은 가장 어려운 과제였습니다. 에이전트는 증명의 복잡도를 이해하는 데 어려움을 겪었으며, 많은 타임아웃이 발생했습니다.
  • 그러나 잘못된 증명 (Erroneous proofs) 은 하나도 발견되지 않았습니다. 즉, 생성된 증명은 논리적으로 정확했습니다.

5. 의의 및 결론 (Significance & Conclusion)

이 연구는 다음과 같은 중요한 시사점을 제공합니다:

• LLM 의 능력과 한계: LLM 은 과학적 논문을 기반으로 새로운 기법을 구현하고, 구체적인 실패 사례를 통해 스스로 디버깅할 수 있는 능력이 있습니다. 하지만 정확성 (Correctness) 은 보장되지 않으며, 인간이 구체적인 예시와 체계적인 테스트를 제공해야만 신뢰할 수 있는 도구를 만들 수 있습니다.
• "Jagged Intelligence" (불규칙한 지능): LLM 은 복잡한 추론을 잘 수행하면서도, s = s를 true 로 단순화하는 것과 같은 매우 단순한 작업에서 실수할 수 있습니다. 이는 자동 추론 도구 개발 시 지속적인 검증이 필요함을 의미합니다.
• 미래 전망: 인간이 코드를 직접 작성하지 않고도 LLM 이 자동 추론 도구를 개발할 수 있다는 점은, 새로운 알고리즘의 빠른 실험과 통합에 혁신적인 가능성을 제시합니다. 다만, 증명 생성과 같은 고차원적인 작업에서는 여전히 인간의 가이드가 필수적입니다.

요약하자면, 이 논문은 LLM 이 인간 개입 없이도 경쟁력 있는 SMT 솔버를 구축할 수 있음을 증명했으나, 그 과정에서 체계적인 검증 체계와 인간의 전략적 개입이 필수적임을 강조했습니다.