🤖 AI

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

Goedel-Architect 是一个用于 Lean 4 定理证明的智能体框架，它利用蓝图生成与细化策略，在处理 MiniF2F、Putnam 和 IMO 等具有挑战性的数学基准测试时，实现了比现有流水线显著更低的成本以及最先进的性能。

原作者： 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 Fo

发布于 2026-06-05

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： 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

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正试图用乐高积木搭建一座宏伟且复杂的城堡。你有一份蓝图，但它不是一张图纸，而是一份指令清单，上面写着：“要建造塔楼，你首先需要一个地基，然后是一个墙壁，最后是一个窗户。”

问题在于，如果你试图通过一次巨大的飞跃来建造整个塔楼，你可能会卡住，或者在盖到一半时发现地基建错了。

Goedel-Architect 是一个全新的、智能的机器人团队，旨在用一种叫做 Lean 4 的语言来建造这些数学“城堡”（形式化证明）。它并没有试图一次性完成整个建筑，而是采用了一种名为**蓝图生成与精炼（Blueprint Generation and Refinement）**的策略。

以下是它的工作原理，分为简单的步骤：

1. 蓝图（总体规划）

在机器人开始建造之前，它会先绘制一张蓝图。

它是什么？ 可以把它看作是一个依赖关系图。它列出了证明这个大数学问题所需的每一个微小步骤（称为“引理”）。
它是如何工作的： 它绘制箭头来展示哪些步骤依赖于其他步骤。例如：“在完成墙壁之前，你不能建造屋顶。”
转折点： 有时，如果数学问题非常难，机器人会被给予一个自然语言证明。这就像是人类数学家给机器人提供了一个粗略的草图或一个关于如何解决问题的故事。机器人利用这个故事，从一开始就能绘制出更出色、更准确的蓝图。

2. 施工队（并行证明）

一旦蓝图准备就绪，机器人不会一个接一个地建造。它会派出整个由专业建筑师组成的团队（一个“Lean 证明器”）来同时进行所有微小步骤的工作。

每个建筑师只关注他们特定的步骤以及他们被允许使用的步骤（他们的“依赖项”）。
他们尝试建造自己的部分。如果成功了，他们就把那部分蓝图变成绿色。
如果失败了，就会变成蓝色（卡住）或红色（损坏）。

3. 修补循环（精炼）

这是 Goedel-Architect 区别于其他机器人的地方。

旧方法： 许多其他 AI 系统尝试解决一个问题，遇到困难后，就会不断地尝试将这一个卡住的部分拆解成更小的部分。这就像是通过在同一个地方用力猛砸来修理一面坏掉的墙一样。这往往会导致死胡同。
Goedel 的方式： 如果一名建筑师卡住了，整个团队会停下来并观察整张蓝图。
- 诊断： 机器人会问：“为什么失败了？”
  - 情况 A（红色）： “哦，这个步骤实际上是错误的！”（蓝图有一个错误的构想）。机器人修正该陈述。
  - 情况 B（蓝色）： “这个步骤是真的，但现在建造它太难了。” 机器人将这个大步骤拆解成两个或三个更小的、更容易的辅助步骤。
- 修订： 机器人根据这些新的、更小的步骤重写蓝图，并再次派出施工队。
- 效率： 至关重要的一点是，任何已经成功建造的部分（绿色）都会保持为绿色。机器人不会丢弃已有的成果；它只是修复损坏的部分并添加新的辅助步骤。

为什么这很重要？

论文声称这种方法是一个“游戏规则改变者”，主要基于两个原因：

它极其聪明且准确：
- 在一个标准的高中数学题测试（MiniF2F）中，它解决了 99.2% 的题目。在有了一点人类风格的故事（自然语言）帮助下，它解决了 100%。
- 在更难的大学水平数学（PutnamBench）上，它在自主状态下解决了 75.6%，在有帮助的情况下解决了 88.8%。
- 它甚至解决了来自非常近期、难度极高的竞赛（如 IMO 2025 和 Putnam 2025）中的题目，而此前没有任何其他开源机器人能解决这些题目。
它极其廉价：
- 其他解决这些问题的顶级机器人通常使用运行成本高达数千美元的“黑盒”模型。
- Goedel-Architect 使用了一个更便宜的开源大脑（DeepSeek-V4-Flash）。
- 成本： 为了解决整个 PutnamBench 测试，Goedel-Architect 花费了大约 294 美元。排名第二的开源竞争对手花费了大约 163,000 美元。这实现了 500 倍的节省。

核心结论

Goedel-Architect 就像一位大师级的建筑师，它不仅是尝试钉入一颗钉子，它还会绘制地图，派出团队进行并行建设，并且当某些部分损坏时，它会重新绘制整张地图来修复逻辑，保留好的部分，仅修改必要的部分。它证明了你并不需要最昂贵、最神秘的 AI 来解决最难的数学问题；你只需要一种更聪明的组织工作的方式。

技术摘要：Goedel-Architect

问题陈述

本文探讨了 Lean 4 中形式化定理证明的挑战，旨在弥合高性能专有系统与易于获取的开源流水线之间的差距。虽然前沿 AI 系统已展示出显著的数学能力（例如，获得 IMO 金牌，解决 Erdős 开放问题），但这些证明的验证需要严格的形式化。现有的开源解决方案在处理如 PutnamBench 等困难基准测试时表现不佳（得分 <15%），而高性能系统则依赖于未发布的模型或昂贵的专有 API（每次基准测试运行成本高达数千美元）。核心难点在于如何高效地将复杂的定理分解为可证明的引理，而不陷入递归死循环或产生过高的计算成本。

方法论

Goedel-Architect 是一个以**蓝图生成与精炼（blueprint generation and refinement）**为核心的智能体框架。与依赖递归自顶向下分解或单次证明生成的方案不同，该系统基于一个全局依赖图进行运作。

1. 蓝图生成

过程始于生成一个蓝图，其定义为一个由形式化陈述的定义和引理构成的依赖图，这些定义和引理共同构建出目标定理。

结构： 目标定理是图中唯一的汇点（sink）。每个节点代表一个定义或引理，边表示声明的依赖关系（即哪些引理被允许作为证明的依据）。
输入： 定理的形式化陈述始终是生成的种子。对于困难问题，自然语言证明（由更强的模型生成或作为解法提供）可以作为结构性引导。
验证： 生成器针对 Lean 编译器进行迭代，以确保生成的代码文件能够解析、所有节点类型正确，且图是无环且连通的。

2. 并行定理证明

一旦生成初始蓝图 ( $G_0$ )，系统会将每个引理节点分发给一个配备工具的 Lean 证明器进行并行处理。

上下文： 特定引理的证明器仅能看到该引理本身及其声明的依赖项（作为已知事实），而无法看到整个图。
工具： 证明器利用 Lean 编译器进行类型检查，并利用 Mathlib 检索服务进行引理查找。
诊断： 如果引理失败，证明器会返回结构化诊断。这包括：
- 否定（Negation）： 如果证明器找到了反例，它会注册一个对否定命题的证明。
  ，以及
- 缺口分析（Gap Analysis）： 如果引理未被证明但被认为是正确的，证明器会识别证明链在哪里断裂。

3. 蓝图精炼

如果仍有引理未被证明，精炼模型将根据失败信号重写全局蓝图 ( $G_{k+1}$ )。

策略： 精炼包括将困难引理分解为辅助引理、通过重新布线依赖关系来授予必要的访问权限，或者修改/删除已被证明为假的陈述。
保留： 前一次迭代中已成功证明的引理（绿色节点）及其签名将被保留，以确保计算工作不会被丢弃。
迭代： 修订后的蓝图将在并行状态下进行再次证明。该循环持续进行，直到所有节点都被解决或达到迭代预算上限。

核心贡献

以蓝图为中心的架构： 本文引入了一种全局依赖图方法，这与递归分解形成了对比。这使得并行证明尝试可以共享上下文，并使精炼过程能够同时作用于整个策略而非局部。
开源权重下的最先进性能： 该系统使用开源权重的 DeepSeek-V4-Flash (284B-A13B) 作为骨干网络，实现了最先进的性能，避免了对未发布模型或专有前沿模型的依赖。
成本效率： 该流水线的成本远低于同类高性能系统。论文报告其单个问题的成本约为 $0.44，比其他开源流水线低至 500 倍，且比专有替代方案低几个数量级。
自然语言引导： 框架证明了可选的自然语言证明可以作为初始蓝图有效的结构支架，特别是对于具有非局部结构（如循环和、除性链）的问题，有助于为精炼循环锚定策略。

实验结果

系统在五个基准测试上进行了评估：MiniF2F-test、PutnamBench、IMO 2025、Putnam 2025 和 USAMO 2026。

MiniF2F-test： 在没有自然语言引导的情况下实现了 99.2% 的 pass@1（242/244 个问题）。在加入可选的自然语言引导后，解决了全部 244 个问题（100%），刷新了开源权重的记录。
PutnamBench： 实现了 75.6% 的 pass@1（508/672 个问题），超越了 Hilbert 流水线（pass@1 为 70.0%）和 AxProverBase（pass@1 为 54.7%）。在使用自然语言引导（pass@4）时，解决率提升至 88.8%（597/672）。
IMO 2025： 解决了 4/6 个问题。
Putnam 2025： 解决了 11/12 个问题。
USAMO 2026： 解决了 3/6 个问题（这是一个无污染基准，因为题目日期晚于模型训练截止日期）。

成本分析： 在 PutnamBench 上，Goedel-Architect 以 $294 的 API 成本解决了全部 672 个问题。相比之下，排名第二的开源流水线（Hilbert）据报道在单次运行中花费了约 $163k–$ 170k，凸显了巨大的效率差距。

重要性与主张

作者声称，Goedel-Architect 建立了一个新的帕累托前沿（Pareto frontier）。它证明了通过高度高效的开源权重骨干网络和创新的流水线设计，可以实现足以媲美 AlphaProof 或使用 Claude Opus 4.5 等大型专有系统的顶级性能。

论文强调，全局依赖图（允许整体精炼）与开源模型（DeepSeek-V4-Flash）的结合是取得成功的关键。该系统有效地缩小了学术可及性与前沿性能之间的差距，使高水平的形式化证明能够在极低的成本下实现。作者指出，虽然自然语言引导显著提升了处理最难问题的性能，但在标准基准测试上，核心流水线在没有引导的情况下依然稳健且有效。