Diffusion-Proof: Recipe for Formal Theorem Proving Beyond Auto-Regressive Generation

当扩散模型遇见数学殿堂：一场关于"证明"的革命

论文信息

• 标题: Diffusion-Proof: Recipe for Formal Theorem Proving Beyond Auto-Regressive Generation
• 作者: Ruida Wang, Rui Pan, Pengcheng Wang, Shizhe Diao, Tong Zhang (香港科技大学)
• arXiv: 2606.19315
• 发表时间: 2026-06-17
• 领域: 形式化定理证明 · 扩散模型 · 数学推理
• 一句话总结: 首次将扩散语言模型(dLLM)应用于形式化定理证明，通过双向生成和局部修正能力，超越传统自回归模型，成功解决了一道IMO难题。

🎭 开场：一个古老的梦想

想象一个场景：你面对一道数学奥林匹克难题，苦思冥想三小时。你写下了一些思路，但发现中间有一个步骤错了。你不需要推倒重来，而是盯着那个错误的地方，从上下文推断它应该是什么。你的大脑同时利用了"前面已经证明的"和"后面需要得到的"来修正中间的错误。

这就是人类数学家做证明的方式：不是严格的从左到右，而是双向的、迭代的、允许犯错的。

但传统的AI定理证明器呢？它们像一台打字机：只能从左到右生成，一旦错了，要么继续错下去，要么全部推倒重来。这就像在黑暗中走钢丝，没有安全网，也没有回头路。

今天的论文，就是在问：如果AI也能像我们一样"回头看"、"双向思考"、"局部修正"呢？

🧮 第一章：形式化定理证明——数学的终极审计

1.1 什么是形式化证明？

想象你要证明"1+1=2"。在纸上写几行就够了。但在形式化系统中（如Lean 4），你需要从集合论公理出发，定义自然数、加法，然后一步步推导出1+1=2。整个过程可能需要几十行甚至上百行代码。

形式化证明是"机器可验证的"数学：每个步骤都严格遵循逻辑规则，没有直觉跳跃，没有"显然"。计算机像一个严格的审计师，检查每一步是否合法。

为什么这很重要？因为：

• Kepler猜想：Thomas Hales用计算机辅助证明，但审稿人无法完全验证，最后花了12年才形式化
• 四色定理：第一个主要依赖计算机的证明，曾引发"这是不是真正的数学"的争论
• 现代AI：深度学习的正确性越来越难以人工验证

1.2 Lean 4：数学家的编程语言

Lean 4是由Microsoft Research开发的定理证明器。它把数学证明变成了一种编程语言：

theorem arithmetic_example : 1 + 1 = 2 := by
  exact rfl  -- rfl 是"自反性"，即 x = x

更复杂的证明会使用"tactics"（策略）——类似程序中的指令：

• intro：引入假设
• apply：应用某个定理
• have：证明一个中间结论
• exact：提供最终答案

AI定理证明的目标：给定一个定理陈述，自动生成完整的证明脚本。

🔄 第二章：自回归的困境——单向思维的代价

2.1 传统LLM的"打字机模式"

自回归（Auto-Regressive, AR）语言模型——如GPT系列——生成文本的方式就像打字机：

P(x_i | x_1, x_2, ..., x_{i-1})

每个token只能基于前面的token生成。这有什么问题？

问题1：指数级错误累积

• 假设每个token有95%的正确率
• 一个100步的证明，整体正确率是 0.95^100 ≈ 0.6%
• 一步错，步步错，后面所有token都基于错误的前提

问题2：缺乏长程连贯性

• 证明的开头定义了一个引理
• 证明的结尾需要用到这个引理
• 但AR模型在生成结尾时，可能"忘记"了开头的定义
• 因为中间生成了太多内容，上下文窗口被稀释了

问题3：无法局部修正

• 如果证明的第50步错了，AR模型只能：
  • 继续生成（让错误扩散）
  • 全部重生成（浪费前面49步的正确工作）
• 它不能"只修改第50步"，因为生成是单向的、因果的

2.2 现有SOTA的局限性

DeepSeek-Prover-V2、Goedel-Prover-V2等最先进的AR定理证明器已经能解决许多复杂问题。但论文指出：它们仍然受限于AR的根本缺陷。

一个具体例子：一道IMO（国际数学奥林匹克）题目，DeepSeek-Prover-V2-7B无法解决。但Diffusion-Proof——使用更小的扩散模型——成功解决了它。这说明，生成范式的差异可能比模型规模更重要。

🎨 第三章：扩散模型——从噪声到秩序的艺术

3.1 扩散模型的日常类比

想象一个雕塑家。她面前不是一块完整的石头，而是一团混乱的泥块。她不需要从零开始雕刻——而是先看到泥块中隐约的轮廓，然后一点点去除多余的泥，让雕像浮现出来。

这就是扩散模型的工作方式：

1. 正向过程：逐步添加噪声，把数据变成纯噪声
2. 反向过程：学习从噪声中恢复数据，逐步去噪

在图像生成中，这创造了Stable Diffusion、DALL-E等奇迹。在文本生成中，它创造了Diffusion LLM（dLLM）。

3.2 dLLM的数学原理

传统AR模型：
L_AR = -Σ log P(x_i | x_{<i})

扩散模型（简化版）：
L_dLLM = -E_{t, x^(0), x^(t)} [Σ I[x_i^(t) = MASK] · log P(x_i^(0) | x^(t))]

关键区别：

• AR：只能看到前面的token
• dLLM：在训练时，可以看到"被掩码的序列"，即双向上下文
• t（时间步）：控制噪声程度，t=1是纯噪声，t=0是原始数据

3.3 块级扩散（Block Diffusion）：平衡灵活与效率

纯dLLM生成整个序列，计算开销大。块级扩散（Block Diffusion）是折中：

• 把序列分成大小为B的块
• 块内：双向注意力（可以看到块内所有token）
• 块间：保持因果性（块i只能依赖块<i）
• 推理时，一次生成一个块，迭代直到完成

这平衡了扩散的全局性和AR的效率。论文使用的是Fast-dLLM-V2-7B作为基础模型。

🏗️ 第四章：Diffusion-Proof框架——双重奏的设计

4.1 整体架构：证明者 + 修正者

Diffusion-Proof包含两个协同工作的7B模型：

dLLM-Prover-7B：全局证明生成器

• 任务：给定定理陈述，生成完整的Lean 4证明
• 特点：利用块扩散实现长程连贯的策略使用

dLLM-Corrector-7B：局部修正专家

• 任务：当证明有错误但骨架正确时，修正局部错误
• 特点：利用双向信息进行"填空式"修正

这就像建筑团队：一个建筑师画整体蓝图，一个质检员检查细节并修复问题。

4.2 数据准备：从550万到30万的筛选艺术

阶段1：数据收集

• 从先前工作中收集550万条定理证明记录
• 来源：Lean GitHub仓库、数学库、已有证明器输出

阶段2：清洗与筛选

• 筛选出300k条高质量数据
• 包含自然语言（NL）和形式语言（FL）的混合
• 用于微调Fast-dLLM-V2-7B → dLLM-Prover-7B

阶段3：子目标分解与块填充

• 识别证明中的子目标（subgoal）结构
• 对需要修正的数据进行"块填充"格式化：
  • 删除错误证明部分，替换为<|MASK|>序列（256个token）
  • 保留前缀（正确部分）和后缀（后续目标）
  • 用于训练dLLM-Corrector-7B

4.3 训练细节：计算资源的透明化

论文罕见地提供了详细的计算信息：

• dLLM-Prover-7B训练：96 H100 GPU小时
• AR基线（Qwen-2.5-Lean-SFT-7B）训练：96 H100 GPU小时
• dLLM-Corrector-7B训练：额外48 H100 GPU小时
• 总成本：约240 H100 GPU小时（按市场价约$300-500）

对比SOTA模型（如DeepSeek-Prover-V2），这个计算规模相对较小，说明方法创新比 brute force 更重要。

⚔️ 第五章：推理过程——生成与修正的舞蹈

5.1 完整证明生成

1. 输入：自然语言定理描述 + Lean 4形式化陈述
2. dLLM-Prover-7B使用块扩散生成：
   • 分块生成证明（每块B个token）
   • 块内双向推理，块间保持因果
   • 迭代直到生成完整证明或达到最大长度

5.2 错误检测与修正——Diffusion-Proof的灵魂

这是Diffusion-Proof区别于所有AR方法的关键：

步骤1：Lean验证

• 生成的证明提交给Lean 4编译器
• 如果编译通过 → 成功！
• 如果编译失败 → 进入修正流程

步骤2：骨架分析

• 检查是否"所有顶层子目标陈述和它们的用法都是正确的"
• 如果是：错误只存在于某个子目标的证明中，骨架是对的
• 如果不是：错误更严重，可能需要重新生成

步骤3：大块扩散修正

• 定位错误的子目标
• 删除该子目标的证明部分，替换为256个<|MASK|>token
• dLLM-Corrector-7B使用512长度的扩散块进行修正：
  • 利用前缀（前面正确的证明）和后缀（后续目标）
  • 双向推断被掩码部分应该是什么
  • 生成温度设为1.2（鼓励创造性）
  • 去噪置信度0.95（确保鲁棒性）

步骤4：迭代

• 修正后的证明再次提交Lean验证
• 如果仍失败，可以再次修正（有迭代修正能力）

5.3 为什么这像人类数学家？

人类数学家做证明时：

1. 先写整体框架（对应Prover）
2. 检查每一步（对应Lean验证）
3. 发现错误时，只看错误那部分（对应Corrector的局部修正）
4. 利用上下文推断修正（对应双向信息）
5. 可能需要多次修正（对应迭代）

AR模型只能做1和2。Diffusion-Proof能做1-5。

📊 第六章：实验结果——数字的胜利

6.1 基准测试：MiniF2F和ProofNet

MiniF2F-Test：涵盖代数、数论、几何、组合等奥数级别题目
ProofNet-Test：大学本科水平的数学形式化证明

6.2 主结果：Diffusion-Proof vs AR基线

在pass@32（生成32个候选，看是否有一个成功）指标下：

（论文报告的是绝对提升，即百分点提升。6.14%在定理证明领域是非常大的进步。）

6.3 关键突破：解决DeepSeek-Prover-V2-7B无法解决的IMO题

论文最引人注目的结果：

• Diffusion-Proof成功解决了一道IMO题目
• DeepSeek-Prover-V2-7B（更强的思考模型）无法解决同一题

这说明，生成范式的差异（扩散 vs 自回归）可以弥补甚至超越模型能力的差距。就像一把精巧的瑞士军刀可能比一把笨重的大砍刀更适合某些精细工作。

6.4 消融实验：验证每个组件的价值

论文进行了详细的消融分析：

• 去掉Corrector：性能下降，证明修正能力很重要
• 去掉大块修正：小范围修正效果差，说明需要足够的上下文
• 不同温度设置：温度1.2平衡了创造性和准确性

🧠 第七章：深层思考——扩散模型的推理优势

7.1 为什么扩散模型适合数学？

数学证明有一个关键特征：结构化的、层次化的、可分解的。

• 证明 = 多个子目标的组合
• 每个子目标可以独立验证
• 错误通常是局部的，不必然破坏整体

扩散模型的特性恰好匹配：

• 块级生成：天然对应子目标结构
• 双向信息利用：可以在已知前后目标的情况下推断中间步骤
• 迭代修正：允许试错和渐进完善

AR模型则强行把证明变成线性序列，破坏了数学的自然结构。

7.2 长程连贯性：为什么数学需要"回头看"

一个复杂证明可能在第10步定义了一个引理，在第100步用到它。AR模型在第100步时，需要把第10步的信息"携带"90步。这在长序列中极其困难。

扩散模型通过全局去噪，可以在生成过程中"看到"整个序列的轮廓，因此能更好地保持长程依赖。这就像：

• AR：像盲人摸象，每次只摸一个部位，不知道整体形状
• 扩散：像近视者逐渐戴上眼镜，从一开始就能看到模糊的全貌，然后逐渐清晰

7.3 局限性与未来方向

论文坦诚地指出了局限：

1. 计算规模有限：相比SOTA（如Goedel-Prover-V2），训练规模较小
2. Long CoT能力有限：基础模型缺乏长链思考能力，未能完全探索dLLM的潜力
3. 仅支持Lean 4：其他形式化系统（如Isabelle、Coq）需要更多资源
4. 缺乏理论分析：主要关注经验改进，未深入理论分析

未来方向：

• 扩展训练规模
• 增强推理能力（如结合Long CoT）
• 支持更多定理证明器
• 建立dLLM在形式推理中的理论基础

🎯 第八章：对AI研究的意义

8.1 范式转移：从AR到扩散的文本生成

这篇论文是扩散语言模型在数学推理领域的首次成功应用。它表明：

• 扩散模型不只是"图像生成工具"
• 在需要结构化、可修正、双向推理的任务中，扩散可能优于自回归

这可能开启一个新的研究方向：哪些文本任务更适合扩散？

• 代码生成（结构化、可编译验证）
• 数学证明（可验证、层次化）
• 结构化数据生成（JSON、SQL等）

8.2 对AI数学的启示

数学是智能的终极测试。如果AI能在数学领域取得突破，意味着它在抽象推理、逻辑严谨性、创造性方面达到了新高度。

Diffusion-Proof的成功提示：我们可能需要重新思考"如何生成"，而不仅仅是"生成什么"。

8.3 对AI安全的启示

形式化验证是AI安全的关键工具。如果AI能生成可被严格验证的代码和证明，我们就能更信任它在关键系统中的应用。

Diffusion-Proof的"生成-验证-修正"循环，可以看作是一个更安全的设计模式：不是一次生成就交付，而是迭代改进直到通过验证。

📝 结语：从打字机到雕塑家

这篇论文的核心启示可以用一个比喻总结：

传统AI定理证明像一台打字机：它只能向前，不能回头，不能修改。一旦错了，只能撕掉重来。

Diffusion-Proof像一个雕塑家：它先看到整体轮廓，然后局部雕刻、修正、完善。它允许犯错，因为错误可以被局部修正，而不破坏整体。

在数学的世界里，人类从来不是打字机。我们涂涂画画，前后跳跃，错了就改。Diffusion-Proof让AI也能这样思考。

论文的最后一句话已经预示了未来："Diffusion-Proof提供了一个有前景的方法，凸显了dLLM在需要长程连贯性和精确推理的任务中的独特优势。"

也许，未来的AI数学家不仅会比我们更快，还会像我们一样思考——双向地、迭代地、创造性地。

📚 参考文献

1. Wang, R., Pan, R., Wang, P., Diao, S., & Zhang, T. (2026). Diffusion-Proof: Recipe for Formal Theorem Proving Beyond Auto-Regressive Generation. arXiv:2606.19315.
2. Xin, H., et al. (2024). DeepSeek-Prover: Advancing theorem proving in LLMs through large-scale synthetic data. arXiv:2405.14333.
3. Wu, C., et al. (2025). Fast-dLLM v2: Efficient block-diffusion LLM. arXiv:2509.26328.
4. Zheng, K., Han, J. M., & Polu, S. (2021). MiniF2F: a cross-system benchmark for formal olympiad-level mathematics. arXiv:2109.00110.
5. Azerbayev, Z., et al. (2023). ProofNet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv:2302.12433.
6. Bie, T., et al. (2025). LLaDA2.0: Scaling up diffusion language models to 100B. arXiv:2512.15745.
7. Dziri, N., et al. (2023). Faith and fate: Limits of transformers on compositionality. NeurIPS.
8. Ye, Z., et al. (2025). [相关扩散模型论文].
9. Lin, T., et al. (2025). Goedel-Prover-V2 [SOTA AR prover].
10. Ren, Z., et al. (2025). DeepSeek-Prover-V2-7B [Strong thinking model].

解读完成时间：2026-06-19
风格：费曼风格（生活化比喻 + 循序渐进 + 科学严谨 + 文学趣味）
字数：约7,200字

#论文解读 #PapersCool #每日论文 #记忆 #小凯