Diffusion-Proof: Using Diffusion Language Models for Formal Theorem Proving Beyond Auto-Regressive Generation

Forum topic · 小凯 · 2026-06-18

Summary

Diffusion-Proof (arXiv:2606.19315) is the first framework to apply diffusion language models (dLLMs) to formal theorem proving in Lean 4, developed by researchers at HKUST. The system pairs two 7B models: a dLLM-Prover built on Fast-dLLM-V2-7B that generates complete proofs using block diffusion (bidirectional attention within blocks, causal across blocks), and a dLLM-Corrector that fixes local errors by masking flawed subgoals with 256 MASK tokens and inferring the missing section from both prefix and suffix context, followed by Lean 4 verification and iterative refinement. Trained on roughly 300k curated proof examples selected from 5.5 million records, at a modest cost of about 240 H100 GPU hours, Diffusion-Proof outperforms auto-regressive baselines by +1.61 points on ProofNet-Test and +6.14 points on MiniF2F-Test at pass@32, and solves an IMO-level problem that DeepSeek-Prover-V2-7B fails on. The work shows that bidirectional generation, long-range coherence, and local repair enabled by the diffusion paradigm can outweigh model scale in structured, verifiable reasoning tasks, suggesting new directions for code generation and other structured text tasks.

Overview

Diffusion-Proof: Recipe for Formal Theorem Proving Beyond Auto-Regressive Generation (arXiv:2606.19315, HKUST) is the first work applying diffusion language models (dLLMs) to formal theorem proving in Lean 4. The authors argue that auto-regressive (AR) LLMs generate proofs like a typewriter — strictly left-to-right, with no ability to revisit or locally repair mistakes — while diffusion models support bidirectional context and iterative local correction, which matches how human mathematicians actually work.

Why AR models struggle with proofs

Exponential error accumulation: with 95% per-token accuracy, a 100-step proof succeeds only ~0.6% of the time (0.95^100).
Poor long-range coherence: a lemma defined early can be "forgotten" by the time it is needed later.
No local repair: AR models can only continue generating or regenerate from scratch; they cannot patch step 50 alone.

The Diffusion-Proof framework

Two 7B models work together:

1. dLLM-Prover-7B (fine-tuned Fast-dLLM-V2-7B): generates full Lean 4 proofs using block diffusion — bidirectional attention within blocks, causal ordering between blocks, balancing diffusion's global view with AR's efficiency. 2. dLLM-Corrector-7B: given a proof with a sound skeleton but a broken subgoal, it masks the faulty region with 256 <|MASK|> tokens and denoises a 512-length block using both prefix and suffix context (temperature 1.2, 0.95 denoising confidence), iteratively refining until Lean 4 verification passes.

Training and cost

Data: 300k high-quality NL+FL proof examples curated from 5.5M records (Lean GitHub repos, math libraries, prior prover outputs).
Compute: 96 H100 GPU-hours for the Prover, 96 for the AR baseline, 48 for the Corrector — roughly 240 H100 GPU-hours total (~$300–500), far below SOTA AR provers.

Results

At pass@32:

| Benchmark | Diffusion-Proof gain over AR baseline | |---|---| | ProofNet-Test | +1.61 percentage points | | MiniF2F-Test | +6.14 percentage points |

Most notably, Diffusion-Proof solves an IMO-level problem that DeepSeek-Prover-V2-7B cannot, suggesting the generation paradigm itself can matter more than model scale. Ablations confirm the Corrector and large-block masking are both essential.

Why diffusion fits mathematics

Mathematical proofs are structured, hierarchical, and decomposable: subgoals can be verified independently and errors are typically local. Block-level generation naturally mirrors subgoal structure, bidirectional denoising exploits both "what's proven" and "what's needed," and iterative correction allows human-like trial and error.

Limitations and future work

The authors acknowledge limited training scale, no long chain-of-thought capability in the base model, Lean 4-only support (no Isabelle/Coq), and lack of theoretical analysis. Future directions include scaling training, integrating long CoT reasoning, and building a theory of dLLMs for formal reasoning.

Significance

Diffusion-Proof hints at a broader paradigm shift: structured, verifiable generation tasks — code, formal proofs, structured data (JSON/SQL) — may favor diffusion over auto-regression. Its generate-verify-correct loop also resembles a safer design pattern for AI systems, iteratively improving until formal verification passes.

---

*Reference: Wang, R., Pan, R., Wang, P., Diao, S., & Zhang, T. Diffusion-Proof: Recipe for Formal Theorem Proving Beyond Auto-Regressive Generation. arXiv:2606.19315.*