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

A research team has introduced Diffusion-Proof, a framework that applies diffusion large language models to formal theorem proving for the first time, according to a paper posted to arXiv on June 17. The approach uses two 7-billion-parameter models to generate and correct mathematical proofs, outperforming a comparable auto-regressive baseline on two standard benchmarks. The framework, detailed in a preprint, consists of two components: dLLM-Prover-7B, which writes entire proofs with long-range coherent tactic usage, and dLLM-Corrector-7B, a diffusion-based correction model that uses bi-directional information to perform local proof repair [1][2]. Diffusion LLMs generate text through iterative denoising of multi-token blocks, a departure from the next-token prediction method used by auto-regressive models [2]. The authors argue that auto-regressive models can suffer from error compounding over long sequences, a challenge that is particularly acute in formal mathematics where maintaining coherence across a proof is critical [2]. On the ProofNet-Test benchmark, Diffusion-Proof achieved an absolute improvement of 1.61% over the auto-regressive baseline trained on the same dataset. On the MiniF2F-Test benchmark, the improvement was 6.14% [1][2]. The paper also reports that Diffusion-Proof solved one International Mathematical Olympiad problem that the more advanced thinking model DeepSeek-Prover-V2-7B could not resolve [2]. The work addresses a gap in the literature. While auto-regressive LLMs have been widely applied to formal theorem proving, the use of diffusion LLMs in this domain has remained largely understudied [2]. The iterative denoising process at the core of dLLMs allows the model to refine entire blocks of text simultaneously, which the researchers leverage for both whole-proof generation and targeted correction [2]. Formal theorem proving requires models to produce sequences of logical tactics that are both locally valid and globally coherent. The compounding of errors in auto-regressive generation can derail a proof early, whereas the diffusion approach's ability to revisit and denoise multi-token blocks offers a structural advantage for maintaining consistency across long outputs [2]. The dLLM-Corrector-7B model specifically exploits the in-filling capabilities of diffusion LLMs, using context from both before and after a problematic segment to suggest repairs [2]. The paper appears as a preprint and has not yet been peer-reviewed. The code and data associated with the article are indexed on platforms including CatalyzeX and Hugging Face [1].