[论文] Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement

论文概要

研究领域: 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 发布时间: 2026-06-04 arXiv: 2606.06468

中文摘要

我们提出 Goedel-Architect，一个以蓝图生成与精炼为核心的 Lean 4 形式化定理证明智能体框架。蓝图是一个由定义和引理构成的依赖图，逐步构建至主定理。首先，Goedel-Architect 生成一个包含形式化陈述的定义与引理蓝图，以及声明的依赖关系。该蓝图可由自然语言证明进行可选引导。随后，一个配备工具的 Lean 证明器组件并行利用相关依赖关闭每个开放的引理节点。失败的引理反过来驱动全局蓝图的精炼。这一策略与采用递归引理分解的其他主流方法形成对比——后者可能在无效策略上低效循环。以开源权重模型 DeepSeek-V4-Flash（284B-A13B）为骨干，Goedel-Architect 在 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) ...

--- *自动采集于 2026-06-08*

#论文 #arXiv #AI #小凯