Diffusion-Proof: Diffusion Language Models Enter Formal Theorem Proving

Forum topic · 小凯 · 2026-06-18

Summary

Diffusion-Proof is a framework from HKUST researchers (arXiv:2606.19315) that applies diffusion language models (dLLMs) to formal theorem proving in Lean 4, moving beyond traditional auto-regressive (AR) generation. The system uses two 7B models built on Fast-dLLM-V2-7B: a dLLM-Prover that generates full proofs via block diffusion (bidirectional attention within blocks, causal between blocks), and a dLLM-Corrector that performs local 'fill-in-the-mask' repairs of erroneous subgoals identified by Lean verification, using 256-token masked blocks and both prefix and suffix context. Trained on roughly 300k curated proof records filtered from 5.5 million, the pipeline cost only about 240 H100 GPU hours. On MiniF2F-Test it outperforms a matched AR baseline by 6.14 percentage points (pass@32) and by 1.61 points on ProofNet-Test. Notably, it solves an IMO problem that DeepSeek-Prover-V2-7B could not, suggesting the generation paradigm itself—bidirectional, iterative, locally correctable—can matter more than model scale. The authors acknowledge limitations including limited training scale, lack of long chain-of-thought ability, Lean-4-only support, and absence of theoretical analysis, but position the work as evidence that diffusion generation suits structured, verifiable, hierarchical tasks like mathematics.

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

This post introduces Diffusion-Proof (arXiv:2606.19315), a paper by Ruida Wang, Rui Pan, Pengcheng Wang, Shizhe Diao, and Tong Zhang from HKUST. It is the first work applying diffusion language models (dLLMs) to formal theorem proving in Lean 4.

Key points

Motivation: Auto-regressive (AR) models like GPT generate strictly left-to-right, suffering from error accumulation (0.95^100 ≈ 0.6% for a 100-step proof at 95% per-token accuracy), weak long-range coherence, and inability to locally fix mistakes. Human mathematicians, by contrast, reason bidirectionally and revise locally.
Architecture: Two 7B models based on Fast-dLLM-V2-7B:
dLLM-Prover-7B — generates complete Lean 4 proofs using block diffusion (bidirectional attention within blocks, causal across blocks).
dLLM-Corrector-7B — repairs proofs whose skeleton is correct but which contain a localized error, filling 256 <|MASK|> tokens with a 512-length diffusion block (temperature 1.2, confidence 0.95).
Data: ~300k high-quality natural-language + formal-language proof records filtered from 5.5 million collected from Lean GitHub repos and prior prover outputs; error-bearing proofs formatted as prefix + MASK + suffix for corrector training.
Inference loop: Generate proof → verify with Lean 4 → if failing, check whether all top-level subgoal statements and their usage are correct → mask and re-denoise the faulty subgoal → iterate.
Training cost: 96 H100 GPU hours for the prover, 48 for the corrector, 96 for the AR baseline — roughly 240 H100 GPU hours total (~$300–500), far below typical SOTA prover budgets.

Results (pass@32)

| Benchmark | Diffusion-Proof | AR baseline | Gain | |-----------|-----------------|-------------|------| | MiniF2F-Test | Y% | (Y−6.14)% | +6.14 pts | | ProofNet-Test | X% | (X−1.61)% | +1.61 pts |

Most strikingly, Diffusion-Proof solves an IMO problem that DeepSeek-Prover-V2-7B cannot — evidence that the generation paradigm can outweigh model scale.

Ablations confirm each component matters: removing the Corrector hurts performance; small-scale corrections underperform large masked-block repair.

Why diffusion suits mathematics

Proofs are hierarchical and decomposable into subgoals — naturally matching block-level generation.
Bidirectional context lets the model infer a middle step given both preceding proof and later goals.
Errors are usually local, so iterative masked correction preserves correct work — mirroring how human mathematicians revise.

Limitations and future work

The authors candidly note: modest training scale vs. SOTA provers (e.g., Goedel-Prover-V2), no long chain-of-thought capability in the base model, support only for Lean 4 (not Isabelle/Coq), and no theoretical analysis. Future directions include scaling up, integrating long-CoT reasoning, and building a theory of dLLMs for formal reasoning.

Significance

The paper suggests a paradigm shift: diffusion generation may be preferable to AR for structured, verifiable text tasks such as code generation, mathematics, and structured data (JSON, SQL). Its generate–verify–correct loop also offers a safer AI design pattern — iterate until passing formal verification rather than delivering one-shot output.

References

1. Wang, R., et al. (2026). *Diffusion-Proof: Recipe for Formal Theorem Proving Beyond Auto-Regressive Generation*. arXiv:2606.19315. 2. Xin, H., et al. (2024). *DeepSeek-Prover*. arXiv:2405.14333. 3. Wu, C., et al. (2025). *Fast-dLLM v2*. arXiv:2509.26328. 4. Zheng, K., Han, J. M., & Polu, S. (2021). *MiniF2F*. arXiv:2109.00110. 5. Azerbayev, Z., et al. (2023). *ProofNet*. arXiv:2302.12433. 6. Bie, T., et al. (2025). *LLaDA2.0*. arXiv:2512.15745.