LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification

AI summary

Overview

Research area: Machine learning — specifically AI for mathematics, process supervision / reward modeling, and LLM verification of natural-language reasoning.

Technical level: Advanced. The core idea is easy to state, but the paper assumes familiarity with proof assistants (Lean 4 / Mathlib), process reward models, and reinforcement learning (GRPO).

Scope: The paper introduces LeanPRM, a pipeline that uses the Lean proof assistant to generate step-level correctness labels for natural-language mathematical proofs, plus a 200-proof held-out benchmark, and evaluates verifier models trained on that data against a PRM800K-trained baseline across five benchmarks and three model sizes.

What This Paper Is About

AI systems now produce long, difficult mathematical proofs, but a proof has no final answer to check — its correctness lies in whether each step follows from the previous ones. Training a learned verifier to check proofs step by step requires a correctness label on every step, and such labels are scarce: human annotation is expensive, outcome-based labeling does not apply, and formalizing proofs in Lean requires expert effort. LeanPRM's goal is to manufacture those step labels automatically, by having a model write each natural-language step alongside a paired Lean step that the proof assistant can mechanically check.

Key Contributions

1. LeanPRM, a Lean-grounded labeling framework. To the authors' knowledge, the first framework that uses Lean to produce step-level correctness labels for natural-language proofs at scale. Each step of a natural-language proof is paired with a formal Lean tactic; Lean compiles the proof, and the outcome of each tactic becomes the label of the corresponding natural-language step. A second model call separates mathematical errors from failures that are only formal-syntax problems.

2. A corpus of 10,634 labeled proofs. 6,370 correct and 4,264 incorrect proofs containing 152,005 labeled steps, produced with no human annotation. 98% of the corpus comes from NuminaMath-LEAN and Lean-Workbook. Every negative example carries a mathematical error class (six mathematical classes are retained; four formalization-side classes are removed).

3. LeanPRM-Bench. A held-out benchmark of 200 natural-language proofs (100 correct, 100 incorrect) with step labels, error classes and formal proofs, released for evaluating proof verifiers. No benchmark theorem appears in the training data.

4. A controlled evaluation. With the same model, recipe and number of updates (500), verifiers trained on Lean-grounded labels outperform verifiers trained on human PRM800K labels on four of five benchmarks, select better proofs at test time on IMO-level problems, and improve at every model size from 0.6B to 8B parameters on three of the five benchmarks.

Main Findings

• Large gain on the in-domain benchmark. A Qwen3-4B verifier trained on LeanPRM raises exact step-label accuracy on LeanPRM-Bench from 48.2 to 74.7, versus 60.3 when the same base model is trained with the same recipe on PRM800K.

• Wins on four of five benchmarks at equal training. LeanPRM-Verifier-4B beats PRM800K-Verifier-4B by 14.4 points on LeanPRM-Bench, 9.7 on Hard2Verify, 4.1 on PRMBench and 9.4 on IMO-GradingBench.

• One benchmark favors the human labels. PRM800K-Verifier-4B keeps an 8.1-point lead on ProcessBench (83.0 average F1 versus 74.9). The paper attributes this to ProcessBench's short solutions coming from the same distribution as PRM800K's training data, and to its annotation convention, which counts a missing justification as an error only when it affects the validity of the solution.

• Training on solving problems does not produce a verifier. NuminaMath-Solver-4B, trained with reinforcement learning on 19,200 NuminaMath problems with a final-answer reward, raises final-answer accuracy on its own validation problems from 30.0% to 47.5%, yet stays within a point of the untrained model on LeanPRM-Bench (48.3 versus 48.2) and falls below it on every external benchmark.

• The verifier is useful for test-time selection. On IMO-GradingBench (30 problems, about 33 human-graded proofs each), at N=16 LeanPRM-Verifier-4B picks a correct proof 35.9% of the time against 32.4% for random selection, and its advantage grows with N up to N=8. PRM800K-Verifier-4B reaches 33.2% because it accepts about 79% of all proofs although only 30% are graded correct, so its picks differ little from chance.

• Training helps at every model size. After 500 updates the gain on LeanPRM-Bench over the untrained model is 31 points at 0.6B, 27 at 4B and 29 at 8B. The 4B and 8B models reach nearly the same LeanPRM-Bench accuracy (74.7 and 75.0) and are within 0.8 points on PRMBench and IMO-GradingBench; the 8B model is 4.4 points ahead on ProcessBench, and the 4B model is ahead on Hard2Verify. The 0.6B model stays 21 points below the 4B model on LeanPRM-Bench.

• A longer run improves results further. LeanPRM-Verifier-4B †, a separate 4B run of 1,582 updates of which only the last 300 are on LeanPRM, reaches 78.7 on LeanPRM-Bench, 79.0 on Hard2Verify, 72.6 on ProcessBench, 48.3 on PRMBench and 71.8 on IMO-GradingBench. Its data differ as well as its length, so it is reported only for reference.

• Prompted commercial models are strong but not dominant. Four commercial models reach 71.7 to 80.3 mean exact step-label accuracy on LeanPRM-Bench over three runs (Claude Sonnet 5: 71.7, Claude Fable 5.1: 78.3, GPT-5.6 Sol: 75.3, Claude Opus 5: 80.3), and lead on Hard2Verify, ProcessBench and IMO-GradingBench. In their original reference runs all four mislabel the same 26 LeanPRM-Bench proofs; LeanPRM-Verifier-4B † labels 8 of those 26 exactly.

• The labels are audited, not assumed correct. In a blind audit of 100 stratified proofs, a judge that never saw the labels returned a usable answer for 99, disputed 1 of the 52 proofs labeled correct, and of the 47 labeled incorrect found an error in 27 and none in 20. A second audit of 30 flagged steps per class showed formalization-side steps were judged sound in 77% to 93% of cases (for example 28/30 for wrong rewrite direction and 26/30 for theorem misapplication), while mathematical steps were judged sound less than half the time (13/30 for unjustified assumption and 13/30 for invalid inequality bound). This motivated removing every attempt whose first failure is formalization-side.

• Data pipeline yield. Starting from about 17,800 distinct theorem statements, Stage 2 produced a labeled proof for 13,940; 13,007 remained after lexical filters and removal of duplicate and empty proofs; quality control left 10,634. Among the 4,264 incorrect proofs, every one fails first at a mathematical error, most often an unjustified assumption (21.3% of errors).

Methodology in Plain English

Stage 1 — write a proof and its formal twin. The authors collect about 17,800 theorem statements from public formal corpora (mostly NuminaMath-LEAN and Lean-Workbook, with smaller amounts from Pythagoras, Herald, ProofNet and FormalQualBench). For each statement, a model writes a proof in one shot, as numbered steps of ordinary mathematical prose, where every step is paired with the Lean tactic that carries it out. Crucially, the model never sees Lean's output while writing — otherwise it would repair its mistakes or give up, and the genuine errors the authors want to label would disappear. The model is always asked to prove the theorem and is never told to make a mistake.

Stage 2 — let Lean grade it. The formal proof is compiled with Lean 4 and Mathlib (both v4.25.0-rc2). Because each sentence was written with its own formal step, a compiler error points to exactly one step. Everything before the first failure is labeled correct; the failing step and everything after it are labeled incorrect. Since a formal step can fail for purely syntactic reasons while the mathematics is sound, a second model call reads the statement, the steps and the compiler output, then returns a verdict: correct, mathematical error (with one of ten error classes), or syntax error (with a single attempt to patch the Lean step, kept only if the patched proof then compiles). Proofs whose first failure is formalization-side are discarded, as are ill-posed statements and malformed outputs.

Keeping the prose honest. Lexical filters check that no natural-language step mentions Lean or specific tactics, and incorrect proofs whose failing step announces its own error are removed — the latter check removed 55.2% of incorrect proofs from an earlier joint-generation procedure and 2.3% from the blind procedure.

Training the verifier. The verifier sees only natural language: a theorem and its numbered steps. It writes reasoning, then labels each step correct or incorrect and gives a whole-proof verdict. Qwen3 models at 0.6B, 4B and 8B are trained in thinking mode with GRPO. The reward is 0.7 times step recall combined with 0.3 times verdict correctness; the step term is the product of recall on correct steps and recall on incorrect steps when the proof contains an error, which rules out the shortcuts of labeling everything correct or everything incorrect. Each update uses 64 proofs, a learning rate of 10⁻⁶, importance-ratio clipping to [0.8, 1.26] and a KL penalty of 10⁻³; the main comparison uses 500 updates, covering 32,000 proofs — 3.12 passes over the 10,264 LeanPRM training proofs and 0.45 over the 70,502 PRM800K training proofs.

Why This Matters

Impact on research. The paper shows that an exact mechanical checker can supervise informal reasoning without autoformalization: Lean is used once, offline, to build training data, and the resulting verifier reads natural language directly. That breaks the dependency on human step annotations (PRM800K needed about 800,000 step labels) and on final-answer-derived labels, which do not apply to proofs. The corpus can in principle grow with the supply of formal statements rather than with annotator time.

Real-world applications:

• Grading and giving step-level feedback on student or competition-style proofs that are too hard for non-experts to check.
• Serving as a reward model for training provers, since the paper's future work proposes exactly this.
• Reviewing AI-generated mathematical arguments in research and engineering settings where correctness must be established but formalization is impractical.
• Extending the same recipe to other open-ended tasks with no final answer but with parts an exact checker can verify — the authors name test suites for code and simulators for science.

Industry relevance. The result is directly relevant to teams building reasoning models and reward models: it offers a scalable data-generation recipe, an open benchmark, and a controlled comparison against the standard human-labeled alternative at three model sizes. The finding that RL on solving problems does not by itself produce a verifier is a practical caution for anyone assuming verification ability comes free with stronger problem solving.

Future Directions

1. Isolate the source of the gain. The authors compared Lean labels with PRM800K's human labels but did not train on the same proofs labeled by an LLM judge, so they cannot yet say how much of the improvement comes from the labels and how much from training on proof-style data.

2. Broaden the error distribution. Because negative examples are Claude's own mistakes, they may cover a narrower range of errors than a proof verifier should detect. Expanding the generators or deliberately inducing diverse failure modes is an open problem.

3. Tighten the label separation. The mathematical-versus-formalization distinction relies on a model's classification, checked with a single judge model on a sample, so some borderline steps may still carry the wrong label.

4. Grow beyond existing formal collections. Generating new theorem statements would let the corpus expand in both size and difficulty beyond current formal collections, and the methodology could transfer to other domains with exact checkers.

Target Audience

Researchers and engineers working on LLM reasoning, process reward models, and AI for mathematics; practitioners building verifiers or reward models who need scalable supervision without human annotation; and anyone evaluating AI-generated proofs who wants to understand where step-level labels can come from. Readers without a background in proof assistants or reinforcement learning can follow the pipeline and results but will need to consult the appendices for the training and evaluation details.

Authors’ abstract

AI systems now write long and difficult mathematical proofs, and checking their step-by-step validity is becoming a bottleneck. A learned verifier could check proofs cheaply, but training one requires a correctness label on every step, and such labels are hard to obtain for open-ended proofs. Existing methods take them from human annotators, which is costly, or derive them from final answers, which proofs do not have, and formalizing each proof in Lean requires expert effort. We introduce LeanPRM, a framework that uses the Lean proof assistant to create step-level labels for natural-language proofs. A model writes a natural-language proof together with a paired formal proof, without feedback from Lean. Lean then labels every step, and a second model discards failures caused only by the formal syntax, so that the negative labels mark errors in the mathematics. LeanPRM contains 10,634 proofs with 152K labeled steps and no human annotation. A Qwen3-4B verifier trained on LeanPRM raises exact step-label accuracy on a held-out set of 200 proofs (LeanPRM-Bench) from 48.2 to 74.7, as opposed to 60.3 when the same base model is trained on PRM800K. It also selects better proofs in best-of-N selection on IMO-level problems, and outperforms the PRM800K-trained verifier on three of four external verification benchmarks. Training on LeanPRM improves verifiers at every size from 0.6B to 8B parameters on LeanPRM-Bench, Hard2Verify and IMO-GradingBench. Given the labels need no human annotation, LeanPRM can grow with the supply of formal statements, offering a path to step-level feedback on AI-generated proofs that are hard for humans to check.