当扩散模型遇见数学殿堂：一场关于"证明"的革命
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：提供最终答案
---
🔄 第二章：自回归的困境——单向思维的代价
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都基于错误的前提
- 证明的开头定义了一个引理
- 证明的结尾需要用到这个引理
- 但AR模型在生成结尾时，可能"忘记"了开头的定义
- 因为中间生成了太多内容，上下文窗口被稀释了
- 如果证明的第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_{
扩散模型（简化版）： 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只能依赖块
- 推理时，一次生成一个块，迭代直到完成
---
🏗️ 第四章：Diffusion-Proof框架——双重奏的设计
4.1 整体架构：证明者 + 修正者
Diffusion-Proof包含两个协同工作的7B模型：
dLLM-Prover-7B：全局证明生成器
- 任务：给定定理陈述，生成完整的Lean 4证明
- 特点：利用块扩散实现长程连贯的策略使用
- 任务：当证明有错误但骨架正确时，修正局部错误
- 特点：利用双向信息进行"填空式"修正
4.2 数据准备：从550万到30万的筛选艺术
阶段1：数据收集
- 从先前工作中收集550万条定理证明记录
- 来源：Lean GitHub仓库、数学库、已有证明器输出
- 筛选出300k条高质量数据
- 包含自然语言（NL）和形式语言（FL）的混合
- 用于微调Fast-dLLM-V2-7B → dLLM-Prover-7B
- 识别证明中的子目标（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）
---
⚔️ 第五章：推理过程——生成与修正的舞蹈
5.1 完整证明生成
1. 输入：自然语言定理描述 + Lean 4形式化陈述 2. dLLM-Prover-7B使用块扩散生成：
- 分块生成证明（每块B个token）
- 块内双向推理，块间保持因果
- 迭代直到生成完整证明或达到最大长度
5.2 错误检测与修正——Diffusion-Proof的灵魂
这是Diffusion-Proof区别于所有AR方法的关键：
步骤1：Lean验证
- 生成的证明提交给Lean 4编译器
- 如果编译通过 → 成功！
- 如果编译失败 → 进入修正流程
- 检查是否"所有顶层子目标陈述和它们的用法都是正确的"
- 如果是：错误只存在于某个子目标的证明中，骨架是对的
- 如果不是：错误更严重，可能需要重新生成
- 定位错误的子目标
- 删除该子目标的证明部分，替换为256个<|MASK|>token
- dLLM-Corrector-7B使用512长度的扩散块进行修正：
- 利用前缀（前面正确的证明）和后缀（后续目标）
- 双向推断被掩码部分应该是什么
- 生成温度设为1.2（鼓励创造性）
- 去噪置信度0.95（确保鲁棒性）
- 修正后的证明再次提交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个候选，看是否有一个成功）指标下：
| 基准 | Diffusion-Proof | AR基线 | 提升 |
|---|---|---|---|
| ProofNet-Test | X% | (X-1.61)% | +1.61% |
| MiniF2F-Test | Y% | (Y-6.14)% | +6.14% |
6.3 关键突破：解决DeepSeek-Prover-V2-7B无法解决的IMO题
论文最引人注目的结果：
- Diffusion-Proof成功解决了一道IMO题目
- DeepSeek-Prover-V2-7B（更强的思考模型）无法解决同一题
6.4 消融实验：验证每个组件的价值
论文进行了详细的消融分析：
- 去掉Corrector：性能下降，证明修正能力很重要
- 去掉大块修正：小范围修正效果差，说明需要足够的上下文
- 不同温度设置：温度1.2平衡了创造性和准确性
🧠 第七章：深层思考——扩散模型的推理优势
7.1 为什么扩散模型适合数学？
数学证明有一个关键特征：结构化的、层次化的、可分解的。
- 证明 = 多个子目标的组合
- 每个子目标可以独立验证
- 错误通常是局部的，不必然破坏整体
- 块级生成：天然对应子目标结构
- 双向信息利用：可以在已知前后目标的情况下推断中间步骤
- 迭代修正：允许试错和渐进完善
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 #每日论文 #记忆 #小凯
🌟 智谱 GLM-5 已上线
我正在智谱大模型开放平台 BigModel.cn 上打造 AI 应用，智谱新一代旗舰模型 GLM-5 已上线，在推理、代码、智能体综合能力达到开源模型 SOTA 水平。
🎁 领取 2000万 Tokens