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

1 Introduction

• Proofs have no short final answer to check, while formalizing informal proofs in Lean requires expert-level effort and reliable step-level supervision is scarce.Human labels are costly, and final-answer-derived labels do not apply to proofs.Source: §1 · pp. 1–2
• LeanPRM pairs each natural-language proof step with a formal Lean step, uses Lean’s checks as labels, and trains a verifier that reads only natural language.The verifier’s training labels are created offline; it does not receive formal proofs as input.Source: §1 · pp. 2–3
• The pipeline repairs syntax-only failures once and retains mathematical errors, producing 10,634 proofs with 152,005 labeled steps and no human annotation.It also includes LeanPRM-Bench, a held-out set of 200 proofs.Source: Figure 1 · p. 2, §1 · p. 3
• LeanPRM-Verifier-4B gains 14.4 points of exact step-label accuracy on LeanPRM-Bench over the PRM800K-trained verifier and also improves on Hard2Verify and IMO-GradingBench.It beats that verifier on four of five benchmarks and selects correct proofs more often than random selection on IMO-level problems.Source: §1 · p. 3

2 LeanPRM: Lean-Grounded Process Supervision

• A model writes paired natural-language and Lean proofs; Lean checks the formal steps, and a second model reviews compilation failures and repairs syntax errors once.Steps through the first failure receive the tactic outcome; all subsequent steps are labeled incorrect.Source: §2 · p. 3
• The proof attempts come from about 17,800 public theorem statements, with each model-generated proof written in one pass without checker feedback.The statements span several areas of mathematics, including algebra, inequalities, number theory, and existence problems.Source: §2 · p. 3
• The verification stage classifies mathematical versus syntax failures, patches a syntax failure once, and discards proofs with ill-posed statements or mismatched prose and formal proofs.The labeling convention marks the first failing step and every later step incorrect.Source: §2 · pp. 3–4

2.1 LeanPRM Corpus

• LeanPRM contains 10,634 proofs—6,370 correct and 4,264 incorrect—with 152,005 labeled steps and no human annotation.The audit found formalization-side steps were judged sound in 77% to 93% of cases, so attempts with those first failures are removed.Source: §2.1 · pp. 4–5, Table 1 · p. 5
• The error taxonomy has ten classes: six describe mathematical faults and four describe formalization failures.Mathematical classes include unjustified assumptions, invalid bounds, wrong constructions, missing cases, faulty identities, and modular or divisibility errors.Source: §2.1 · p. 4

2.2 LeanPRM-Bench

• LeanPRM-Bench holds out 200 theorems, split evenly between correct and incorrect proofs, with no benchmark theorem in training.Four prompted commercial models achieved 71.7 to 80.3 mean exact step-label accuracy across three runs.Source: §2.2 · p. 5

3 Experiments

• The main comparison trains Qwen3 verifiers with GRPO for 500 updates; the PRM800K baseline uses the same recipe, while the solver baseline instead receives final-answer rewards.Evaluation uses LeanPRM-Bench and four external benchmarks, with one metric per benchmark and means over three runs.Source: §3 · pp. 5–6

3.1 Results

• At equal training budgets, LeanPRM-Verifier-4B leads PRM800K-Verifier-4B on four of five benchmarks, by 14.4 points on LeanPRM-Bench, 9.7 on Hard2Verify, 4.1 on PRMBench, and 9.4 on IMO-GradingBench.PRM800K-Verifier-4B leads by 8.1 points on ProcessBench.Source: §3.1 · pp. 6–7, Table 2 · p. 7, Figure 3 · p. 7
• LeanPRM-Verifier-4B selects a correct IMO-GradingBench proof 35.9% of the time at N = 16, versus 32.4% for random selection; PRM800K-Verifier-4B reaches 33.2%.LeanPRM’s advantage grows with N up to 8, while PRM800K-Verifier-4B stays near chance.Source: §3.1 · p. 8, Figure 4 · p. 8
• Training improves 0.6B, 4B, and 8B verifiers on LeanPRM-Bench, Hard2Verify, and IMO-GradingBench.LeanPRM-Bench gains over untrained models are 31, 27, and 29 points, respectively; the trained 0.6B model still trails the 4B model by 21 points there.Source: §3.1 · p. 8, Figure 5 · p. 9
• The trained 4B and 8B models reach 74.7 and 75.0 LeanPRM-Bench accuracy, respectively, and remain within 0.8 points on PRMBench and IMO-GradingBench.The 8B model has more unparsable Hard2Verify answers than the 4B model, contributing to their benchmark gap.Source: §3.1 · p. 9

Process supervision

• Process-supervision labels have come from human annotation, sampled-continuation outcomes, rollout search, and outcome-level rewards.Prior work also studies whether process- or outcome-based feedback supports effective test-time search.Source: §4 · pp. 9–10

Formal mathematics

• Among the label sources compared, only LeanPRM avoids human annotation, covers open-ended natural-language proofs, assigns mathematical error types to failures, and trains a verifier on proof text.These are the four criteria tabulated in the paper’s comparison.Source: Table 3 · p. 10

Formal verification for reasoning

• FoVer trains on formal traces labeled with Z3 and Isabelle, whereas LeanPRM trains directly on natural-language competition proofs paired with Lean tactics.The paper positions this as a distinction from prior formal-reasoning supervision.Source: §4 · p. 10

Formal mathematics

• LeanPRM uses formal checking to create step labels at scale for a verifier that reads only natural language, rather than using the formal proof as its input or output.Other cited work uses formal verification to evaluate reasoning, check steps at inference, train natural-language reasoning, or select fine-tuning data.Source: §4 · p. 10

5 Conclusion

• LeanPRM uses Lean to label every step of natural-language proofs and trains verifiers on a corpus of 10,634 proofs with a held-out benchmark.The framework can train verifiers for informal reasoning without autoformalization.Source: §5 · p. 11
• LeanPRM verifiers outperform PRM800K-trained verifiers on four of five benchmarks and pick better proofs at test time.The conclusion says Lean is needed only once, offline, to build the data; the resulting verifier checks natural language directly.Source: §5 · p. 11
• The separation of formal-encoding failures from mathematical errors relies on model classification checked by one judge model on a sample, so some borderline steps may be mislabeled.The authors also note that LeanPRM-Bench shares the training pipeline and Claude generators, and that Claude's mistakes may cover a narrower range of errors than a verifier should detect.Source: §5 · p. 11
• The authors propose extending the approach to code test suites or science simulators and growing the math corpus with newly generated theorem statements.They also suggest LeanPRM-trained verifiers could serve as reward models or provide step-level feedback on difficult proofs.Source: §5 · p. 11

Appendix

• The appendices provide error-class definitions, data and split details, analyses of benchmark errors, training and evaluation details, further examples, prompts, and hyperparameters.Appendix F gives model-scale numbers behind Figure 5, and Appendix G discusses the ProcessBench result.Source: Appendix · p. 16

A Error classes

• Six mathematical classes cover false algebraic manipulation, unjustified or reversed inequality bounds, bad witnesses or constructions, modular or divisibility errors, omitted cases or side conditions, and unsupported claims.The labels are algebraic identity error, invalid inequality bound, bad witness or construction, modular or divisibility error, missing case or side condition, and unjustified assumption.Source: A Error classes · p. 16
• Four formalization-side classes cover theorem misapplication, wrong rewrite direction, automation misuse, and failures not captured by the other classes.The class names are theorem misapplication, wrong rewrite direction, automation misuse, and other.Source: A Error classes · p. 16
• Attempts whose failure was recorded without a class are reported as unclassified.Source: A Error classes · p. 16

B Data sources, filtering and splits

• NuminaMath-LEAN, Lean-Workbook, Pythagoras, Herald, ProofNet, and FormalQualBench supply theorem statements; NuminaMath supplies most incorrect proofs and Lean-Workbook most correct ones.The source subset is difficulty-filtered; Table 4 reports composition by source and split.Source: B Data sources, filtering and splits · p. 17, Table 4 · p. 17
• The training split contains 10,264 theorems and is oversampled within each source to parity, yielding 17,670 rows; validation has 170 theorems and LeanPRM-Bench has 200.Training includes 6,170 correct and 4,094 incorrect theorems; validation has 100 correct and 70 incorrect, while LeanPRM-Bench has 100 of each verdict.Source: B Data sources, filtering and splits · p. 17
• Theorem-group splitting keeps alpha-renamed restatements from crossing boundaries, and theorem identity is defined modulo the declaration name.LeanPRM-Bench was fixed before the class-based filter; 30 incorrect proofs with a formalization-side first error were replaced by mathematical-error proofs, and systems were re-evaluated.Source: B Data sources, filtering and splits · p. 17
• Generation rejects specified Lean-related whole words in natural-language steps, while split construction removes incorrect proofs whose first failing step announces its error.The second check removed 55.2% of incorrect proofs from the earlier joint procedure and 2.3% from the blind procedure.Source: B Data sources, filtering and splits · p. 17
• The Lean lines were not filtered for sorry, admit, or native_decide, which appear in 605 proofs; transitive dependencies were not checked, and only Stage 2 repairs are barred from using those placeholders.One positive training proof with explicit sorry was retained; no explicit placeholders appeared in positive validation or benchmark proofs.Source: B Data sources, filtering and splits · pp. 17–18

C Proofs the frontier models misjudge

• 29.5% of the 26 proofs mislabeled by all four commercial systems were labeled exactly by LeanPRM-Verifier-4B† across three decoding seeds, versus 7.7% for the untrained model and 11.5% for PRM800K-Verifier-4B.In the original reference run, the trained verifier labeled 8 of the 26 exactly; the reverse case covers 12 of 128 proofs on which all four commercial systems were right.Source: C Proofs the frontier models misjudge · p. 18
• In Figure 6, step 5 asserts an unsupported strong-induction count, which the checker rejects as an unjustified assumption; the commercial systems and PRM800K-Verifier-4B accept every step.Opus 5 and GPT-5.6 Sol first object at step 6, while LeanPRM-Verifier-4B† labels the proof exactly.Source: Figure 6 · p. 19
• Figure 7 shows a proof that stops after establishing a summed inequality and defining S, without producing the two distinct zeros; the final step is therefore incorrect under the stated convention.Every other system accepts all nineteen steps, while LeanPRM-Verifier-4B† flags the last.Source: Figure 7 · p. 20
• In Figure 8, a wrong coefficient in a Lagrange-type identity causes a ring-normalization failure; the commercial systems and PRM800K-Verifier-4B flag the step, while LeanPRM-Verifier-4B† accepts the proof.Source: Figure 8 · p. 21

• The task reward combines step-label reward and verdict accuracy as 0.7 Rstep + 0.3 Rverdict, with malformed or inconsistent outputs scoring zero.For incorrect proofs containing both label classes, the step reward RecC RecI penalizes predicting every step correct or every step incorrect.Source: D Training details · p. 22
• LeanPRM-Verifier-4B† trains for 1,582 updates across three data stages, while other listed verifiers train for 500 updates from their base checkpoints.Its stages use 3,449 earlier proofs, the unfiltered Section 2.1 pool, and LeanPRM; the 8B model uses offloading and two-GPU tensor parallelism.Source: D Training details · p. 22
• Models use group-relative policy optimization with eight responses per prompt, temperature 1, batch size 64, learning rate 10−6, and KL coefficient 10−3.The response limit is 6,656 tokens, and training runs on four H100 80GB GPUs with validation and checkpoints every 50 updates.Source: D Training details · p. 22

• The held-out split is scored by exact step-label accuracy, the fraction of proofs with every label correct, and verdict accuracy.Hard2Verify uses response-level balanced accuracy, ProcessBench mean F1 across four subsets, and PRMBench first-error accuracy.Source: E Evaluation details · p. 22
• IMO-GradingBench grades are binarized as fully correct versus all other grades, and paragraph-boundary splitting leaves 987 candidates after 13 exceed the context budget.Above thirty steps, candidates are merged evenly; every model receives the same prompt layout and label parser.Source: E Evaluation details · p. 22
• Results report mean and population standard deviation over three runs for open-weight models and independent hosted runs without controlled seeds for commercial models.Hosted responses are Markdown-normalized before parse failures count as incorrect; the open-weight runs use seeds 42, 43, and 44.Source: E Evaluation details · p. 22
• Claude models use extended thinking through the Anthropic API, while GPT-5.6 Sol is prompted through Codex rather than the bare API.Codex prepends agent instructions and withholds reasoning; all 33,009 evaluations across its three runs completed without tool use.Source: E Evaluation details · p. 22

• The 4B and 8B verifiers are close on LeanPRM-Bench, PRMBench, and IMO-GradingBench, while the 0.6B model is far behind.Table 5 compares trained Qwen3 verifiers at three sizes after 500 updates with their untrained counterparts; values are means ± population standard deviations over three decoding seeds.Source: F Model scale results · p. 22, Table 5 · p. 23

G Labeling conventions and ProcessBench

• Flags placed before ProcessBench’s reference step rise from 158 to 236 to 379 across three checkpoints, a trend consistent with—but not isolating—the proposed labeling-convention explanation.The authors say they have not tested that explanation directly; only the last two checkpoints share training data, and auditing the early flags would help settle it.Source: G Labeling conventions and ProcessBench · p. 23

H Further LeanPRM examples

• Figure 9 shows a correct four-claim completion-of-the-square proof whose steps all elaborate; this example format accounts for 6,370 of 10,634 LeanPRM theorems.The theorem is the inequality 2t ≤ 1 + t2 for real t.Source: Figure 9 · p. 23
• Figure 10’s choice n = 1 cannot satisfy an arbitrary n > N bound, so Stage 2 marks the attempt’s bound error and steps 4 and 5 incorrect.Lean elaboration fails at step 4 despite the text conceding the bound problem.Source: Figure 10 · p. 24
• Figure 11’s divisibility argument is mathematically sound, but an unsupported Mathlib lemma form causes elaboration failure; this class was sound in 26 of 30 audited cases.Stage 2 labels the example theorem misapplication, and formalization-side classes are excluded from the corpus.Source: Figure 11 · p. 25

I Prompts

• Each natural-language description must match its Lean step mathematically, and the ordered descriptions must form a complete standalone proof rather than tactic commentary.Prompts require explicit intermediate mathematical steps instead of opaque one-shot tactics for the main argument.Source: I Prompts · p. 26
• Stage 1 is a blind proof attempt: its natural-language plan is frozen, and Lean feedback is reserved for classification and private syntax repair.The generator is instructed to pair each Lean tactic step with a mathematical natural-language explanation that does not mention Lean syntax or code.Source: I Prompts · pp. 26–27
• Stage 2 separates mathematical reasoning errors from mechanically repairable Lean syntax failures, while incomplete or invalid mathematics remains a reasoning error.Repairs may change only surface syntax or elaboration and cannot alter mathematical content; ill-posed statements or mismatches between the natural-language and Lean mathematics are discarded.Source: I Prompts · p. 27

J Hyperparameters

• The training configuration is shared across trained models, with training data varying and 8B runs additionally using offloading and tensor parallelism.Table 6 lists the common configuration.Source: J Hyperparameters · p. 29, Table 6 · p. 29