扩散证明：超越自回归生成的形式定理证明方法

近年来，增强大语言模型（LLM）的形式数学推理能力已成为数学和计算机科学界的重点关注点。虽然在使用最先进的自回归 (AR) LLM 进行形式定理证明方面取得了重大进展，但这些模型仍存在固有的局限性。由于长程一致性和长序列错误复合的挑战，他们的下一个词元预测生成方法可能会产生次优的性能。扩散 LLM (dLLM) 的最新进展通过多词元块的迭代去噪生成文本，提供了一种有前途的替代方案。然而，维持远程一致性至关重要的 dLLM 在形式数学中的应用仍然没有得到充分研究。为了应对上述挑战，据我们所知，我们提出**扩散证明**，这是第一个训练和应用 dLLM 进行形式定理证明的框架。我们的框架包含两个模型的训练和推理方法。第一个是*dLLM-Prover-7B*，它通过远程连贯策略使用来执行整体证明写作。第二个是*dLLM-Corrector-7B*，这是一种新颖的基于大块扩散的校正模型。它利用 dLLM 的填充功能，使用双向信息执行本地证明校正。大量实验表明，**Diffusion-Proof** 相对显着优于在相同数据集下训练的 AR LLM 基线。与基线相比，**Diffusion-Proof** 在 ProofNet-Test 基准上实现了 **1.61%** 的绝对改进，在 MiniF2F-Test 基准上实现了 **6.14%** 的绝对改进。值得注意的是，**Diffusion-Proof**成功解决了更先进的思维模型 DeepSeek-Prover-V2-7B 无法解决的一个 IMO 问题，展示了 dLLM 在形式定理证明方面的独特优势。