自回归证明定理总在"走着走着就崩了"，他们干脆把生成范式换成了扩散

一个让我盯着 Table 3 看了好久的结论：在最长的那批证明上，扩散模型把基线拉开了将近一倍。

先说个我自己调形式化证明模型时的真实困扰。

你让一个 7B 的 prover 去证 Lean 里的定理，它前面几步走得有模有样，子目标拆得也对，结果到第七八步突然冒出一个方向反了的不等式，或者一个在自然数域里根本不该用的 linarith，整个证明就这么崩了。回头看，错误往往不是出在"不会"，而是出在"它写到后面时，已经忘了前面给自己挖的坑"。

这就是自回归（Auto-Regressive, AR）生成的老毛病——逐 token 从左到右预测，没有回头看的机会，错误会沿着序列一路累积，长程一致性（long-range coherence）越往后越难维持。在写一句话、答一道选择题的时候这不算什么，但形式化定理证明是出了名的"一步错步步错"——Lean 编译器可不会因为你前面九步漂亮就放过第十步的类型错误。

这篇来自 UIUC（Tong Zhang 组）的 Diffusion-Proof，给的方案挺干脆：既然 AR 的问题出在生成范式本身，那就别用 AR 了，换成扩散语言模型（diffusion LLM, dLLM）来写证明。

论文地址：https://arxiv.org/abs/2606.19315

🎯 核心摘要

形式化定理证明这两年是数学和 CS 社区的共同热点，但主流 prover 全是 AR 架构，受困于长程一致性差、错误累积两个固有缺陷。Diffusion-Proof 是（据作者所知）第一个把扩散语言模型用于形式化定理证明的框架，它训了两个 7B 模型协同工作：dLLM-Prover-7B 负责"整证明书写"，靠块扩散维持长程连贯的战术使用；dLLM-Corrector-7B 是个新颖的大块扩散纠错模型，利用扩散天然的双向填空（in-filling）能力做局部修补。

在完全相同的训练数据和方法下，它比 AR 基线在 ProofNet-Test 上绝对涨 1.61 个点、在 MiniF2F-Test 上涨 6.14 个点。最扎眼的是，它解出了一道连带 Long CoT 的 DeepSeek-Prover-V2-7B 都搞不定的 IMO 题。

我的判断：这篇论文真正值钱的地方不在那几个点的 SFT 涨幅，而在它用一个干净的受控实验，把"扩散在长程推理上确实比 AR 有结构性优势"这件事给坐实了——尤其是 Table 3 那个长证明子集的对比。

📖 先把"为什么是扩散"讲明白

要理解这篇论文，得先搞清楚 AR 和扩散到底差在哪。我尽量用大白话讲。

AR 模型，就是 GPT 那套：给定前面的 token \(\bm{x}[0:i-1]\)，预测下一个 token \(x_i\)，严格从左到右，一锤子买卖。它的训练目标就是标准的交叉熵：让模型对"下一个词"猜得越准越好。问题是，生成的时候它没法回头改——第 5 个 token 写错了，第 6 到第 100 个都得在这个错误的基础上往下走。

扩散 LLM（dLLM）则是另一套思路，借鉴了图像扩散模型的"去噪"逻辑。它引入一个时间步 \(t\)，先按概率把一部分 token 替换成 [MASK]（加噪），然后让模型从这个"残缺的句子"里把被遮住的 token 还原出来（去噪）。训练目标是只在被 mask 的位置上算 loss：

关键差别在这里：dLLM 解码时能同时看到一个 token 的前文和后文（双向信息），而且是迭代式精炼——一轮去噪不满意可以再来一轮。这俩特性，恰好对上了形式化证明的两个痛点：双向信息帮你维持长程一致性，迭代精炼让你有机会修正局部错误。

不过纯扩散也有代价——它天生不像 AR 那样能任意长度地往下生成。所以 Diffusion-Proof 用的是块扩散（block diffusion）这个折中方案：把序列切成大小为 \(B\) 的块，块内双向注意力、块间保持因果关系，推理时逐块迭代解码直到停止。说白了就是"局部用扩散、全局像 AR"，既拿到了双向精炼的好处，又保留了 AR 那种能写任意长证明的灵活性。

顺带提一句，块扩散这个底座并不是这篇论文发明的，它用的基础模型是 Fast-dLLM-V2-7B，而后者的 base 又是 Qwen-2.5-Instruct-7B。这个谱系关系很重要，下面讲基线选择时你会看到为什么。

🏗️ 方法：两个模型，各干各的

Diffusion-Proof 的整体框架就是下面这张图，建议对着看。

图1：(a) 数据收集与模型训练流程——从 5.5M Lean 数据集清洗筛出 300k 的 NL-FL 混合数据，微调 Fast-dLLM-V2-7B 得到 dLLM-Prover；再从带子目标分解的数据做"块填充"构造纠错训练数据，进一步训出 dLLM-Corrector。(b) 推理时的书写与纠错——Prover 用块扩散生成完整证明，若 Lean 验证失败但子目标骨架正确，就交给 Corrector 用大扩散块做局部修补。右上角两个黄色框分别是 Prover 和 Corrector 的训练样本示例。

整个流程的精髓是把全局书写和局部纠错分成两个模型。为什么要分开？后面消融实验会给出很有说服力的证据，先按下不表。

dLLM-Prover-7B：负责把证明从头写到尾

数据这块，作者从已有工作里收集了 5,595,798 条代码补全式证明记录，采样出 300k 条做 SFT。有个细节我觉得挺讲究——纯 Lean 证明和带自然语言（NL）注释的证明，比例大约是 1:2。也就是说三分之二的训练数据是"边写证明边带自然语言思路"的，这对维持长程规划应该有帮助。

训练上沿用 DeepSeek-Prover 的代码补全风格，不套 chat template。扩散块大小保持在 32（和原模型一致，为了训练稳定）。还有一个我比较认可的做法：课程式数据排序（curriculum data sorting），按证明长度从短到长喂给模型，先学简单的再啃复杂的，让 loss 曲线更平稳。这个 trick 在很多长序列训练里都被验证有效。

dLLM-Corrector-7B：专门做"大块填空式"修补

这是论文最新颖的部分。Corrector 是在 Prover 基础上接着训的，但干了件很关键的事——把扩散块大小从 32 一口气扩到 512。

为什么要扩这么大？因为纠错往往要重写一整段子目标证明，32 个 token 的小块根本装不下。Lean 里的子目标用 have 关键字标记，作者把顶层子目标证明组织成大小为 256 的 token 块，用占位符 <|fim_middle|> 填充，每次只处理一个块。训练时对子目标证明块和占位符 token 同时施加 loss，逼着模型学会"在一个大块里既写出正确的局部证明、又把剩余空间用占位符填满"。最终构造了 128k 条 corrector 训练数据。

下面这张图是 Corrector 训练数据的样子，能直观看到那个"大扩散块覆盖纠错窗口"是怎么回事：

图6：Corrector 的训练数据示例。被标注的目标纠错块（如 h3）被组织进一个大扩散块里，这个块同时覆盖了它的前缀和后缀上下文——这正是双向信息能发挥作用的地方。模型要学的就是在掩码区域填入正确的子目标证明。

推理：先写，崩了再修

推理流程分两段：

第一段，整证明书写。dLLM-Prover-7B 拿到定理的 NL 和 Lean4 语句，用块扩散一次性生成完整证明，方法基于 DeepSeek-Prover-V1。

第二段，触发纠错。这里有个明确的触发条件——初始证明没过 Lean 验证，但所有顶层子目标的语句和用法都是对的。换句话说，骨架对了、只是某个子目标的内部证明写挂了。这时候：

1. 删掉出错的那段子目标证明；
2. 用 256 个 <|MASK|> token 替换它；
3. dLLM-Corrector-7B 用 512 长度的扩散块，结合前缀和后缀的双向上下文，把这个掩码区域重新填好。

推理超参也有点意思：生成温度 1.2（鼓励更有创造性的证明书写），去噪置信度阈值提到 0.95（保证鲁棒性）。温度拉到 1.2 这个值在 prover 里算偏高的，作者的逻辑是形式化证明需要更大的探索空间。

🧪 实验：相同数据下，扩散确实更能打

实验设计我得先夸一句——基线选得很干净。

基线是 Qwen-2.5-Lean-SFT-7B，用完全相同的 300k 数据集、完全相同的 text-to-text 方法微调出来的。而且它的 base 模型 Qwen-2.5-Instruct-7B 正好就是 Fast-dLLM-V2-7B 的 base。这意味着 AR 和扩散两边，除了"生成范式"这一个变量，其他几乎全控住了。这种受控对比，远比"我比 SOTA 高几个点"有说服力。

评测在两个标准基准上：MiniF2F-Test（244 道，IMO/AIME/AMC + Math-500 子集 + 手工题）和 ProofNet-Test（186 道大学教材定理，含实复分析、线代、拓扑）。指标用 pass@32，每个可纠错定理额外做 32 次纠错。双方都不允许 Long CoT。

主实验

MiniF2F 涨 6.14 个点，到 50%，这个幅度在同数据 SFT 对比里相当能打了。按题型拆开看更有意思：

代数题涨了 11.36 个点，IMO 翻了三倍（虽然基数小，从 1 道到 3 道）。AIME 和 Induction 原地踏步——这俩要么题太难要么样本太少，扩散也没辙。

跟更广的基线比（非受控）

作者也老老实实放了一张"非受控对比"表，并明确说了各系统在数据规模、RL、搜索、Long CoT 上都不一样，不能直接比。我觉得这个态度值得点赞。

看明白了吗？Diffusion-Proof 只用了 300k 数据做标准 SFT，没上 RL、没上 Long CoT，就摸到了 DeepSeek-Prover-V1.5（SFT + RL）的水平。这说明换生成范式带来的增益，跟堆 RL、堆 CoT 的增益某种程度上是正交的——理论上你完全可以在扩散底座上再叠 RL，那才是真正值得期待的组合。

🔬 我最看重的一张表：长证明子集

如果整篇论文只让我留一个证据，我会留 Table 3。

在最长的那 50% 证明里，扩散把 18.52% 拉到了 24.07%，差距明显比整体大。这正好印证了开篇那个直觉——AR 的错误累积在长序列上才最致命，而扩散的长程一致性优势也正是在长证明上才真正兑现。这不是巧合，是机制层面的因果。

📊 消融：为什么必须是"两个模型"

这部分回答了前面埋的伏笔——为什么不用一个统一模型，非要拆成 Prover 和 Corrector？

双模型设计与纠错策略（Table 4，MiniF2F-Test）

几个结论很硬：

第一，统一模型只有 40.98%，反而最差。原因是大块纠错训练（把块扩到 512）虽然改善了局部填空能力，但损害了首次整证明生成的能力。这就解释了为什么必须分家——一个模型很难同时擅长"从零写"和"打补丁"这两件需求相反的事。

第二，光是 dLLM-Prover 单独干，就有 48.36%，已经超基线 4.51 个点。Corrector 再补上 1.64 个点到 50%。

第三，纠错策略上，顶层纠错（重生成整个顶层子目标证明）解 4 题，明显优于原地纠错的 2 题。作者的解释是顶层纠错给了模型更大的修订自由度。而 AR 基线那套"从首个错误前一行重写"的纠错只修对了 1 题，而且那题 dLLM-Prover 一遍就过了。

验证损失分析：一个反直觉的发现

这块挺烧脑但很关键。作者拿 DeepSeek-Prover-V2 完成的 190 道正确 Lean 证明，把所有模型都强制设成纯因果掩码（dLLM 把扩散块大小设为 1，退化成 AR），然后比交叉熵 loss。

图3：四个模型在因果掩码下的验证损失分布。蓝色（Trained Autoreg）和红色（Trained Diffusion）几乎完全重叠，均值都在 0.41 附近；橙色（Base Autoreg）和绿色（Base Diffusion）也几乎重叠，均值在 0.74 附近。微调把两类模型都从 0.74 拉到了 0.41。

统计结果是：两个 SFT 模型之间的 Pearson 相关系数高达 0.9846，两个 base 模型之间 0.9838，p 值都小于 \(10^{-100}\)。

这说明什么？在纯因果（AR 模式）的 loss 上，扩散模型和 AR 模型几乎等价——也就是说，扩散模型并没有因为架构不同就学到了"更好的 token 级预测能力"。

那它凭啥在实际证明上赢这么多？作者的归因是：优势不来自更强的逐 token 预测，而来自扩散生成模式本身——迭代精炼、长程一致性、双向信息感知。这个发现我觉得相当漂亮，它把"扩散的增益到底来自哪"这个问题给做实了：不是模型变聪明了，是生成方式变好了。这也反过来印证了 Table 3 的长证明结论。

说实话，看到 0.9846 这个相关系数的时候我愣了一下。直觉上你会觉得扩散模型既然表现更好，loss 应该也更低才对。但人家偏不——loss 一模一样，赢在生成范式。这种"控制变量控到这个份上"的实验，是我愿意相信这篇论文结论的主要原因。

💡 那道 IMO 题：扩散的"杀手锏"案例

论文花了不少篇幅讲 imo_1962_p2 这道题——Diffusion-Proof 证出来了，而带 Long CoT 推理的 DeepSeek-Prover-V2-7B 在 pass@32 下没证出来。

DS-Prover-V2 的问题在于：它在自然语言层面的分析其实很充分，但缺乏详细的证明计划和连贯的战术使用，在 NL 计划里反复自我纠正，却没能给 Lean 层面带来额外洞察。具体崩在第二种情况——它在 h19 里给了个方向反了的不等式，整个证明就塌了。这不就是开篇说的那个"方向反了的不等式"嘛，AR 的通病。

而 Diffusion-Proof 的 Corrector 靠大扩散块的双向信息，把这个长程依赖处理对了。这个案例的价值在于，它不是靠"模型更大"或"算力更多"赢的，而是靠生成范式本身的结构优势——这恰恰是这篇论文想证明的核心论点。

其他几个小案例也都指向同一个方向：mathd_numbertheory_521 里，原证明在自然数域错用了 linarith，Corrector 改成了更合适的 omega，而且有意思的是 h6 的证明竟然在 h4 之前生成——这只有双向感知才做得到。

🤔 我的判断：值得读，但别神化

先说亮点。

这篇论文最大的贡献不是那几个 SFT 点数，而是第一次用一个干净的受控实验，把"扩散在形式推理上对 AR 的结构性优势"给量化、给坐实了。尤其是验证损失分析那段——证明优势来自生成范式而非 token 预测能力——这个洞察的价值超过实验数字本身。Table 3 的长证明对比则从应用侧给了对应的证据，逻辑闭环很完整。双模型分工的设计也有扎实的消融支撑，不是拍脑袋。

再说几个我皱眉的地方。

第一，绝对数值还不高。 ProofNet 才 7.53%，MiniF2F 50%。跟带 RL 和 Long CoT 的 DeepSeek-Prover-V2 的 70.49% 比，差着一大截。当然作者也承认了这是非受控对比，但读者得清楚：这篇是"换范式的可行性验证"，不是"屠榜"。

第二，没上 RL。 整篇都是 SFT。形式化证明现在的 SOTA 基本都靠 RLVR + Long CoT 堆出来，扩散底座能不能吃得下 RL、吃下去之后增益是否还能叠加，这是个大问号。我个人最期待的恰恰是这个组合，但论文没碰。

第三，纠错的适用面有限。 Corrector 在 ProofNet 上一道题都没多解出来，因为 ProofNet 偏高级知识、子目标划分没那么复杂。也就是说大块纠错这套主要在"骨架对、局部错"的场景才生效，覆盖面没那么广。

第四，推理成本。 完整流水线评测约 16 小时，虽然论文也提到 dLLM 相比 AR 有 2.54x 的推理加速，但整体流程引入了 Prover + Corrector 两段，工程复杂度上去了。

工程上的启发我觉得很明确：如果你在做长序列、强一致性要求的结构化生成（不只是定理证明，代码生成、复杂 SQL、长程 agent 规划都算），AR 的错误累积是真实存在的天花板，扩散/块扩散是一个值得认真试的方向。而且这篇用 Fast-dLLM-V2-7B 做底座、标准 SFT 就能跑起来，复现门槛不算高。

最后留个更本质的问题：扩散到底是 AR 的替代品，还是补充品？这篇论文给的答案偏向"在特定场景下是更好的替代"。但我更倾向于认为，未来真正能打的，可能是"扩散底座 + RL + 搜索"的缝合体——这篇只是把第一块拼图摆上了桌。

（arXiv ID：2606.19315，作者 Ruida Wang、Rui Pan、Pengcheng Wang、Shizhe Diao、Tong Zhang）

觉得有启发的话，欢迎点赞、在看、转发。跟进最新AI前沿，关注我