Diffusion LLMs May Have Found Their Best First Job: Fixing Formal Proofs

Diffusion language models have spent the last year looking for a job description better than “what if chat completion, but stranger?” Diffusion-Proof gives them one that actually fits: formal proof repair. Not general conversation. Not replacing autoregressive models across the board. A narrow, verifier-guided domain where bidirectional infilling is not a gimmick but a structural advantage.

The paper trains two 7B diffusion language models for Lean4 theorem proving. dLLM-Prover-7B writes whole proofs. dLLM-Corrector-7B performs local proof correction when verification fails. The authors argue that autoregressive generation is awkward for formal proofs because left-to-right decoding compounds early errors and cannot naturally patch a broken subgoal using both prefix and suffix context. Anyone who has fixed a proof, a test failure, or a generated function knows the shape of that problem: the right edit is often in the middle, and the surrounding context is the point.

The base lineage starts from Fast-dLLM-V2-7B, with a fair-comparison setup tied to Qwen-2.5-Instruct-7B. The data pipeline is substantial: the authors collect 5,595,798 theorem-proving records, clean and select 300k supervised fine-tuning records for prover training, and construct 128k corrector-training records from proofs with subgoal decomposition. The corrector expands the diffusion block size from 32 to 512, which is the practical move that lets it fill local proof gaps using broader bidirectional context.

The corrector is the part to watch

The evaluation uses MiniF2F-Test with 244 Lean4 math problems and ProofNet-Test with 186 college-textbook theorems. The primary metric is pass@32, using 32 corrections for each valid theorem. Diffusion-Proof reports absolute improvements over an autoregressive baseline trained on the same data: +1.61% on ProofNet-Test and +6.14% on MiniF2F-Test. The authors also claim the system solves one IMO problem that DeepSeek-Prover-V2-7B could not solve.

Those numbers should be read with a steady hand. This is not a new theorem-proving regime by itself. A 1.61-point gain on ProofNet and a 6.14-point gain on MiniF2F are interesting, not world-ending. But because the comparison is against a baseline trained on the same data, the result is more informative than the usual “we added more scale and the chart went up” story. The paper is making an architectural claim: diffusion-style bidirectional denoising can be useful for repair.

The corrector is more compelling than the whole-proof generator. Whole-proof writing still has the familiar problem of producing a long artifact whose correctness depends on many local choices. The corrector has a cleaner contract: Lean says where the proof broke, the system identifies a local gap, and the diffusion model fills that gap using context from both sides. That is exactly where an autoregressive model is least naturally shaped and a diffusion/infill model has a plausible edge.

Verifier-guided repair is bigger than Lean

Formal proof is a favorable environment for this idea because Lean provides a hard verifier. The model does not get to vibe its way through correctness. The proof compiles or it does not. That makes proof repair an unusually honest benchmark for local correction under constraints.

The broader software lesson is that many engineering tasks are repair tasks, not pure generation tasks. Fix a failing unit test while preserving surrounding code. Patch a SQL query without changing verified joins. Repair a config block while respecting constraints above and below it. Modify a generated API client without breaking call sites. These are not naturally left-to-right activities. Developers move around the file, use error messages, preserve known-good structure, and edit the minimum broken region. If diffusion LLMs become useful anywhere in software workflows, verifier-guided local repair is a credible first beachhead.

That does not mean teams should rush to replace coding agents with diffusion decoders. General software is messier than Lean. Tests can be incomplete, flaky, slow, or absent. Repositories contain implicit conventions, build-system traps, stale documentation, and side effects that do not reduce to a neat proof state. Lean gives Diffusion-Proof a clean oracle. The next question is whether the same correction pattern survives noisy CI, partial tests, and large repositories.

For practitioners, the useful action is to think about model roles rather than model religions. Autoregressive models may remain the best general planners and conversational interfaces. Diffusion models may become valuable as targeted repair engines, especially where you can provide a failing artifact, a verifier signal, and a bounded edit region. The right product shape may not be “diffusion assistant.” It may be an agent loop that calls a diffusion corrector when the verifier identifies a local failure.

The release caveat matters

The paper says training code, models, and datasets are planned for release, but at publication time the arXiv paper is the primary artifact. That keeps this in the promising-research bucket. Formal-methods claims are unusually verifiable once artifacts land, and the Lean community is good at finding out whether a theorem-proving system actually works. Until then, the sober read is: plausible mechanism, useful early evidence, wait for reproducibility.

There is also a benchmark-design point here. Diffusion-Proof’s value is not just its score. It gives diffusion LLMs a falsifiable use case. For too long, text-diffusion papers have been forced into comparisons where autoregressive models are already extremely optimized: open-ended chat, generic reasoning, and next-token-style benchmarks. Proof repair changes the shape of the task. It asks for bidirectional local reconstruction under a verifier, which is closer to what diffusion was built to do.

My take: diffusion LLMs do not need to beat autoregressive models at being chatbots to matter. They need a workflow where their generation geometry buys something real. Lean proof correction may be that first honest job. If the code release holds up, the interesting future is not “diffusion replaces the assistant.” It is “the assistant learns when to call the corrector.”

Sources: arXiv, DeepSeek-Prover-V2, MiniF2F, Lean theorem prover