LeanPRM: Lean-based process supervision for natural-language proof verification

Open-ended natural language proofs have no final answer to check, step-level correctness labels are scarce, making it difficult to train verifiers that read only natural language.

• Scenario: The authors state that AI can already write long and difficult mathematical proofs, including solutions to long-standing open problems, and a fully machine-checked proof of Fermat's Last Theorem. Checking these proofs is harder, especially for non-experts; the authors state there is little supervision available to train future systems.
• Existing shortcomings: Existing outcome and process reward models target problems with short checkable answers, but proof correctness lies in whether each step follows from previous steps. Human annotation is expensive; PRM800K requires about 800,000 step labels, and proofs are harder to judge. Methods that score by whether continuation reaches the correct answer do not apply when there is no final answer; translating informal proofs into Lean is itself difficult and requires expert-level work.
• Observation: Pairing natural language steps with formal steps allows Lean, a precise mechanical checker, to label natural language steps. If the generator sees Lean output, it will fix errors or give up, losing the real errors to be labeled.
• Proposed framework: LeanPRM has the model write paired proofs without checker feedback, labels steps with Lean, then uses a second model call to remove failures caused solely by formal syntax, so negative labels correspond to mathematical errors. The corpus is 10,634 proofs, 152,005 step labels (abstract says 152K), no human annotation, with a held-out LeanPRM-Bench (200 proofs). The authors claim this is, to their knowledge, the first framework to use Lean to scale step-level correctness labels for natural language proofs.

The authors divide related work into process supervision and formal mathematics, and use Lean only to label natural language proofs to connect the two.

Process supervision

• PRM800K (Lightman et al., 2023): Uses human step annotations to scale process supervision for mathematical reasoning. Table 3 marks it as requiring human labor, not covering open-ended proofs, and not giving mathematical error types for failing steps.
• Deriving labels from outcome signals: Math-Shepherd (Wang et al., 2023) estimates step quality using correctness of sampled continuations; OmegaPRM (Luo et al., 2024) extends such annotation with tree search; RL Tango (Zha et al., 2025) trains generative process verifiers directly from outcome rewards. The authors state these labels come from model-generated solution distributions, obtained via human judgment or rollout statistics.
• Earlier comparisons and later uses: Cobbe et al. (2021) introduced outcome-trained verifiers for word problems; Uesato et al. (2022) compared process feedback and outcome feedback on natural language tasks. Later text also mentions extending automatic step labels with rollouts and value estimates, writing verification as generation, and that such verifiers make test-time search effective because models struggle to correct their own reasoning without external feedback.

Using formal systems to label or check

• FoVer (Kamoi et al., 2025): Trains process reward models on formal reasoning traces annotated in Z3 and Isabelle, then evaluates transfer to natural language reasoning. The authors state LeanPRM instead trains directly on natural language competition proofs paired with Lean tactics, and distinguishes mathematical errors from formalization failures.
• Safe (Liu et al., 2025) and Theorem Prover as a Judge (Leang et al., 2025): The former uses Lean 4 to check natural language solutions step by step at inference time for scoring; the latter uses Lean's verdict on whole solutions to select fine-tuning data. Table 3 marks both as not covering open-ended proofs, not providing error types, and not training verifiers that read proof text.
• LeanTutor (Patel et al., 2026): Uses Lean to check student proofs step by step and give feedback. Table 3 marks it as covering open-ended proofs and having error classes, but not training a verifier that reads proof text. The authors state they scale such step labels and use them as training data for a verifier that reads only natural language.

Formal mathematics

• Proof assistants and provers: Lean 4 (de Moura and Ullrich, 2021) and Mathlib are used to create data and train formal theorem provers and autoformalization systems. The text lists DeepSeek-Prover, Kimina-Prover, Goedel-Prover-V2, Seed-Prover, and Lean-STaR which interleaves informal thinking with tactics; miniF2F and PutnamBench track progress.
• Statements and other uses: Autoformalization and Lean Workbook provide statements; informal proofs can be mapped to formal proof sketches. Recent work also uses formal verification to evaluate natural language reasoning, check key steps at inference time, or provide training signals for natural language reasoning and formal proof generation. The authors state their use differs: what is supervised is natural language reasoning, and formal proofs are never model outputs nor appear in its inputs.

Verifier training, evaluation, and baselines

• Training and analogies: The verifier is trained with GRPO (Shao et al., 2024), a variant of PPO that DeepSeek-R1 scaled to reasoning, implemented in VERL. The prover-verifier game comes from Anil et al. (2021), used for language models by Kirchner et al. (2024); a critic that points out errors in outputs (McAleese et al., 2024) is called by the authors the closest analogy outside mathematics.
• Evaluation benchmarks: ProcessBench measures finding the first error step in short solutions from elementary, competition, and olympiad problems, with data including GSM8K and MATH; PRMBench probes failure modes of process reward models; Hard2Verify targets proofs whose correctness is hard to judge. Appendix G discusses how benchmark annotation conventions interact with training conventions.
• Baseline methods and benchmarks: Baselines are untrained Qwen3-4B, PRM800K-Verifier-4B trained with the same recipe on PRM800K human labels, and NuminaMath-Solver-4B trained with reinforcement learning on final-answer rewards on 19,200 NuminaMath problems. Evaluation uses LeanPRM-Bench, Hard2Verify, ProcessBench, PRMBench, IMO-GradingBench.

The authors position their work as: process supervision labels previously came from humans or continuation outcomes, and formal mathematics' precise checking was mainly used to train and evaluate provers that write Lean; LeanPRM uses Lean only to label natural language proofs, and the trained verifier never sees formal proofs. In Table 3, only LeanPRM is marked as: step labels require no human labor, covers open-ended proofs, failing steps have mathematical error types, and trains a verifier that reads proof text.

LeanPRM 用两阶段把 Lean 的编译结果变成自然语言步骤标签：生成器盲写配对证明，检查与分类在生成之后进行，验证器训练时只看自然语言。

设定与标签约定

• 对每条定理陈述，模型一次写出证明，每步是一句数学散文加对应 Lean tactic。模型始终被要求证明定理，从不被要求犯错，因此错误是它认真尝试时自己犯的。
• 生成器看不到所写 Lean 步骤的运行结果。作者给出的理由是：若看得到，模型会修复错误或放弃，真实错误就留不下来。
• 编译成功则每步标为正确。否则第一个失败步及其后每一步标为不正确，因为建立在未确立步骤上的内容也未确立。对“为真但论证不充分”的步骤，这可以与 ProcessBench 不同：后者只在缺失论证影响解答有效性时才算错（Appendix G）。

Stage 1：盲写配对证明

• 起点约 17,800 条互异定理陈述，主要来自 NuminaMath-LEAN 与 Lean-Workbook，其余包括 Pythagoras、Herald、ProofNet、FormalQualBench（Figure 2、Appendix B）。领域为代数、不等式、数论、存在性问题，以及一些微积分和组合。
• NuminaMath 取 Gemini Flash-Lite 标为 hard 的一层；Lean-Workbook 按陈述类别抽样，没有难度标签。作者称许多陈述因难度入选，所以不少认真尝试会失败。
• 一次模型调用按编号步骤生成，只看陈述，不接收检查器反馈。多数定理用 Claude Sonnet 5，较早子集用 Claude Opus 4.8。提示词在 Appendix I，此处不展开其具体约束。

Stage 2：编译、分类与修补

• 冻结的形式证明用 Lean 4 与 Mathlib（均为 v4.25.0-rc2）编译，编译输出不给生成器。因每句有自己的形式步骤，编译错误指向恰好一步。论文未报告这次分类调用使用的模型名称。
• 第二次、也是最后一次模型调用读取陈述、步骤和编译输出，给出三种判定：correct（已编译且自然语言忠实于形式证明）、mathematical error（指出第一个失败步并赋予错误类）、syntax error（只得到一次机会修补对应 Lean 步骤且不改变数学；修补稿仅在随后能编译时保留）。
• 陈述不适定、输出畸形，或散文与形式证明不一致时，证明可被丢弃。不因证明不完整、或需要补入大量新数学才能写完而丢弃；作者把停在未关闭目标之前的尝试保留为推理错误。

语料、错误类与质控

• Stage 2 为 13,940 条陈述产出带标签证明，词法过滤并去掉重复与空证明后剩 13,007。质控后为 10,634 份：6,370 正确、4,264 不正确，152,005 个步骤标签，无人工标注；98% 来自 NuminaMath-LEAN 与 Lean-Workbook。
• Figure 2：NuminaMath 5,312（50.0%），Lean-Workbook 5,071（47.7%），其他 251（2.4%）。Table 4 写明 NuminaMath 提供大部分不正确证明（3,978），Lean-Workbook 提供大部分正确证明（4,787）。十类错误中六类是数学错误，四类是形式化失败。Figure 2 右侧，不正确证明的首错类：无根据假设 33.2%，无效不等式界 17.6%，缺情形或侧条件 17.2%，错误见证或构造 16.7%，代数恒等式错误 13.6%，模或整除错误 1.8%。定义在 Appendix A。
• 质控用 Claude Opus 5 做两次盲审，裁判看不到作者的标签；提示词在 Appendix I。第一次：100 份分层证明中 99 份有可用回答；标为正确的 52 份里异议 1 份；标为不正确的 47 份里，找到错误 27 份、没有 20 份。作者称第二次审计说明这些分歧从何而来。
• Table 1：形式化侧步骤占未过滤池中不正确尝试的 35.8%；每类 30 步中，判为成立的是错误改写方向 28/30、定理误用 26/30、其他 26/30、自动化误用 23/30。两个最大数学类，无根据假设与无效不等式界，均为 13/30。作者因此去掉首错属于形式化侧的全部尝试。另有词法过滤，使自然语言不提及 Lean，并去掉失败步自己宣布错误的不正确证明（Appendix B）。

训练目标与留出基准

• 验证器读定理和编号步骤，先写推理，再给每步 correct 或 incorrect，并给整份证明一个判定；任一步为不正确时，判定必须是不正确。基座为 Qwen3 的 0.6B、4B、8B，thinking mode，用 GRPO。每个证明在温度 1 下采样 8 条，组内归一化奖励作为每个 token 的 advantage。重要性比裁剪到 [0.8, 1.26]，KL 系数 10−3。每次更新 64 份证明，学习率 10−6。主比较每个模型 500 次更新。Appendix J 列出共享超参数。
• 设 Rc、Ri 为真正正确步、真正错误步上的标签召回，该类步数为 0 时设为 1。奖励为 r = 0.7 · R_step + 0.3 · 1[v̂ = v]。含错误时 R_step = R_c R_i，否则为每步都被标为正确的指示。乘积用来排除“全标正确”和“全标错误”两种常数捷径。输出畸形、没有推理段、或判定与自身步骤标签矛盾时奖励为 0。Figure 1 的例子中只标出第 6 步时，Rc 为 1、Ri 为 1/2，Rstep 为 0.5，判定必错，r 为 0.65。
• LeanPRM-Bench 留出 200 条定理，正确与不正确各 100，基准定理不出现在训练数据中。正确证明须 Lean 代码编译通过，且审查模型确认自然语言与形式证明一致；每份不正确证明的首错都是数学错误。指标为 exact step-label accuracy（每一步都标对的证明占比）和 verdict accuracy（整份判定正确的占比）。

Experimental Setup

• Models tested and referenced: Verifiers are trained from Qwen3-0.6B, Qwen3-4B, Qwen3-8B. The main comparison is 4B, 500 updates. Reference prompts include Claude Sonnet 5, Claude Opus 5, Claude Fable 5.1 (Anthropic API, extended thinking, high effort, 16,000 tokens, retried once to 32,000 on truncation or refusal) and GPT-5.6 Sol (Codex command line, all tools disabled, high reasoning effort). Codex prepends its own agent instructions to the paper prompt and does not return reasoning, so that row is prompted via Codex, not a bare API.
• Training data and budget: LeanPRM training split has 10,264 entries (6,170 correct, 4,094 incorrect); after oversampling the smaller verdict grid to balance, the training view is 17,670 rows. The PRM800K baseline instead uses its 70,502 training proofs, converted to the same step-label format. NuminaMath-Solver-4B replaces the verification reward with a final-answer reward, with 19,200 problems. 500 updates cover 32,000 proofs, i.e., 3.12 epochs over LeanPRM training proofs and 0.45 epochs over PRM800K.
• Benchmarks and metrics: LeanPRM-Bench has 200 entries; Table 2 uses exact step-label accuracy; verdict accuracy is defined but no value is given in Table 2. Hard2Verify is response-level balanced accuracy on 200 problems. ProcessBench is the F1 (harmonic mean of incorrect-solution and correct-solution accuracy) averaged over four subsets, 3,400 examples total. PRMBench is first-error accuracy on 6,216 rows, not the default PRMScore. IMO-GradingBench binarizes four-level human scores into fully correct or not, then uses balanced accuracy; 13 of 1,000 entries exceeding the context are removed, leaving 987.
• Reasons for not using the other two default metrics: PRMScore only marks incorrect steps as incorrect, which penalizes the instruction to label everything after the first error as incorrect. IMO-GradingBench does not use four-class accuracy because the verifier gives only binary judgments and about 30% of its proofs are rated correct. Parse failures count as incorrect.
• Replication: Open-weight models use temperature 1 and seeds 42, 43, 44; the mean of three runs and the overall standard deviation are reported. Commercial models are three separate hosted runs with uncontrolled seeds. All models share the same prompt layout and label parser.
• Benchmark replacement: LeanPRM-Bench is fixed before category filtering; 30 incorrect proofs whose first error is on the formalization side are replaced with 30 from the validation split whose first error is a math error, so the validation split has 170 entries (100 correct, 70 incorrect). Models at 500 updates were not trained on these 30 and were not selected on the validation set. The † second stage stops at the best checkpoint on an earlier validation split that contains 17 of these 30 (Appendix B, D).

Main Results

Per Table 2, the table below shows the mean of three runs. Rows are models, not pooled averages. † is 1,582 updates with different data; the paper treats it only as a reference. GPT-5.6 Sol is omitted from the table; its five-column means are 75.3, 85.5, 79.8, 47.1, 83.2.

Swipe horizontally to read the table

Model	LeanPRM-Bench exact	Hard2Verify response BA	ProcessBench avg. F1	PRMBench first err.	IMO-GB BA
Qwen3-4B (initial)	48.2	37.1	74.3	42.5	53.8
PRM800K-Verifier-4B	60.3	63.1	83.0	43.3	57.0
NuminaMath-Solver-4B	48.3	33.6	71.2	41.5	52.4
LeanPRM-Verifier-4B	74.7	72.8	74.9	47.4	66.4
LeanPRM-Verifier-4B†	78.7	79.0	72.6	48.3	71.8
Claude Sonnet 5	71.7	83.1	84.9	48.6	80.7
Claude Opus 5	80.3	81.0	84.5	47.6	81.8
Claude Fable 5.1	78.3	86.0	86.0 not reported	48.6	85.4

In the table above, the ProcessBench cell for Claude Fable 5.1 should read 84.7 from Table 2, not 86.0; 86.0 is its Hard2Verify mean. Correction in the next sentence: Fable 5.1's ProcessBench avg. F1 is 84.7 (Table 2).

• The authors state that at the same 500 updates, LeanPRM-Verifier-4B is the highest in its group on four of five benchmarks, with point gains over PRM800K-Verifier-4B of 14.4 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.
• The authors attribute this lead to distribution and labeling conventions: ProcessBench's short solutions match the PRM800K training distribution, and missing arguments count as errors only when they affect solution validity (Appendix G).
• The authors state that reinforcement learning on solving does not produce a verifier: NuminaMath-Solver-4B raises its own verification problems' final-answer accuracy from 30.0% to 47.5%, differs from the untrained model by no more than 1 point on LeanPRM-Bench, and is below the untrained model on every external benchmark. The commercial reference models lead on Hard2Verify, ProcessBench, and IMO-GradingBench; the authors do not claim they are uniformly higher on LeanPRM-Bench or PRMBench.

Test-Time Selection

• Best-of-N is tested on IMO-GradingBench: 30 problems, about 33 human-graded proofs each. After sampling N proofs, the verifier randomly picks one among those it accepts; if none are accepted, it picks randomly among all. It records whether the picked proof is rated correct.
• Figure 4 right: at N=16, LeanPRM-Verifier-4B is 35.9% and random selection is 32.4%. The authors state its advantage grows with N up to N=8. The paper does not give the exact proportion at N=8.
• PRM800K-Verifier-4B with the same recipe and budget is 33.2%. It accepts about 79% of proofs while only 30% are rated correct; the authors state its selection is close to random. The figure averages 30 problems and three decoding seeds, with shading at 1 standard deviation.

Model Scale

• Figure 5 and Table 5 compare 0.6B, 4B, and 8B before and after training, all at 500 updates. The authors state training helps every scale on LeanPRM-Bench, Hard2Verify, and IMO-GradingBench; relative to the untrained model, the gains on LeanPRM-Bench are reported as 31 points for 0.6B, 27 points for 4B, and 29 points for 8B.
• Untrained 8B is 45.7 on LeanPRM-Bench, below untrained 4B's 48.2, so the larger gain only brings it to parity with 4B. After training they are 74.7 and 75.0; on PRMBench and IMO-GradingBench the difference is within 0.8 points. On ProcessBench, 8B is higher by 4.4 points; on Hard2Verify, 4B is 72.8 and 8B is 66.7.
• After training, 0.6B is 54.0 on LeanPRM-Bench, which the authors state is still 21 points below 4B. Before training, fewer than one-fifth of its proofs on Hard2Verify, ProcessBench, and PRMBench have well-formed labels, which the authors use to explain its near-zero pre-training scores. On Hard2Verify, 9% of 8B's responses are unparseable versus 2% for 4B; on parseable answers they are 74.7 and 75.1, and the paper does not state which model corresponds to which. Before training, 8B is highest on ProcessBench and PRMBench at 79.5 and 47.6; after training it is 79.3 and 48.0, within 0.4 points of untrained.

Common Errors of Commercial Models

• Section 2.2: under the same prompt, the four commercial models' mean exact step-label accuracy on LeanPRM-Bench ranges from 71.7 to 80.3, matching Sonnet 5's 71.7 and Opus 5's 80.3 in Table 2. In the original reference runs, all four mislabel the same 26 proofs.
• Appendix C: LeanPRM-Verifier-4B† labels all steps correctly on 8 of these, 6 incorrect and 2 correct; across three seeds, the exact proportion on these 26 is 29.5%, versus 7.7% for the untrained model and 11.5% for PRM800K-Verifier-4B. The reverse case accounts for 12 of the 128 proofs that all four get right. Appendix examples show the remaining cases follow the checker's conventions, e.g., an argument that stops before the conclusion has its last step counted as incorrect.
• Appendix G: the authors believe the gap on ProcessBench is mostly due to labeling conventions, but they do not test this directly. Across the three checkpoints of the run behind † (532, 1,282, 1,332 updates), labels strictly earlier than the reference step go from 158 to 236 to 379. Only the latter two checkpoints share training data; the authors state the trend is consistent with this explanation but do not isolate it.

Other Ablations and Analyses

• Figure 4 left: exact step-label accuracy of three scales on the LeanPRM validation split; the 4B point at update 300 is measured separately with the same greedy protocol. The paper does not give per-point values on the curve.
• Figure 4 middle: PRM800K-Verifier-4B by exact accuracy and NuminaMath-Solver-4B by final-answer accuracy show little change in the latter half on their respective validation splits. The authors use this to state that a 500-step budget is a reasonable setting.
• Appendix B: when building the split, incorrect proofs whose failed step self-reports an error are removed; the earlier joint pipeline removes 55.2% and the blind-writing pipeline removes 2.3%.
• Appendix B: Stage 1's Lean rows are not filtered for sorry, admit, or native_decide; these appear in 605 proofs. One explicit sorry is kept in the positive training set, and transitive dependencies are not checked.
• Appendix D: † is a single continuous run: 532 updates on 3,449 training proofs generated earlier jointly, 750 updates on the unfiltered pool (best validation checkpoint at 808), then 300 updates on LeanPRM, totaling 1,582. The authors state the data and lengths differ, so it is only a reference.
• The paper does not report separate ablations of learning rate, KL coefficient, or sampling count; the above hyperparameters are shared by all trained models, and 8B additionally uses parameter and optimizer offloading and tensor parallelism across two GPUs.

Limitations and future directions noted by the authors

• The separation of mathematical errors from formalization failures depends on model classification, and only one judge model checks on samples, so boundary steps may still be mislabeled (Limitations).
• Comparisons were made with PRM800K human labels, but training was not done on the same batch of proofs with LLM judge labels, so it is not yet possible to distinguish how much of the gain comes from labels versus from proof-genre data (Limitations).
• LeanPRM-Bench shares the same pipeline and the same Claude generator as the training data; evidence for verifier generalization comes mainly from four external benchmarks (Limitations).
• Negative examples come from Claude's own errors, covering a narrower range of errors than a proof verifier might need to detect (Limitations).
• The authors believe the gap on ProcessBench is mostly due to annotation conventions, but they did not directly test this; auditing premature marking could confirm it (Appendix G).
• Future directions: the same data-generation method might transfer to open-ended tasks without final answers but with precise checkable parts, such as code test suites or scientific simulators; generating new theorem statements to make the corpus exceed existing formal collections in scale and difficulty; the trained verifier can serve as a reward model for training provers and for giving step-level feedback on proofs that are hard for humans to check (Future work).

Experimental coverage

• Open-source base models tested are Qwen3-0.6B, Qwen3-4B, Qwen3-8B; main comparisons and scaling experiments use 500 updates with the same GRPO recipe (Section 3, Appendix F).
• Evaluation sets are LeanPRM-Bench 200 proofs, Hard2Verify, ProcessBench 3,400 cases, PRMBench 6,216 lines, IMO-GradingBench 987 after removing 13; open-weight results are from three runs with seeds 42, 43, 44 (Section 3, Appendix E).
• Baselines include untrained Qwen3, PRM800K human labels, and solver training with NuminaMath final-answer rewards; also prompt references for Claude Sonnet 5, Claude Opus 5, Claude Fable 5.1, GPT-5.6 Sol (Section 3).
• Proof generation uses Claude Sonnet 5 and Claude Opus 4.8; blind review judge is Claude Opus 5, first 100 proofs, second 30 steps per class (Section 2, Section 2.1).
• The paper does not report the model names used for Stage 2 classification and syntax patching; Table 2 does not report verdict accuracy values (Section 2, Section 3).

LeanPRM uses Lean offline to label natural language proof steps, then trains a verifier that reads only natural language.

• Problem: Open-ended proofs have no checkable final answer. Human step labels are expensive, methods that back-propagate labels from final answers do not apply, and formalizing each proof requires experts.
• Method: The generator sees only the statement, writes each step's prose and paired Lean tactic blindly, without seeing checker feedback. Lean 4 and Mathlib (v4.25.0-rc2) compile sequentially: success means all steps correct; otherwise the first failing step and subsequent steps are incorrect. Another call distinguishes mathematical errors from syntax errors; syntax is only patched and rechecked once. After removing formalization-side first errors, the corpus is 10,634 proofs, 152,005 labels. The verifier is trained with GRPO, with a reward multiplying recall of correct steps and recall of incorrect steps, plus a whole-proof verdict.
• Main results: Under the same recipe and 500 updates, LeanPRM-Verifier-4B achieves exact step-label accuracy of 74.7 on LeanPRM-Bench, PRM800K-Verifier-4B 60.3, untrained Qwen3-4B 48.2. The authors report the former is higher by 9.7, 4.1, 9.4 points on Hard2Verify, PRMBench, IMO-GradingBench respectively; on ProcessBench the latter is higher by 8.1 points. A solver model trained with final-answer rewards does not become a verifier.
• Other results: At N=16, LeanPRM-Verifier-4B selects the correct proof on IMO-GradingBench 35.9% of the time, random 32.4%, PRM800K version 33.2%. From 0.6B to 8B, performance rises after training on LeanPRM-Bench, Hard2Verify, IMO-GradingBench; 8B is not higher than 4B on every external benchmark.
• Authors' conclusion: Formal tools can be used only for offline data creation, thus training verifiers that check natural language without automatic formalization. Labels require no human annotation, and the corpus can grow with the supply of formal statements. The authors also state that how much of the gain comes from the labels themselves has not been separated from LLM judge labels, negative examples come from Claude's own errors, and the held-out set shares the same pipeline as training.