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

📄 arXiv: 2606.19315v1 📥 PDF

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

分类: cs.LG

发布日期: 2026-06-17

💡 一句话要点

提出Diffusion-Proof以解决形式定理证明中的长程一致性问题

🎯 匹配领域: 支柱五：交互与反应 (Interaction & Reaction) 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 形式定理证明 大型语言模型 扩散模型 长程一致性 局部校正 自动推理 数学推理

📋 核心要点

  1. 现有自回归LLMs在形式定理证明中面临长程一致性和错误累积的挑战，导致性能不佳。
  2. Diffusion-Proof框架首次将扩散LLMs应用于形式定理证明，通过长程一致性和局部校正提升推理能力。
  3. 实验结果显示，Diffusion-Proof在多个基准测试中显著超越AR LLM基线，且成功解决了更先进模型无法解决的问题。

📝 摘要（中文）

近年来，增强大型语言模型（LLMs）在形式数学推理方面的能力成为数学和计算机科学领域的重点。尽管自回归（AR）LLMs在形式定理证明中取得了显著进展，但其生成方法存在长程一致性和错误累积的固有局限性。本文提出了Diffusion-Proof，这是首个将扩散LLMs（dLLMs）应用于形式定理证明的框架，包含了两个模型的训练和推理方法。实验结果表明，Diffusion-Proof在ProofNet-Test和MiniF2F-Test基准上相较于AR LLM基线有显著提升，展示了dLLMs在形式定理证明中的独特优势。

🔬 方法详解

问题定义：本文旨在解决自回归LLMs在形式定理证明中由于长程一致性不足和错误累积导致的性能问题。现有方法在处理复杂推理时表现不佳，限制了其应用范围。

核心思路：Diffusion-Proof框架通过引入扩散LLMs，利用其迭代去噪的特性，增强了长程一致性和局部校正能力，从而提高了形式定理证明的效果。

技术框架：该框架包括两个主要模型：dLLM-Prover-7B用于整体证明生成，dLLM-Corrector-7B用于局部校正。训练和推理过程均针对这两个模型进行了优化，以确保其在形式数学推理中的有效性。

关键创新：Diffusion-Proof是首个将扩散LLMs应用于形式定理证明的框架，突破了传统自回归生成方法的局限，展现了在长程推理中的优势。

关键设计：在模型设计中，dLLM-Prover-7B采用了长程一致性策略，而dLLM-Corrector-7B则利用双向信息进行局部校正。训练过程中，损失函数和参数设置经过精心调整，以优化模型性能。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，Diffusion-Proof在ProofNet-Test基准上相较于AR LLM基线提升了1.61%，在MiniF2F-Test基准上提升了6.14%。此外，Diffusion-Proof成功解决了一个IMO问题，而更先进的DeepSeek-Prover-V2-7B未能解决，显示了其独特优势。

🎯 应用场景

该研究的潜在应用领域包括自动定理证明、数学教育辅助工具以及智能推理系统。通过提升形式定理证明的准确性和效率，Diffusion-Proof能够为数学研究和计算机科学提供有力支持，推动相关领域的发展。

📄 摘要（原文）

Enhancing the formal math reasoning capabilities of Large Language Models (LLMs) has become a key focus in both mathematical and computer science communities in recent years. While significant progress has been made in using state-of-the-art Auto-Regressive (AR) LLMs for formal theorem proving, these models suffer from inherent limitations. Their next-token prediction generation methods may yield suboptimal performance due to the challenges of long-range coherence and the compounding of errors over long sequences. Recent advancements in diffusion LLMs (dLLMs), which generate text through iterative denoising of a multi-token block, offer a promising alternative. However, the application of dLLMs to formal mathematics, where maintaining long-range coherence is critical, remains largely understudied. To address the challenges above, we propose Diffusion-Proof, to the best of our knowledge, the first framework to train and apply dLLMs for formal theorem proving. Our frameworks contain training and inference methods for two models. The first one is dLLM-Prover-7B, which performs whole-proof writing with long-range coherent tactic usage. The second one is dLLM-Corrector-7B, which is a novel large block diffusion-based correction model. It leverages the in-filling capabilities of dLLMs to perform local proof correction using bi-directional information. Extensive experiments demonstrate that Diffusion-Proof relatively significantly outperforms the AR LLM baseline trained under the same dataset. Diffusion-Proof achieves an absolute improvement of 1.61% on ProofNet-Test and 6.14% on MiniF2F-Test benchmarks compare to the baseline. Notably, Diffusion-Proof successfully resolves one IMO problem that more advanced thinking model DeepSeek-Prover-V2-7B could not solve, showcasing the unique advantage of dLLMs in formal theorem proving.