괴델-아키텍트: 청사진 생성 및 개선을 통한 형식적 정리 증명의 효율성 향상

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

본 논문에서는 Lean 4 환경에서 동작하는 형식적 정리 증명 프레임워크인 Goedel-Architect를 소개합니다. Goedel-Architect는 청사진(blueprint) 생성 및 개선에 중점을 두며, 여기서 청사진은 주요 정리에 도달하기 위한 정의와 보조정명의 의존성 그래프를 나타냅니다. 먼저, Goedel-Architect는 공식적으로 명시된 정의와 보조정명, 그리고 선언된 의존성을 포함하는 청사진을 생성합니다. 이 청사진은 선택적으로 자연어 증명에 의해 안내될 수 있습니다. 그런 다음, 도구 지원 Lean 검증 모듈은 관련 의존성을 사용하여 각 열린 보조정명 노드를 병렬로 채웁니다. 실패한 보조정명은 전체적인 청사진을 개선하는 데 사용됩니다. 이러한 전략은 다른 주요 접근 방식과 달리, 재귀적 보조정명 분해를 사용하는 경우 발생할 수 있는 비효율적인 루프 현상을 방지합니다. Goedel-Architect는 DeepSeek-V4-Flash (284B-A13B) 모델을 기반으로 하며, MiniF2F-test에서 99.2%의 pass@1 성능, PutnamBench에서 75.6%의 pass@1 성능을 달성했습니다. 특히 어려운 문제에 대해 자연어 증명을 사용하여 초기 청사진을 생성하면, 나머지 두 개의 MiniF2F-test 문제를 해결하여 100%를 달성하고, PutnamBench의 성능을 88.8% (597/672)로 향상시켰으며, IMO 2025에서 4/6, Putnam 2025에서 11/12, USAMO 2026에서 3/6 문제를 해결했습니다. 이는 오픈 소스 파이프라인으로서 최고 수준의 성능을 제공하며, 유사한 오픈 소스 파이프라인에 비해 최대 500배 저렴합니다.

We introduce Goedel-Architect, an agentic framework for formal theorem proving in Lean 4 centered on blueprint generation and refinement. A blueprint is a dependency graph of definitions and lemmas that builds up to the main theorem. First, Goedel-Architect generates a blueprint of formally stated definitions and lemmas, along with declared dependencies. This blueprint is optionally guided by a natural language proof. Then, a tool-equipped Lean prover component closes each open lemma node in parallel using relevant dependencies. Failed lemmas in turn drive refinement of the global blueprint. This strategy contrasts with other mainstream approaches which use recursive lemma decomposition, and can inefficiently loop on dead-end strategies. Using the open-weight DeepSeek-V4-Flash (284B-A13B) as the backbone, Goedel-Architect attains 99.2% pass@1 on MiniF2F-test and 75.6% pass@1 on PutnamBench. With an optional natural-language proof seeding the initial blueprint on the harder problems, we additionally close the remaining two MiniF2F-test problems (reaching 100%), lift PutnamBench to 88.8% (597/672), and solve 4/6 on IMO 2025, 11/12 on Putnam 2025, and 3/6 on USAMO 2026. This represents state-of-the-art performance for an open-source pipeline at a price point up to 500x less than comparable open-source pipelines.