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

Motivation

• Known: 최근 frontier AI 시스템들이 IMO 등 수학 대회에서 뛰어난 성과를 보이고 있으며, Lean과 같은 정형 언어를 이용한 formal theorem proving은 AI가 생성한 증명의 엄밀성과 검증 가능성을 보장하는 방법으로 주목받고 있다. AlphaProof와 같은 closed-weight RL 기반 시스템이 최고 성능을 보이지만, 오픈소스 non-agentic prover들은 PutnamBench 같은 어려운 벤치마크에서 15% 미만의 낮은 성능을 보인다.
• Gap: PutnamBench에서 50% 이상을 달성하는 기존 시스템들은 모두 unreleased model/pipeline을 사용하거나, 수천 달러의 API 비용이 드는 frontier model에 의존하고 있어, 오픈 가중치와 오픈 파이프라인을 저비용으로 동시에 만족하는 고성능 시스템이 부재하다. 또한 기존 pipeline 접근법은 recursive lemma decomposition에 의존해 dead-end 전략에서 비효율적으로 반복되는 문제가 있다.
• Why: 공개 가중치 모델과 공개 파이프라인만으로 저비용에 frontier급 formal theorem proving 성능을 달성함으로써, 연구자와 애호가들이 접근 가능한 고성능 오픈소스 시스템의 새로운 Pareto frontier를 제시하기 때문에 중요하다.
• Approach: 전역 dependency graph 형태의 blueprint를 top-down recursion 대신 반복적으로 재작성하는 방식을 중심 메커니즘으로 채택하고, 오픈 가중치 백본(DeepSeek-V4-Flash)과 오픈 파이프라인만으로 구성하여 비용을 획기적으로 낮췄다.

Achievement

1. 최고 수준의 벤치마크 성능: DeepSeek-V4-Flash(284B-A13B) 백본만으로 MiniF2F-test에서 99.2% pass@1, PutnamBench에서 75.6% pass@1을 달성했다.
2. 자연어 증명 시딩을 통한 추가 성능 향상: 어려운 문제에 자연어 증명을 초기 blueprint에 시딩함으로써 MiniF2F-test 100% 완주, PutnamBench 88.8%(597/672)까지 향상시켰다.
3. 최신 대회 문제 해결: IMO 2025 4/6, Putnam 2025 11/12, USAMO 2026 3/6 문제를 해결했다.
4. 압도적인 비용 효율성: 비교 가능한 오픈소스 파이프라인 대비 최대 500배 저렴한 비용(문제당 약 $0.44 vs 약 $244)으로 state-of-the-art 오픈소스 성능을 달성했다.

How

• Blueprint generation: 목표 정리의 formal statement를 입력받아 정의와 lemma로 이루어진 dependency graph를 하나의 Lean 파일로 생성하며, 각 lemma는 의존 가능한 다른 노드를 명시적으로 선언하고 이는 LeanArchitect Lean package로 기록·검증된다. 목표 정리는 그래프의 유일한 sink이며, 처음에는 lemma 본문이 증명되지 않은 상태로 남는다.
• 자연어 증명 guidance(선택적): 어려운 문제에 대해 강한 모델이나 공식 solution 등에서 얻은 자연어 증명을 구조적 가이드로 사용해 blueprint를 생성할 수 있으며, 이는 Draft-Sketch-Prove 아이디어를 graph 형태로 확장한 것이다.
• Theorem proving: tool-equipped Lean prover 컴포넌트가 각 open lemma node를 declared parents(의존 노드)만을 활용해 병렬로 증명 시도하고, Lean compiler와 Mathlib으로 후보 증명을 검증한다.
• Blueprint refinement: 실패한 노드는 STATEMENT WRONG(반례 발견 또는 거짓으로 추정되나 반증 불가) 또는 PROOF TOO HARD(참으로 보이나 parent로부터 chain 불가) 두 진단 중 하나를 받아, 각각 formalization 수정 또는 lemma 분해로 이어지며, 이미 해결된 노드는 green으로 보존한 채 revised blueprint를 생성한다.
• 이 과정을 모든 노드가 해결되거나 iteration 예산이 소진될 때까지 반복한다.

Originality

• recursive top-down lemma decomposition 대신 전역 dependency graph(blueprint)를 반복적으로 재작성하는 방식을 제안하여, 병렬 증명 시도들이 context를 공유하고 refinement가 전체 전략에 동시에 작용할 수 있게 함
• 실패 노드를 STATEMENT WRONG과 PROOF TOO HARD로 명시적으로 이분화하여 진단·대응하는 refinement 메커니즘 설계
• Draft-Sketch-Prove의 flat sketch 방식을 graph 기반의 named sub-lemma 구조로 확장하여 자연어 증명을 구조적 가이드로 활용
• 오픈 가중치 백본과 오픈 파이프라인만으로 closed 시스템에 필적하는 성능을 최대 500배 낮은 비용으로 달성

Limitation & Further Study

• 발췌된 본문에서는 blueprint refinement의 구체적 알고리즘(예: 얼마나 자주, 몇 회 iteration까지 수행되는지)에 대한 세부사항이 충분히 제시되지 않아 방법론의 완전한 재현성 검증이 어렵다.
• 자연어 증명 시딩이 필요한 "harder problems"의 선정 기준이 불명확하며, 이 개입이 없는 완전 자동 파이프라인만으로는 일부 최고난도 문제(IMO, USAMO)에서 여전히 낮은 solve rate를 보인다.
• 비용 비교가 특정 backbone과 API 가격 시점에 의존적이어서, 모델 가격 변동이나 backbone 교체 시 500배라는 비용 우위가 어떻게 변화할지에 대한 논의가 부족하다.
• 후속 연구로 자연어 증명 없이도 최고난도 대회 문제(IMO, USAMO)의 solve rate를 높이는 방향, 그리고 다른 open-weight 백본으로의 일반화 검증이 필요하다.

Evaluation

총평: 전역 dependency graph 기반 blueprint 생성·정제라는 새로운 파이프라인 설계를 통해 오픈 가중치 모델만으로 closed 시스템에 필적하는 formal theorem proving 성능을 매우 낮은 비용으로 달성한 인상적인 연구이며, 오픈소스 정형 증명 생태계에 실질적인 기여를 한다.