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

📄 arXiv: 2606.06468v1 📥 PDF

作者: 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

分类: cs.AI

发布日期: 2026-06-04

💡 一句话要点

提出Goedel-Architect以简化形式定理证明过程

🎯 匹配领域: 支柱五：交互与反应 (Interaction & Reaction)

关键词: 形式定理证明 蓝图生成 引理优化 Lean 4 自动化证明 深度学习 算法效率

📋 核心要点

  1. 现有的形式定理证明方法常常依赖递归引理分解，可能导致低效的循环和死胡同问题。
  2. Goedel-Architect通过生成和优化蓝图来解决这一问题，允许并行处理引理并根据失败情况调整全局蓝图。
  3. 实验结果显示，Goedel-Architect在多个基准测试中表现优异，尤其在困难问题上通过率显著提升。

📝 摘要（中文）

我们介绍了Goedel-Architect，这是一个基于蓝图生成和优化的形式定理证明框架，专注于Lean 4环境。该框架首先生成一个包含定义和引理的依赖图蓝图，并可通过自然语言证明进行指导。随后，Lean证明器组件并行处理每个开放引理节点，利用相关依赖来关闭引理。失败的引理会推动全局蓝图的优化。与其他主流方法相比，Goedel-Architect在MiniF2F-test和PutnamBench上分别达到了99.2%和75.6%的通过率，展现了其在开源管道中的领先性能。

🔬 方法详解

问题定义：论文旨在解决现有形式定理证明方法中效率低下和循环死胡同的问题，特别是在引理分解过程中。

核心思路：Goedel-Architect的核心思路是生成一个依赖图蓝图，允许并行处理引理，并根据失败的引理动态优化蓝图，从而提高证明效率。

技术框架：整体架构包括蓝图生成、引理处理和全局优化三个主要模块。蓝图生成阶段结合自然语言证明，随后Lean证明器并行处理引理，最后根据结果优化蓝图。

关键创新：最重要的技术创新在于蓝图生成和优化策略的结合，避免了传统方法中的递归引理分解，显著提高了效率。

关键设计：关键设计包括使用DeepSeek-V4-Flash作为基础模型，设置合理的参数以支持并行处理，并设计灵活的依赖管理机制以适应不同的证明场景。

🖼️ 关键图片

fig_0
fig_1

📊 实验亮点

实验结果显示，Goedel-Architect在MiniF2F-test上达到了99.2%的通过率，在PutnamBench上达到了75.6%。在更困难的问题上，通过自然语言证明的引导，进一步提升了MiniF2F-test的通过率至100%，并将PutnamBench的通过率提升至88.8%。

🎯 应用场景

该研究的潜在应用领域包括自动化定理证明、形式验证和程序分析等。通过提高定理证明的效率，Goedel-Architect可以在软件开发、数学研究和人工智能等领域产生实际价值，推动相关技术的发展。

📄 摘要（原文）

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.