[논문] Goedel-Architect: 청사진 생성·정제로 형식 정리 증명 간소화
개요
우리는 Lean 4에서 형식적 정리 증명을 위한 에이전시 프레임워크인 Goedel‑Architect를 소개한다. 이 프레임워크는 청사진(blueprint) 생성 및 정제에 초점을 맞춘다. 청사진이란 주요 정리까지 이르는 정의와 보조정리(lemma)들의 의존성 그래프를 의미한다. 먼저 Goedel‑Architect는 형식적으로 기술된 정의와 보조정리, 그리고 선언된 의존성을 포함하는 청사진을 생성한다. 이 청사진은 선택적으로 자연어 증명에 의해 가이드될 수 있다. 이후 도구가 장착된 Lean 증명기 컴포넌트가 각 열린 보조정리 노드를 관련 의존성을 활용해 병렬로 닫는다. 실패한 보조정리는 전역 청사진의 정제를 촉진한다. 이 전략은 재귀적 보조정리 분해를 사용하는 기존 주류 접근법과 대조적이며, 후자는 종종 막다른 전략에 비효율적으로 반복한다. 백본으로 오픈‑weight DeepSeek‑V4‑Flash (284B‑A13B)를 사용한 결과, Goedel‑Architect는 MiniF2F‑test에서 pass@1 99.2 %, PutnamBench에서 **pass@1 75.6 %**를 달성한다. 더 어려운 문제들에 대해 초기 청사진을 자연어 증명으로 시드하면, 추가로 MiniF2F‑test의 남은 두 문제를 모두 해결해 **100 %**에 도달하고, PutnamBench를 88.8 % (597/672) 로 끌어올린다. 또한 IMO 2025에서 4/6, Putnam 2025에서 11/12, USAMO 2026에서 3/6 문제를 해결한다. 이는 동일한 오픈소스 파이프라인 대비 최대 500배 저렴한 비용으로 달성한 최첨단 성능을 의미한다.
주요 기여
이 논문은 다음 분야의 연구를 제시한다:
- cs.AI
방법론
자세한 방법론은 전체 논문을 참고하시기 바란다.
실용적 함의
본 연구는 cs.AI 분야의 발전에 기여한다.
저자
- Jui-Hui Chung
- Ziyang Cai
- Zihao Li
- Qishuo Yin
- Rohit Agarwal
- Simon Park
- Rodrigo Porto
- Narutatsu Ri
- Ziran Yang
- Shange Tang
- Xingyu Dang
- Hongzhou Lin
- Mengdi Wang
- Danqi Chen
- Chi Jin
- Liam H Fowl
- Sanjeev Arora
논문 정보
- arXiv ID: 2606.06468v1
- 분류: cs.AI
- 발표일: 2026년 6월 4일
- PDF: PDF 다운로드