扩散模型也能做定理证明了，比自回归强，MiniF2F上高出6个百分点，还解了一道DeepSeek没解出的IMO题。
研究团队提出Diffusion-Proof，这是首个将扩散LLM（dLLM）应用于形式定理证明的框架。该框架包含两个7B模型：dLLM-Prover-7B负责整段证明生成，dLLM-Corrector-7B利用双向信息进行局部校正。相比同等数据集训练的自回归基线，Diffusion-Proof在ProofNet-Test上提升1.61%，在MiniF2F-Test上提升6.14%。此外，该框架成功解决了一个更先进的DeepSeek-Prover-V2-7B未能解答的IMO问题，展示了扩散模型在长程连贯性任务上的优势。
Diffusion-Proof: Recipe for Formal Theorem Proving Beyond Auto-Regressive Generation
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.