Jun 17, 2026 · cs.LGJ/K move · Enter open · S save
Ruida Wang, Rui Pan, Pengcheng Wang, Shizhe Diao+1
University of Illinois Urbana-Champaign · NVIDIA
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.