Goedel‑Architect（arXiv:2606.06468）paper main points | 论文要点

Goedel‑Architect（arXiv:2606.06468）论文要点提取

标题：Goedel‑Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement
机构：普林斯顿大学；通讯：Sanjeev Arora、陈丹琦（Danqi Chen）、Chi Jin 等；基座：DeepSeek‑V4‑Flash（284B‑A13B，开源权重）；面向 Lean4 形式化定理证明智能体流水线。

一、研究背景与动机

近年AI数学在IMO、Erdős公开猜想取得进展，但AI生成证明需要Lean类形式化工具做机器可校验，避免幻觉引理。
现有形式证明系统分三类：
- 非智能体：单次输出完整Lean证明（Goedel‑Prover、DeepSeek‑Prover），Putnam级题目正确率很低；
- 单智能体Agent：单个大模型交替调用Lean编译器（AxProverBase、Numina‑Lean‑Agent），多使用闭源Claude/Gemini；
- 流水线Pipeline：递归子目标分解（Hilbert、Seed‑Prover），递归树方案一旦分支走进死胡同，整棵子树工作作废，容易无效循环；顶尖效果的系统大多是闭源，或者推理API成本极其昂贵。
痛点：缺少基座开源、整套流水线可复现、算力成本可控，同时竞赛级形式证明性能对标闭源大模型的系统。

二、核心创新：Blueprint（蓝图）全局DAG范式，区别传统递归分解

Goedel‑Architect核心是蓝图Blueprint：有向无环依赖图DAG，图节点=定义/引理/主定理；边=依赖关系；主定理是图唯一汇点。整体分为三大阶段循环迭代：

1）蓝图生成 Blueprint Generation

输入：定理的Lean形式化陈述；可选输入：自然语言非正式证明草稿作为结构引导（+NL模式）
输出：完整Lean文件，每个节点给出严格形式化命题，但全部引理留sorry_using[...]（只写依赖、不写证明）；通过Lean编译器校验语法、类型、图无环。

可选自然语言草稿只提供高层策略，不直接生成Lean代码；困难题目依靠该引导大幅提升成功率。

2）定理证明 Theorem Proving

将蓝图中每一个未证明节点并行派发Lean证明器；每个证明器仅可见当前节点 + 它声明依赖的上游节点，不看整张图。
证明器可调用Lean编译器、Mathlib检索；每个节点返回三类结果：
1. ✅ PROVED：成功证明（绿色节点）；证明结果保留，后续迭代不再重复证明；
2. ❌ STATEMENT_WRONG：命题本身为假，得到机器校验反例（红色节点）；
3. ⚠️ PROOF_TOO_HARD：命题大概率为真，但当前预算无法证明（蓝色节点）；输出结构化失败诊断报告：失败分析、卡住位置、建议拆分辅助引理。

3）蓝图精炼 Blueprint Refinement（迭代闭环）

读取所有节点诊断报告，修改整张全局依赖图，保留所有已经证明成功的节点不变（签名不变就复用证明），只修改失败节点：

若诊断STATEMENT_WRONG：修复引理假设/结论，或者直接删除该节点并重接线依赖；
若诊断PROOF_TOO_HARD：按照建议拆出新的辅助引理节点，更新依赖边；
输出修正后的蓝图 $G_{k+1}$，再次送入证明阶段循环；直到全部节点证明完成或迭代预算耗尽。

关键差异对比：传统递归分解是自上而下一棵树，子分支失败就丢弃；Blueprint维护全局DAG，已证明节点可跨迭代复用；失败输出结构化诊断而不只是简单报错；支持并行证明多个独立分支。

三、主要实验与基准结果

pass@1：流水线层面单次蓝图生成，最多迭代8‑16轮；+NL模式：引入外部自然语言证明草稿做蓝图种子。

Benchmark	Goedel‑Architect pass@1	Goedel‑Architect (+NL)
MiniF2F‑test	99.2%（242/244）	100%（244/244）
PutnamBench(672题)	75.6%	88.8%（597/672）
IMO 2025	—	4/6
Putnam 2025	—	11/12
USAMO 2026（无训练污染）	—	3/6

算力成本亮点（核心结果）

PutnamBench完整评测总开销仅 294美元，单题平均0.44美元；
对比Hilbert（Gemini2.5Pro）约16.3万美元，成本降低接近500倍，同时pass@1准确率还更高。
性能随蓝图精炼迭代次数呈近似对数线性提升，迭代越多解题越多。

消融实验（控制变量，全部使用DeepSeek‑V4‑Flash同一基座）

直接单轮输出Lean证明：MiniF2F 67.6%；PutnamBench仅6.5%；
普通单Agent工具增强推理TIR：MiniF2F 97.1%，PutnamBench 54.5%；
将Hilbert递归流水线移植到同一个DeepSeek基座，效果显著弱于Goedel‑Architect； > 结论：性能提升主要来自Blueprint流水线架构，不是基座模型本身的能力。

+NL模式的作用

部分高难度题目，仅从形式化命题很难想出正确整体证明策略；引入外部自然语言证明草稿，作为蓝图DAG的高层结构脚手架，可以攻克一批原本完全无法解决的题目。注意：证明器、精炼阶段仍然全部使用开源基座，外部草稿仅用于初始化蓝图。

四、两个典型失败处理案例（附录B）

STATEMENT_WRONG案例（Putnam1971 A6、Putnam1989 A6）：蓝图生成的辅助引理存在漏洞（缺少假设、二进制表示方向理解错误）；Lean给出反例，精炼阶段直接修改引理命题，下游依赖图同步修正，不需要全部推倒重来。
PROOF_TOO_HARD案例（Putnam1985 B1）：主引理一次性证明难度过高；证明器输出结构化分析，精炼阶段自动拆分为一组更小case‑split辅助引理，拆分后全部节点顺利证出。

五、系统局限与边界

当前测试集范围：高中奥赛、本科Putnam级竞赛数学；尚未对前沿公开数学猜想做评估；
对于部分高度非局部结构证明（循环求和、复杂奇偶链等），无NL引导下蓝图生成会卡住，依赖外部自然语言策略种子；
依赖Mathlib库；高阶分析/PDE等Mathlib覆盖弱的领域，能力受限；
USAMO2026虽然是无污染测试，但仍然是竞赛题，不是开放未解决猜想。

六、论文关键启示（和你之前讨论国产开源Math‑AI关联）

数学形式证明系统 = 基座大模型 + 外层Agent流水线Harness；同样一个开源基座DeepSeek‑V4‑Flash，换Blueprint架构后PutnamBench从54.5% →75.6%，架构带来巨大增益。
失败不能简单丢弃，要转化成结构化诊断信号（区分“命题错”vs“证明太难”），是做长、复杂证明的关键；传统一次性采样模型只会输出幻觉，缺少这套诊断‑修正闭环。
开源数学AI追赶闭源，不只是刷MATH、IMO做题分数；开源整套Agent流水线框架（Blueprint+精炼循环）同等重要，甚至比基座参数更关键。
自然语言非正式证明与形式化DAG蓝图的分工：人/大模型想高层策略，交给流水线拆引理、并行证明、迭代修复。

DEV Community