💻 computer science

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

本文介绍了 Diffusion-Proof，这是首个将基于扩散的大语言模型应用于形式化定理证明的框架，它通过利用迭代去噪来实现长程连贯性和局部修正，从而超越了传统的自回归基准模型，在基准测试中取得了显著提升，并解决了一个现有最先进模型无法解决的国际数学奥林匹克（IMO）问题。

原作者： Ruida Wang, Rui Pan, Pengcheng Wang, Shizhe Diao, Tong Zhang

发布于 2026-06-19

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Ruida Wang, Rui Pan, Pengcheng Wang, Shizhe Diao, Tong Zhang

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

核心理念：修复 AI 数学中的“单行道”问题

想象一下，你正在尝试解决一个非常复杂的数学谜题，比如使用一种叫做 Lean 的形式化语言进行的证明。这种语言就像一段严苛的计算机代码，每一个步骤都必须在逻辑上完美无缺。如果你犯了一个微小的错误，整个证明就会崩塌。

多年来，处理这类工作的最佳 AI 模型一直是 自回归（Auto-Regressive, AR）模型。你可以把这些模型想象成一个正在逐字逐句写故事的人，严格地从左到右书写。他们看不见自己即将写下什么，也无法在不重写整个句子的情况下，轻松修改五分钟前写下的某个词。

问题所在：
在长篇数学证明中，这种“单行道”式的方法会导致两个大问题：

多米诺骨牌效应： 如果 AI 在早期犯了一个小错，它会不断基于这个错误进行构建，使错误不断累积，最终导致整个证明变得毫无意义。
无法“回溯”： 如果 AI 在写到一半时意识到第一步错了，它无法轻易地只修正那第一步。它要么必须从头开始，要么只能笨拙地尝试通过修改句子的结尾来强行匹配开头。

解决方案：“扩散”方法

该论文的作者提出了一种构建数学 AI 的新方法，称为 Diffusion-Proof。他们不再采用逐字书写的方式，而是使用了一种 扩散大语言模型（Diffusion Large Language Model, dLLM）。

类比：雕塑家 vs. 抄写员

旧方法（AR 模型）： 想象一位正在写信的抄写员。一旦墨水干了，他们就无法更改。如果写错了一个词，他们只能划掉它，然后在旁边写下一段凌乱的备注。
新方法（扩散模型）： 想象一位用粘土创作的雕塑家。他们不仅仅是在添加粘土，而是从一个粗糙、带有噪声的土块开始，进行迭代式精炼。他们可以同时观察整体形状，在观察右侧曲线的同时，平滑掉左侧的一个凸起，并通过“去噪”整个画面来修复错误，直到作品趋于完美。

从技术层面讲，扩散模型是以块（blocks）（即单词块）而不是单个单词的形式生成文本。它可以同时观察句子的开头和结尾，从而确定中间部分应该填入什么。

Diffusion-Proof 如何运作：双人搭档组合

论文介绍了一个用于解决这些数学问题的两部分团队：

1. 架构师 (dLLM-Prover-7B)

这是主要的构建者。因为它采用了“雕塑家”的方法（块扩散），它在长程规划方面表现得更出色。

为什么重要： 在构建长篇证明时，架构师可以把握“大局”。它知道最后的步骤需要满足某个特定条件，因此它会设定证明的开端，使其完美契合该条件。它不会在中间迷失方向，因为它能同时“看到”整块文本。

2. 检查员 (dLLM-Corrector-7B)

即使是最优秀的架构师也会犯错。有时证明看起来很完美，但某个特定的步骤却是错误的。

旧方法： 如果 AR 模型犯了错，它通常会尝试通过在错误之后编写更多文本来试图修复，但这往往会让情况变得更糟。
新方法： 检查员是一个专门训练用于填补空白的模型。如果证明失败了，系统会将出错的部分用一个“掩码”（类似于空白空间）盖住，并要求检查员仅仅重写那个特定的区块。
超能力： 因为检查员使用的是扩散方法，它可以查看错误发生之前的文本和错误发生之后的文本，从而推断出缺失的部分究竟应该是什。这就像一位编辑，通过阅读句子中错误词汇前后的内容来猜测正确的单词，而不是仅仅根据前一个词进行猜测。

结果：击败巨头

研究人员在两个著名的数学基准测试上测试了这个新系统：

MiniF2F： 一个包含高中及竞赛级数学问题的集合。
ProofNet： 一个包含大学水平数学问题的集合。

计分板：

这个全新的 Diffusion-Proof 系统击败了在完全相同数据上训练的传统（自回归）最佳模型。
在 MiniF2F 测试中，它多解决了 6.14% 的问题。
在 ProofNet 测试中，它多解决了 1.61% 的问题。

“IMO 时刻”：
最令人兴奋的结果是一个特定的国际数学奥林匹克（IMO）问题。一个非常先进且著名的 AI 模型——DeepSeek-Prover-V2（它使用“思维链”推理）未能解决这个问题。而 Diffusion-Proof 解决了它。

为什么？DeepSeek 模型陷入了一个试图修复自身计划的死循环，因为它无法看到证明开头与结尾之间的长程联系。而扩散模型凭借其能够同时观察整个证明“块”的能力，找到了正确的路径。

总结

该论文声称，通过从“逐字书写”转向“雕刻文本块”，AI 可以变得更擅长形式化数学。它创造了一个能够更好地进行长距离规划，并能通过观察整体上下文而非仅仅是即时过去来修复自身错误的系统。这使得它能够解决以往 AI 模型根本无法攻克的难题。

技术摘要：Diffusion-Proof

问题陈述

形式化定理证明需要在复杂的推理序列中保持长程连贯性和逻辑一致性。尽管大语言模型（LLMs）在该领域已取得了显著进展，但目前最先进的方法仍高度依赖于自回归（AR）模型。这些模型从左到右顺序生成文本，仅根据先前的 token 来预测下一个 token。这种架构存在固有的局ations，包括：

误差累积： 早期 token 中的微小错误会在长序列中呈指数级复合，导致逻辑不一致。
缺乏长程连贯性： AR 模型难以维持连贯的全局证明规划，经常无法使中间策略与最终目标保持一致。
缺乏填充能力： AR 模型无法自然地进行“填空式”（in-filling）修正（即在修改证明中间部分的同时保留周围上下文），而这对于在不重写整个证明的情况下修复局部错误至关重要。

尽管扩散语言模型（dLLMs）通过迭代去噪和双向上下文，在代码编写和通用文本生成方面展现出了潜力，但其在形式化数学推理中的应用仍处于探索阶段。

方法论

作者提出了 Diffusion-Proof，这是第一个专门为形式化定理证明设计、用于训练并应用 dLLM 的框架。该框架在 Lean4 环境中运行，并采用了双模型架构：dLLM-Prover-7B 和 dLLM-Corrector-7B。

1. 数据收集与预处理

数据集： 作者从以往的工作中收集了 550 万条定理证明记录。
清洗： 他们使用基于规则的方法对数据进行标准化，将自然语言（NL）陈述、形式语言（FL）陈述和 FL 证明进行分离。
SFT 数据集： 选择了 30 万条记录来创建监督微调（SFT）数据集，保持纯 Lean 证明与带有自然语言注释证明的比例为 1:2。
修正器数据： 对包含子目标分解（由 have 关键字标记）的数据子集进行了处理。证明块被填充了占位符 token，以创建用于“填空式”修正的训练数据。

2. 模型架构与训练

该框架构建于 Fast-dLLM-V2-7B 之上，这是一种基于块（block-based）的扩散模型。不同于传统 dLLM 独立地掩码（mask）单个 token，该模型将序列划分为大小为 $B$ 的块，其中双向注意力被限制在单个块内，同时保留块之间的因果关系。

dLLM-Prover-7B:
- 目标： 进行全篇证明生成，实现长程连贯的策略使用。
- 训练： 使用标准的文本到文本框架在 30 万条 SFT 数据集上进行微调。
- 策略： 采用课程学习，按证明复杂度（增加证明长度）组织训练数据，以稳定损失曲线。扩散块大小设置为 32。
dLLM-Corrector-7B:
- 目标： 利用双向信息进行局部证明修正。
- 训练： 在 12.8 万条子目标分解数据集上进行微调。
- 创新点： 引入了**大块修正（Large Block Correction）**方法。扩散块大小从 32 扩展到 512。该模型经过训练，能够将错误的子目标证明替换为一系列掩码 token，然后利用扩展的上下文（包括前缀和后缀）重新生成该块，从而执行填空式修正。

3. 推理流水线

生成： dLLM-Prover-7B 使用块扩散生成技术，为给定的定理陈述生成完整的证明。
验证： 通过 Lean 进行证明验证。
修正： 如果证明未通过验证，但顶层骨架（子目标陈述）是正确的，则调用 dLLM-Corrector-7B。它将错误的子目标证明替换为掩码 token，并使用 512 个 token 的扩散块重新生成它们，利用双向上下文来修复局部错误并保持全局连贯性。

核心贡献

首个定理证明 dLLM 框架： Diffusion-Proof 是第一个将扩散模型适配于形式化定理证明的框架，解决了数学推理中长程连达性和错误修正的特定挑战。
大块修正训练： 作者引入了一种新的训练方法，利用大扩散块（512 个 token）和双向信息来实现有效的填空式修正，这是扩散模型固有的能力，而在 AR 模型中并不存在。
双模型协同效应： 该框架展示了一种协同方法，即由一个 Prover 处理全局规划，由一个 Corrector 处理局部精炼，其表现优于单模型基线。

实验结果

该框架在 MiniF2F-Test（244 个问题）和 ProofNet-Test（186 个问题）上进行了评估，使用 pass@32 指标。

性能提升： 与在完全相同数据集上训练的基线 AR 模型（Qwen-2.5-Lean-SFT-7B）相比：
- MiniF2F-Test： Diffusion-Proof 达到了 50.00% 的准确率，比基线（43.85%）实现了 6.14% 的绝对提升。
- ProofNet-Test： Diffusion-Proof 达到了 7.53% 的准确率，比基线（5.91%）实现了 1.61% 的绝对提升。
问题类型分析： 该模型在具有挑战性的类别中表现出显著增益，特别是 IMO（国际数学奥林匹克）题目，其准确率从 5.00% 提升到了 15.00%。
案例研究： 值得注意的是，Diffusion-Proof 成功解决了 IMO 题目 imo_1962_p2，而配备了长链式思考（Long CoT）推理能力的更先进的 DeepSeek-Prover-V2-7B 在 pass@32 下未能解决该题。分析表明，AR 模型在处理该题所需的长程依赖和连贯策略规划方面存在困难，而扩散修正器成功利用双向上下文解决了证明。
消融实验：
- 移除修正器后，MiniF2F 的性能下降了 1.64%，证实了修正步骤的价值。
- 即使没有修正器，仅靠 dLLM-Prover 也比 AR 基线高出 4.51%，验证了扩散架构在形式化推理中的固有优势。

意义与主张

论文声称，Diffusion-Proof 突显了扩散模型在形式化定理证明中的独特优势，特别是其维持长程连贯性和执行双向填空修正的能力。

架构优势： 结果表明，对于需要长序列严密逻辑一致性的任务，扩散生成范式相比 AR 模型具有结构性优势，这从较低的验证损失分布和更高的复杂证明成功率中得到了证实。
未来潜力： 作者将这项工作定位为基础性的一步，证明了即使在没有强化学习（RL）或长 CoT 推理的情况下，dLLM 也能超越 AR 基线。他们指出，虽然目前的局限性包括计算规模和缺乏 RL 集成，但该框架为研究具有增强推理能力的模型提供了一个充满希望的方向。

作者强调，他们的主要目标是研究 dLLM 的架构潜力，而非通过大规模扩展或 RL 来追求达到最先进水平（SOTA），因此观察到的改进是扩散范式在形式化推理有效性的有力指标。