Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement

Lean 4에서 청사진 생성과 정제로 형식 정리 증명을 수행하는 에이전트 프레임워크로 SOTA를 달성한다.

Goedel-Architect는 Lean 4에서 형식 정리 증명을 위한 에이전트 프레임워크로, 정의와 보조정리의 의존성 그래프인 청사진(blueprint)을 생성하고 정제하는 것이 핵심이다. 먼저 자연어 증명의 선택적 가이드와 함께 청사진을 생성하고, 도구가 장착된 Lean 증명기가 열린 보조정리를 병렬로 증명한다. 실패한 보조정리는 전역 청사진의 정제를 유도한다. DeepSeek-V4-Flash를 백본으로 MiniF2F-test 99.2%, PutnamBench 75.6% pass@1을 달성하며, 자연어 증명 가이드 추가 시 MiniF2F 100%, PutnamBench 88.8%, IMO 2025 4/6, Putnam 2025 11/12를 해결한다.

핵심 요약

• 정의와 보조정리의 의존성 그래프인 청사진을 생성하고 정제하는 전략을 사용한다.
• 재귀적 보조정리 분해 대신 병렬 증명과 전역 정제로 dead-end 루프를 방지한다.
• DeepSeek-V4-Flash(284B-A13B) 오픈 모델을 백본으로 사용한다.
• MiniF2F-test 100%, PutnamBench 88.8%, IMO 2025 4/6, Putnam 2025 11/12를 달성한다.
• 유사 오픈소스 파이프라인 대비 최대 500배 낮은 비용으로 SOTA를 기록한다.

논문 링크

외부 연구를 정리한 자료입니다. HDATF가 발표한 논문이나 제품 성능을 측정한 결과는 아닙니다.