Diffusion-Proof：以扩散大模型重构形式化定理证明的长程连贯性范式

在人工智能与数学交叉的前沿领域，提升大语言模型的形式化数学推理能力已成为学术界与工业界共同关注的核心议题。尽管近年来基于自回归（Auto-Regressive, AR）的大语言模型在形式化定理证明方面取得了显著进展，但其固有的生成机制限制了性能的进一步突破。自回归模型依赖逐词预测，这种串行生成方式在面对复杂的数学证明时，极易因长程连贯性缺失而导致策略不一致，且随着证明序列的延长，微小的预测误差会不断累积，最终导致证明失败。针对这一痛点，扩散大语言模型（diffusion LLMs, dLLMs）因其通过迭代去噪生成多词块文本的特性，展现出处理长程依赖的潜力。然而，目前关于dLLM在形式化数学这一对长程连贯性要求极高的领域的应用研究仍极为匮乏。为此，本研究提出了Diffusion-Proof，据我们所知，这是首个专门针对形式化定理证明进行训练和应用的扩散大语言模型框架，旨在通过全新的生成范式突破自回归模型的瓶颈。

Diffusion-Proof框架在技术实现上创新性地设计了两种互补的模型架构，以充分发挥扩散模型的优势。首先是dLLM-Prover-7B，该模型专注于整体证明的生成，利用扩散模型在去噪过程中对全局上下文的感知能力，确保在整个证明过程中策略使用的长程连贯性，避免了自回归模型常见的"顾此失彼"现象。其次是dLLM-Corrector-7B，这是一种基于大块扩散（large block diffusion）的修正模型，其核心创新在于利用了扩散模型强大的上下文填充（in-filling）能力。与传统自回归模型只能从左向右生成不同，dLLM-Corrector-7B能够利用证明片段左右两侧的双向信息，对局部证明步骤进行精准修正。这种双向推理机制使得模型能够在发现逻辑错误时，结合前后文的语义约束，高效地重构局部证明块，从而显著提高了证明的鲁棒性和正确率。训练策略上，框架结合了整体生成与局部修正的双重优化目标，使模型既能宏观把握证明结构，又能微观修正逻辑细节。

为了验证Diffusion-Proof的有效性，研究者在多个权威基准数据集上进行了广泛的实验评估，包括ProofNet-Test和MiniF2F-Test。实验设置严格控制变量，确保对比基线是在相同数据集上训练的自回归大语言模型。关键结果显示，Diffusion-Proof在性能上显著超越了自回归基线。具体而言，在ProofNet-Test基准上，Diffusion-Proof实现了1.61%的绝对性能提升；而在更具挑战性的MiniF2F-Test基准上，提升幅度达到了6.14%。这一差距在形式化证明领域具有统计学上的显著意义，表明扩散模型在处理复杂数学逻辑时具有更优的稳定性。此外，消融实验进一步揭示了局部修正模块的重要性，证明了双向信息利用对于纠正长程证明中的细微错误至关重要。

更令人瞩目的是，Diffusion-Proof成功解决了一道国际数学奥林匹克（IMO）级别的难题，而此前被认为更先进的思考模型DeepSeek-Prover-V2-7B未能解决该问题。这一案例强有力地证明了Diffusion-Proof在处理高难度、高连贯性要求数学推理任务时的独特优势。Diffusion-Proof的提出对形式化验证、自动推理及开源社区具有深远的行业意义。首先，它为突破自回归模型在长程逻辑推理中的性能天花板提供了新的技术路径，证明了扩散模型在结构化、逻辑密集型任务中的巨大潜力。对于工业落地而言，该框架有助于提升代码生成、形式化验证工具及智能数学助手的可靠性，特别是在需要严格逻辑一致性的场景中。对于开源社区，Diffusion-Proof开源了首个针对形式化证明优化的dLLM训练与推理框架，降低了后续研究者探索扩散模型在逻辑推理领域应用的门槛。未来，随着扩散模型架构的进一步优化，Diffusion-Proof所确立的整体生成与局部修正相结合的方法论，有望推广至其他需要长程依赖建模的领域，如复杂代码生成、法律文本分析等，推动人工智能在逻辑推理能力上的实质性飞跃。