沙丘社区
论文

Goedel-Architect：以蓝图生成与精化 streamline 形式定理证明

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

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
智能体系统Agent 规划

摘要

我们介绍了 Goedel-Architect，这是一个在 Lean 4 中以蓝图生成和细化为中心的形式定理证明的代理框架。蓝图是构建主定理的定义和引理的依赖图。首先，Goedel-Architect 生成正式陈述的定义和引理以及声明的依赖关系的蓝图。该蓝图可选地由自然语言证明来指导。然后，配备工具的Lean证明器组件使用相关依赖项并行关闭每个开放引理节点。失败的引理反过来又推动了全球蓝图的完善。该策略与其他使用递归引理分解的主流方法形成鲜明对比，并且可能会低效地循环死胡同策略。使用开放权重 DeepSeek-V4-Flash (284B-A13B) 作为骨干，Goedel-Architect 在 MiniF2F 测试上获得 99.2% pass@1，在 PutnamBench 上获得 75.6% pass@1。通过可选的自然语言证明，为更难的问题奠定了初始蓝图，我们还解决了剩下的两个 MiniF2F 测试问题（达到 100%），将 PutnamBench 提升到 88.8% (597/672)，并解决了 IMO 2025 上的 4/6、Putnam 2025 上的 11/12 和 USAMO 2026 上的 3/6。这代表了最先进的性能开源管道的价格比同类开源管道低 500 倍。

Goedel-Architect：以蓝图生成与精化 streamline 形式定理证明：论文配图
图 2：PutnamBench 上的计算缩放。 Goedel-Architect 使用开放权重 DeepSeek-V4-Flash 主干网络解决的累积问题（左轴；右轴为 672672 问题基准的百分比）与对数尺度上的蓝图细化迭代次数相比。 pass@11曲线仅使用默认管道； pass@44 (+ NL) 曲线是 pass@44 NL 的努力。仅初始蓝图（迭代 00）就解决了 200200 个问题；随后的每个细化通道都会增加更多，通过迭代 1616，在 pass@11 处达到 508508 (75.6%75.6\%)，在 pass@44 (+ NL) 处达到 597597 (88.8%88.8\%)。求解计数随着细化计算大致呈对数线性增长。