cs.LGOct 13, 2026

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

Authors: Rodney Lafuente-Mercado, Salman Rahman, Jingyan Shen, James Shiffer, Saadia Gabriel, Pavel Izmailov

Organizations: University of Texas at Austin · University of California, Los Angeles · New York University

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

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.

Figures & tables

Figure 1: Overview of LeanPRM, with one example from the corpus running through it. Top row: Stage 1 writes a proof attempt from the theorem statement alone, each natural-language step paired with its formal step, and Lean checks the steps in order. Bottom row: Stage 2 decides whether the first failure lies in the mathematics or only in the formal syntax (syntax failures are patched and rechecked once), and the verifier is trained on the natural-language steps and their labels only. Here step 5 asserts without justification that conjugation by yy fixes xx , so steps 1 to 4 are labeled correct and steps 5 and 6 incorrect.
Figure 2: Composition of LeanPRM. Left: sources of the 10,634 theorems. Right: error class of the first failing step in each of the 4,264 incorrect proofs. Bars show percentages of incorrect proofs. Every incorrect proof fails first at a mathematical error, most often an unjustified assumption.
First-error classJudged soundShare of errors
Formalization-side
Wrong rewrite direction28/3028/302.7%2.7\%
Theorem misapplication26/3026/309.2%9.2\%
Other26/3026/309.5%9.5\%
Automation misuse23/3023/3013.4%13.4\%
Mathematical
Table 1: Blind audit of flagged steps, 30 per class (all formalization-side classes and the two largest mathematical ones). Judged sound : correct and justified. Share of errors : fraction of incorrect proofs in the unfiltered pool. Formalization-side steps are mostly sound. Mathematical steps are mostly not sound.
 LeanPRM-BenchHard2VerifyProcessBenchPRMBenchIMO-GB
 exactresponse BAavg. F1first err.BA
Qwen3-4B (initial policy)48.2 ±\pm 1.337.1 ±\pm 4.574.3 ±\pm 0.542.5 ±\pm 0.553.8 ±\pm 0.1
PRM800K-Verifier-4B60.3 ±\pm 1.663.1 ±\pm 0.683.0 ±\pm 0.343.3 ±\pm 0.357.0 ±\pm 0.4
NuminaMath-Solver-4B48.3 ±\pm 1.033.6 ±\pm 3.471.2 ±\pm 0.941.5 ±\pm 0.252.4 ±\pm 0.4
LeanPRM-Verifier-4B (ours)74.7 ±\pm 1.872.8 ±\pm 0.974.9 ±\pm 0.447.4 ±\pm 0.266.4 ±\pm 1.1
LeanPRM-Verifier-4B †78.7 ±\pm 1.379.0 ±\pm 0.772.6 ±\pm 0.348.3 ±\pm 0.271.8 ±\pm 1.0
Table 2: Verification accuracy. Open-weight models use temperature 1. Commercial-model settings are given in Appendix E . LeanPRM-Bench is scored by exact step-label accuracy (Section 2.2 ), and the other columns use the metrics of Section 3 . The top block compares 4B models trained for 500 updates with the same recipe, with the untrained model for reference, and bold marks the best value in that block. The bottom block holds reference rows: † a separate 4B run of 1,582 updates, only the last 300 of them on LeanPRM (Appendix D ), and commercial models prompted rather than trained for the task. At equal training, LeanPRM-Verifier-4B is best on four of the five benchmarks. Entries report mean ±\pm population standard deviation over three evaluation runs (Appendix E ).
Figure 3: The top block of Table 2 per benchmark: 4B models trained for 500 updates with the same recipe, and the untrained model. Bars are means over three decoding seeds with one standard deviation as error bars. LeanPRM-Verifier-4B is best on four of the five benchmarks and PRM800K-Verifier-4B on ProcessBench.
Figure 4: Training curves and test-time selection. Left: exact step-label accuracy on the LeanPRM validation split during training, for the verifiers trained from Qwen3 base models of three sizes; the 4B point at update 300 was measured separately with the same greedy protocol. Middle: the two trained baselines on their own validation splits, PRM800K-Verifier-4B by exact accuracy and NuminaMath-Solver-4B by final-answer accuracy; both change little over the second half of training. Right: best-of- NN selection on IMO-GradingBench, the share of selected proofs graded correct, averaged over the 30 problems and three decoding seeds (shaded band: one standard deviation); the dotted line is random selection. LeanPRM-Verifier-4B picks better proofs as NN grows, while PRM800K-Verifier-4B stays near chance.
Figure 5: Accuracy before and after training on LeanPRM, by model size. Each panel is one benchmark; open circles are the untrained Qwen3 models and filled circles the trained verifiers after 500 updates. Training improves every model on LeanPRM-Bench, Hard2Verify and IMO-GradingBench; the untrained 0.6B model scores near zero on three benchmarks because it rarely produces well-formed labels. Points and error bars show the mean and population standard deviation over three decoding seeds.
MethodStep labels fromNo human step labelsOpen-ended proofsError classesTrained verifier
PRM800K ( Lightman et al., 2023 )Human annotators✗✗✗✓
Math-Shepherd ( Wang et al., 2023 )Rollouts✓✗✗✓
OmegaPRM ( Luo et al., 2024 )Rollouts (tree search)✓✗✗✓
FoVer ( Kamoi et al., 2025 )Z3, Isabelle✓✗✗✓
Safe ( Liu et al., 2025 )Lean 4✓✗✗✗
TP-as-a-Judge ( Leang et al., 2025 )Lean 4 (per solution)✓✗✗✗
Table 3: Sources of step-level labels in prior work and in LeanPRM. For each method we give the origin of its step labels and whether they avoid human annotation, cover open-ended natural-language proofs, give each failing step a mathematical error type, and train a verifier that reads the proof text. Only LeanPRM does all four.
Appendix figures & tables9 assets

Supplementary material from the paper’s appendix.

Appendix

 CorrectIncorrectTotal
NuminaMath1,3343,9785,312
Lean-Workbook4,7872845,071
Pythagoras2301231
Herald13114
ProofNet606
Training6,1704,09410,264
Appendix
Table 4: Size of LeanPRM by source (top) and by split (bottom); each theorem contributes one proof. NuminaMath supplies most of the incorrect proofs and Lean-Workbook most of the correct ones.
Figure 6: A proof the trained verifier labels exactly and no commercial system does. Step 5 asserts, by an unelaborated strong induction, that any smooth set of nn numbers yields at least (n−512)/2(n-512)/2 disjoint pairs with equal parity vectors; the argument as written does not justify the count, the checker fails at this step, and the class is unjustified assumption. Sonnet 5, Fable 5.1 and PRM800K-Verifier-4B accept every step, Opus 5 and GPT-5.6 Sol first object at step 6, and LeanPRM-Verifier-4B † flags step 5.
Figure 7: An incomplete proof. The argument establishes the summed inequality and defines SS at step 19, then stops without producing the two distinct zeros. Under the convention of Section 2 the final step of an argument that stops short is incorrect; every other system accepts all nineteen steps, and LeanPRM-Verifier-4B † flags the last.
Figure 8: The reverse case. Step 8 claims a Lagrange-type identity with the wrong coefficient on the first square, so the checker’s ring normalization fails and the class is algebraic identity error. All four commercial systems and PRM800K-Verifier-4B flag step 8; LeanPRM-Verifier-4B † accepts the proof.
 LeanPRM-BenchHard2VerifyProcessBenchPRMBenchIMO-GB
 exactresponse BAavg. F1first err.BA
Qwen3-0.6B base22.7 ±\pm 0.23.6 ±\pm 1.73.2 ±\pm 0.23.5 ±\pm 0.548.4 ±\pm 0.2
Qwen3-4B (initial policy)48.2 ±\pm 1.337.1 ±\pm 4.574.3 ±\pm 0.542.5 ±\pm 0.553.8 ±\pm 0.1
Qwen3-8B base45.7 ±\pm 1.952.4 ±\pm 1.279.5 ±\pm 0.347.6 ±\pm 0.258.4 ±\pm 0.6
LeanPRM-Verifier-0.6B54.0 ±\pm 2.561.8 ±\pm 1.834.9 ±\pm 1.027.7 ±\pm 0.258.4 ±\pm 1.8
LeanPRM-Verifier-4B74.7 ±\pm 1.872.8 ±\pm 0.974.9 ±\pm 0.447.4 ±\pm 0.266.4 ±\pm 1.1
Appendix
Table 5: Model scale at a fixed budget: LeanPRM verifiers trained from Qwen3 base models of three sizes for 500 updates each with the same recipe, with the untrained models for comparison; mean ±\pm population standard deviation over three decoding seeds. The 4B and 8B models are close on LeanPRM-Bench, PRMBench and IMO-GradingBench, and the 0.6B model is far behind.
Figure 9: A correct attempt: for real tt , 2t≤1+t22t\leq 1+t^{2} . Every step elaborates, so every step is labeled correct. The argument is the standard completion of the square, written as four claims each realized by one tactic. Attempts of this kind account for 6,370 of the 10,634 theorems in LeanPRM.
Figure 10: A reasoning error whose text shows the slip. The statement asks, for k≥2k\geq 2 and every bound NN , for some n>Nn>N dividing the sum of the kk -th powers of its divisors. The attempt proposes n=1n=1 , which cannot exceed an arbitrary NN , and step 4 concedes as much while trying to discharge the bound anyway. Elaboration fails at that step; Stage 2 assigns the class invalid inequality bound, and steps 4 and 5 are labeled incorrect.
Figure 11: An attempt from the labeled pool that is not part of LeanPRM. The statement is that d∣nd\mid n implies 2d−1∣2n−12^{d}-1\mid 2^{n}-1 . Step 3 invokes the true fact that x−yx-y divides xm−ymx^{m}-y^{m} ; the mathematics is sound, but the Lean line names the library lemma in a form the pinned Mathlib does not accept, so elaboration fails there and Stage 2 assigns theorem misapplication. The audit judged steps of this class sound in 26 of 30 cases, which is why the formalization-side classes are excluded from the corpus.
Base modelsQwen3-0.6B, Qwen3-4B, Qwen3-8B, thinking mode enabled
OptimizerGRPO as implemented in VERL, learning rate 10−610^{-6}
Batch64 prompts per update, 8 responses per prompt
Clippingratio clipped at 0.20 below and 0.26 above, dual-clip constant 10
RegularizationKL coefficient 10−310^{-3} , low-variance estimator, no entropy bonus
Loss aggregationsequence mean of token means
Sequence lengths8,192 prompt tokens, 6,656 response tokens
Appendix
Table 6: Training configuration shared by every trained model.

Explore similar work

CardsList
May 19, 2026

Pseudo-Formalization for Automatic Proof Verification

Reliable verification of proofs remains a bottleneck for training and evaluating AI systems on hard mathematical reasoning. Fully formal proofs, in languages like Lean, are easy to verify because they are unambiguous and modular. Most proofs, particularly those written by AI systems, have neither property, and translating them into formal languages remains challenging in many frontier math settings. We propose Pseudo-Formalization (PF), a proof format that captures the modularity and precision of formal proofs while retaining the flexibility of natural language. A Pseudo-Formal proof is decomposed into self-contained modules, each stating its premises, conclusion, and proof in natural language. To verify the correctness of a regular natural language proof, an LLM translates it to Pseudo-Formal and then verifies each module independently, an algorithm we call Block Verification (BV). We evaluate PF+BV on two benchmarks spanning olympiad and research-level mathematics, where it pareto-dominates LLM-as-judge baselines on error-finding precision and recall. To support future work, we release our research-level proof verification benchmark ArxivMathGradingBench.

Slim Barkallah, Luke Bailey, Kaiyue Wen +2

Stanford University

Mathematical Reasoning BenchmarksLLM-as-a-JudgeAutoformalization
AskPDF
Feb 2, 2026

ProofVerifier: A Scalable, Diversity-Driven Framework for Natural-Language Proof Verification

While large language models (LLMs) have achieved strong performance on mathematical problems with verifiable answers, many advanced problems are proof-based and require evaluating full proofs. However, training such verifiers requires diverse and trustworthy question-proof-check (QPC) examples at scale, which are scarce. To address this challenge, we develop a human-audited, LLM-assisted data pipeline that produces large-scale QPC triplets with limited human effort. By systematically varying problem sources, generation strategies, and generator models, the pipeline creates diverse problem-proof pairs spanning multiple difficulty levels, linguistic styles, and error types. We combine multi-LLM agreement with hierarchical human auditing to obtain accurate proof-correctness labels. Using these data, we train generative proof verifiers and introduce an auxiliary fluency filter together with balanced token weighting to stabilize binary-reward long-form verification RL. Experiments show that our verifier improves proof-judgment accuracy across different proof styles and provides useful guidance for test-time selection. Overall, our results provide a practical data and training framework for natural-language proof verification.

Haotong Yang, Zitong Wang, Shijia Kang +7

Peking University, Beijing, China · Tencent

Synthetic Data GenerationMathematical Reasoning
AskPDF
Oct 4, 2026

AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness

Proof auto-formalization translates natural-language (NL) theorems and proofs into a formal language (FL) such as Lean, enabling mechanical verification. Despite rapid progress, research-level proofs often depend on concepts missing from leading proof assistant libraries (e.g., Lean's Mathlib), and successful compilation does not guarantee that a translation preserves the theorem's meaning or the proof's reasoning. Furthermore, aligned NL-FL training data are scarce, and leading agents often rely on costly frontier models and manually engineered harnesses. To address the above issues, we present AIProver, an agentic framework for autonomous proof auto-formalization and proof synthesis (AFPS) that jointly post-trains a 119B open-weight language model and evolves its agentic, tool-calling harness with HarnessEvolve. Verifiers assess type correctness, proof completeness, and semantic correctness, returning rewards and diagnostic certificates that drive model fine-tuning and alternating reinforcement learning via symbolic feedback and HarnessEvolve, a certificate-driven evolutionary search over the whole harness control flow that re-tailors the harness to the updated model. For research-level training and evaluation, we introduce LoCoBench, 58.9k instances from Mathlib, CSLib, Mizar Math Library, and a bounded-arithmetic textbook, with a 771-instance validation split whose theorem-proof pairs have no public Lean formalization. Against 39 frameworks spanning AFPS agents, frontier LLMs, and coding agents, AIProver lifts pass@4 semantic correctness over its Leanstral-1.5 base from 15.7% to 36.7% and outperforms every other open-weight system and Aristotle. As a Claude Code and Codex skill, it lifts their semantic correctness from 41.9% and 34.1% to 79.8% and 62.4%, respectively. Further, it is also 24% cheaper than Numina-Lean-Agent, pushing the accuracy-cost frontier of research-level AFPS.

Prithwish Jana, Viet Bach Hoang, Logan Luna +9

Georgia Institute of Technology, USA · University of Pennsylvania, USA · Foothill College, USA +3

Mathematical Reasoning BenchmarksAutomated Theorem ProvingLean Theorem ProvingAutoformalization
AskPDF