LeanPRM：为自然语言证明验证提供基于 Lean 的过程监督

开放式自然语言证明没有最终答案可核对，逐步正确性标签稀缺，难以训练只读自然语言的验证器。

• 场景：作者称 AI 已能写出长而难的数学证明，包括长期开放问题的解答，以及 Fermat 最后定理的完整机器检验证明。核对这些证明更难，对非专家尤其如此；作者称训练未来系统可用的监督很少。
• 现有不足：既有 outcome 与 process reward model 面向有短可核对答案的问题，而证明的正确性在于每一步是否由前面的步骤推出。人工标注昂贵，PRM800K 约需 800,000 个步骤标签，证明更难判断。用续写能否到达正确答案来打分的方法，在没有最终答案时不适用；把非正式证明译成 Lean 本身困难，且要专家级工作。
• 观察：把自然语言步骤与形式步骤配对后，可用 Lean 这一精确机械检查器给自然语言步骤打标签。若生成器看得到 Lean 输出，它会修正错误或放弃，要标注的真实错误就会丢失。
• 提出的框架：LeanPRM 让模型在无检查器反馈下写出配对证明，由 Lean 标注步骤，再用第二次模型调用去掉仅由形式语法造成的失败，使负标签对应数学错误。语料为 10,634 份证明、152,005 个步骤标签（摘要写 152K），无人工标注，并留出 LeanPRM-Bench（200 份）。作者称据其所知，这是首个用 Lean 规模化产生自然语言证明步骤级正确性标签的框架。

作者把相关工作分成过程监督与形式数学两条线，并用 Lean 只给自然语言证明打标签来连接二者。

过程监督

• PRM800K（Lightman et al., 2023）：用人工步骤标注扩大数学推理的过程监督。Table 3 将其标为需要人工、不覆盖开放式证明、不给失败步数学错误类型。
• 从结果信号派生标签：Math-Shepherd（Wang et al., 2023）用采样续写的正确性估计步骤质量；OmegaPRM（Luo et al., 2024）用树搜索扩展这类标注；RL Tango（Zha et al., 2025）直接从 outcome 奖励训练生成式过程验证器。作者称这些标签来自模型生成的解答分布，经人工判断或 rollout 统计得到。
• 更早比较与后续用法：Cobbe et al. (2021) 为文字题引入 outcome 训练的验证器；Uesato et al. (2022) 在自然语言任务上比较过程反馈与结果反馈。后文还写到用 rollout 与价值估计扩展自动步骤标签、把验证写成生成，以及此类验证器使测试时搜索有效，因为模型难以在没有外部反馈时纠正自己的推理。

用形式系统标注或检查

• FoVer（Kamoi et al., 2025）：在 Z3 与 Isabelle 标注的形式推理轨迹上训练过程奖励模型，再评估向自然语言推理的迁移。作者称 LeanPRM 改为直接在与 Lean tactic 配对的自然语言竞赛证明上训练，并区分数学错误与形式化失败。
• Safe（Liu et al., 2025）与 Theorem Prover as a Judge（Leang et al., 2025）：前者在推断时用 Lean 4 逐步检查自然语言解答来打分；后者用 Lean 对整份解答的判定选择微调数据。Table 3 将二者的开放式证明、错误类型、以及训练阅读证明文本的验证器标为否。
• LeanTutor（Patel et al., 2026）：用 Lean 逐步检查学生证明并给反馈。Table 3 将其标为覆盖开放式证明且有错误类，但不训练阅读证明文本的验证器。作者称自己把这类步骤标签规模化，用作只读自然语言的验证器的训练数据。

形式数学

• 证明助手与证明器：Lean 4（de Moura and Ullrich, 2021）与 Mathlib 被用来造数据并训练形式定理证明器和自动形式化系统。文中列举 DeepSeek-Prover、Kimina-Prover、Goedel-Prover-V2、Seed-Prover，以及把非正式思考与 tactic 交错的 Lean-STaR；miniF2F 与 PutnamBench 用于追踪进展。
• 陈述与其他用法：自动形式化与 Lean Workbook 等提供陈述；非正式证明可映射为形式证明草稿。近期工作还用形式验证评估自然语言推理、在推断时检查关键步骤，或为自然语言推理与形式证明生成提供训练信号。作者称自己的用法不同：被监督的是自然语言推理，形式证明从不是模型输出，也不出现在其输入中。

验证器训练、评测与基线

• 训练与类比：验证器用 GRPO（Shao et al., 2024）训练，它是 PPO 的变体，DeepSeek-R1 将其扩到推理，实现于 VERL。证明器—验证器博弈来自 Anil et al. (2021)，Kirchner et al. (2024) 将其用于语言模型；指出输出中错误的 critic（McAleese et al., 2024）被作者称为数学之外最接近的类比。
• 评测基准：ProcessBench 衡量在小学、竞赛与奥林匹克短解答中找出第一个错误步骤，数据包括 GSM8K 与 MATH；PRMBench 探测过程奖励模型的失败模式；Hard2Verify 针对正确性难以判定的证明。Appendix G 讨论基准标注约定与训练约定如何相互作用。
• 基线方法与基准：对照为未训练 Qwen3-4B、同一配方训在 PRM800K 人类标签上的 PRM800K-Verifier-4B，以及在 19,200 道 NuminaMath 题上用最终答案奖励做强化学习的 NuminaMath-Solver-4B。评测用 LeanPRM-Bench、Hard2Verify、ProcessBench、PRMBench、IMO-GradingBench。

作者的定位是：过程监督的标签以往来自人工或续写结果，形式数学的精确检查主要用于训练和评估写 Lean 的证明器；LeanPRM 只用 Lean 给自然语言证明打标签，训练出的验证器从不看到形式证明。Table 3 中，只有 LeanPRM 同时被标为：步骤标签无需人工、覆盖开放式证明、失败步有数学错误类型、并训练阅读证明文本的验证器。

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（整份判定正确的占比）。

实验设置

• 被测与参照模型：从 Qwen3-0.6B、Qwen3-4B、Qwen3-8B 训练验证器。主比较是 4B、500 次更新。参照提示 Claude Sonnet 5、Claude Opus 5、Claude Fable 5.1（Anthropic API，extended thinking，high effort，16,000 token，截断或拒答重试一次到 32,000）和 GPT-5.6 Sol（Codex 命令行，工具全部关闭，high reasoning effort）。Codex 会在论文提示前加上自己的智能体说明，且不返回推理，故该行是经 Codex 提示，不是裸 API。
• 训练数据与预算：LeanPRM 训练分割 10,264 条（正确 6,170、不正确 4,094）；较小判定格过采样到均衡后，训练视图为 17,670 行。PRM800K 基线改用其 70,502 份训练证明，并转成同一逐步标签格式。NuminaMath-Solver-4B 把验证奖励换成最终答案奖励，题量为 19,200。500 次更新覆盖 32,000 份证明，即 LeanPRM 训练证明上 3.12 遍、PRM800K 上 0.45 遍。
• 基准与指标：LeanPRM-Bench 200 份，Table 2 用 exact step-label accuracy；verdict accuracy 有定义，Table 2 未给数值。Hard2Verify 为 200 题的响应级平衡准确率。ProcessBench 为四个子集上的 F1（错误解答与正确解答准确率的调和平均）再平均，共 3,400 例。PRMBench 为 6,216 行的 first-error accuracy，不用默认 PRMScore。IMO-GradingBench 把四级人类评分二值化为完全正确与否后的平衡准确率；1,000 条中 13 条超上下文被去掉，剩 987。
• 不用另外两个默认指标的理由：PRMScore 只把错误步标为不正确，会惩罚“首错之后全部标不正确”的指令。IMO-GradingBench 不用四分类准确率，因为验证器只给二值判定，且其中约 30% 的证明被评为正确。解析失败计为错。
• 重复：开放权重模型温度 1，种子 42、43、44，报告三次均值和总体标准差。商用模型为三次独立托管运行，种子不受控。所有模型同一提示布局和标签解析器。
• 基准替换：LeanPRM-Bench 在类别过滤前固定，其中 30 份不正确证明的首错属形式化侧，后用验证分割里首错为数学错误的 30 份替换，故验证分割为 170 条（正确 100、不正确 70）。500 次更新的模型都未在这 30 份上训练，也未按验证集选择。† 的第二阶段停在更早验证分割的最佳检查点，该分割含这 30 份中的 17 份（Appendix B、D）。

主结果

据 Table 2，下表为三次运行均值。行是模型，不是合并后的平均值。† 为 1,582 次更新且数据不同，论文只作参照。表中省略 GPT-5.6 Sol，其五列均值为 75.3、85.5、79.8、47.1、83.2。

表格较宽，可左右滑动

模型	LeanPRM-Bench exact	Hard2Verify response BA	ProcessBench avg. F1	PRMBench first err.	IMO-GB BA
Qwen3-4B（初始）	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 未报告	48.6	85.4

上表 Claude Fable 5.1 的 ProcessBench 格应读 Table 2 原文 84.7，不是 86.0；86.0 是其 Hard2Verify 均值。更正见下一句：Fable 5.1 的 ProcessBench avg. F1 为 84.7（Table 2）。

• 作者称同等 500 次更新下，LeanPRM-Verifier-4B 在五个基准中的四个上为该组最高，高出 PRM800K-Verifier-4B 的点数为 LeanPRM-Bench 14.4、Hard2Verify 9.7、PRMBench 4.1、IMO-GradingBench 9.4；PRM800K-Verifier-4B 在 ProcessBench 上领先 8.1 个点。
• 作者认为这一领先与分布和标注约定有关：ProcessBench 的短解答与 PRM800K 训练分布相同，且缺失论证只在影响解答有效性时才算错（Appendix G）。
• 作者称在求解上做强化学习并不产生验证器：NuminaMath-Solver-4B 把自身验证题的最终答案准确率从 30.0% 升到 47.5%，在 LeanPRM-Bench 上与未训练模型相差不超过 1 个点，并在每个外部基准上低于未训练模型。商用参照模型在 Hard2Verify、ProcessBench 和 IMO-GradingBench 上领先；作者未称它们在 LeanPRM-Bench 或 PRMBench 上一律更高。

测试时选择

• 在 IMO-GradingBench 上测 best-of-N：30 道题，每题约 33 份人工评分证明。抽 N 份后，验证器在其接受的证明中随机挑一份；若无一接受，则在全部中随机挑。记录挑中的证明是否被评为正确。
• Figure 4 右：N=16 时，LeanPRM-Verifier-4B 为 35.9%，随机选择为 32.4%。作者称其优势随 N 增大，直到 N=8。论文未给出 N=8 的具体比例。
• 同一配方和预算的 PRM800K-Verifier-4B 为 33.2%。它接受约 79% 的证明，而被评为正确的只有 30%，作者称其挑选与随机相差不大。图为 30 题、三个解码种子的平均，阴影为 1 个标准差。

模型规模

• Figure 5 与 Table 5 比较 0.6B、4B、8B 训练前后，均为 500 次更新。作者称训练在 LeanPRM-Bench、Hard2Verify、IMO-GradingBench 上对每个规模都有帮助；相对未训练模型，LeanPRM-Bench 上的增益作者记为 0.6B 的 31 个点、4B 的 27 个点、8B 的 29 个点。
• 未训练 8B 在 LeanPRM-Bench 上为 45.7，低于未训练 4B 的 48.2，故更大的增益只把它带到与 4B 相当。训练后二者为 74.7 与 75.0；PRMBench 与 IMO-GradingBench 上相差在 0.8 个点以内。ProcessBench 上 8B 高 4.4 个点，Hard2Verify 上 4B 为 72.8、8B 为 66.7。
• 0.6B 训练后 LeanPRM-Bench 为 54.0，作者称仍比 4B 低 21 个点。训练前它在 Hard2Verify、ProcessBench、PRMBench 上形成良好标签的证明少于五分之一，作者用这一点解释其训练前接近零分。8B 在 Hard2Verify 上 9% 的回答无法解析，4B 为 2%；可解析答案上二者为 74.7 与 75.1，论文未写明各自对应哪个模型。8B 训练前 ProcessBench、PRMBench 最高，为 79.5 与 47.6，训练后为 79.3 与 48.0，与未训练相差在 0.4 个点以内。

商用模型的共同误判

• Section 2.2：同一提示下，四个商用模型在 LeanPRM-Bench 上的 mean exact step-label accuracy 为 71.7 到 80.3，与 Table 2 中 Sonnet 5 的 71.7、Opus 5 的 80.3 相同。原始参照运行中，四者误标同一 26 份证明。
• Appendix C：LeanPRM-Verifier-4B† 把其中 8 份的逐步标签全部标对，6 份不正确、2 份正确；三个种子上，这 26 份的精确比例为 29.5%，未训练模型 7.7%，PRM800K-Verifier-4B 为 11.5%。反向情形占四者都对的 128 份中的 12 份。附录示例说明其余情况沿检查器约定，例如停在结论之前的论证，其最后一步算不正确。
• Appendix G：作者认为 ProcessBench 上的差距多半来自标注约定，但没有直接检验。† 背后那次运行的三个检查点（532、1,282、1,332 次更新）上，严格早于参考步的标记从 158 到 236 再到 379。只有后两个检查点共享训练数据，作者称趋势与这一解释相符，但没有把它分离出来。

其他消融与分析

• Figure 4 左：三规模在 LeanPRM 验证分割上的 exact step-label accuracy；4B 第 300 次更新的点用同一贪心协议另测。论文未给出曲线上的逐点数值。
• Figure 4 中：PRM800K-Verifier-4B 按精确准确率、NuminaMath-Solver-4B 按最终答案准确率，各自验证分割上后半段变化不大。作者据此称 500 步预算是合理设置。
• Appendix B：构建分割时，失败步自报错误的不正确证明被去掉，较早联合流程去掉 55.2%，盲写流程去掉 2.3%。
• Appendix B：Stage 1 的 Lean 行未过滤 sorry、admit、native_decide，三者出现在 605 份证明中；正例训练集有一份显式 sorry 被保留，传递依赖未检查。
• Appendix D：† 为单次连续运行，532 次更新用较早联合生成的 3,449 份训练证明，750 次用未过滤池（最佳验证检查点为 808），再 300 次用 LeanPRM，共 1,582 次。作者称数据与长度都不同，故只作参照。
• 论文未报告独立的学习率、KL 系数或采样条数消融；上述超参数对所有训练模型共享，8B 另使用参数与优化器卸载，以及两张 GPU 上的张量并行。

作者指出的局限与后续方向

• 数学错误与形式编码失败的分离依赖模型分类，且只用一个裁判模型在样本上检查，边界步骤仍可能带错标签（Limitations）。
• 与 PRM800K 的人类标签做过比较，但没有在同一批证明上用 LLM 裁判的标签训练，因此还不能区分增益有多少来自标签、有多少来自证明体裁的数据（Limitations）。
• LeanPRM-Bench 与训练数据同一管道、同一 Claude 生成器，验证器能否泛化，证据主要来自四个外部基准（Limitations）。
• 负例来自 Claude 自己的错误，覆盖的错误范围可能比证明验证器应检测的更窄（Limitations）。
• 作者认为 ProcessBench 上的差距多半来自标注约定，但没有直接检验；对过早标记做审计可以确定这一点（Appendix G）。
• 后续方向：同一造数方法或可迁到没有最终答案、但有精确检查器可核部分的开放式任务，例如代码的测试套件或科学模拟器；生成新定理陈述，使语料在规模和难度上超出既有形式化文集；训好的验证器可作奖励模型，用于训练证明器，以及对人难以检查的证明给步骤反馈（Future work）。

实验覆盖范围

• 开源被测基座为 Qwen3-0.6B、Qwen3-4B、Qwen3-8B；主比较与规模实验均为 500 次更新、同一 GRPO 配方（Section 3、Appendix F）。
• 评测集为 LeanPRM-Bench 200 份、Hard2Verify、ProcessBench 3,400 例、PRMBench 6,216 行、IMO-GradingBench 去掉 13 条后 987 条；开放权重结果为种子 42、43、44 的三次运行（Section 3、Appendix E）。
• 对照包括未训练 Qwen3、PRM800K 人类标签、NuminaMath 最终答案奖励的求解训练；另有 Claude Sonnet 5、Claude Opus 5、Claude Fable 5.1、GPT-5.6 Sol 的提示参照（Section 3）。
• 证明生成使用 Claude Sonnet 5 与 Claude Opus 4.8；盲审裁判为 Claude Opus 5，第一次 100 份、第二次每类 30 步（Section 2、Section 2.1）。
• 论文未报告 Stage 2 分类与语法修补所调用的模型名称；Table 2 未报告 verdict accuracy 的数值（Section 2、Section 3）。

LeanPRM 用 Lean 离线给自然语言证明打步骤标签，再训练只读自然语言的验证器。

• 问题：开放式证明没有可核对的最终答案。人工步骤标签贵，从最终答案回传标签的方法用不上，逐份形式化又要专家。
• 方法：生成器只看陈述，盲写每步散文及配对的 Lean tactic，看不到检查器反馈。Lean 4 与 Mathlib（v4.25.0-rc2）顺序编译：成功则全步正确，否则首个失败步及之后为不正确。另一次调用区分数学错误与语法错误，语法只许修补并复查一次。去掉形式化侧首错后，语料为 10,634 份证明、152,005 个标签。验证器用 GRPO 训练，奖励把正确步召回与错误步召回相乘，再加上整份判定。
• 主结果：同一配方、500 次更新下，LeanPRM-Verifier-4B 在 LeanPRM-Bench 上的 exact step-label accuracy 为 74.7，PRM800K-Verifier-4B 为 60.3，未训练 Qwen3-4B 为 48.2。作者报告前者在 Hard2Verify、PRMBench、IMO-GradingBench 上分别高出 9.7、4.1、9.4 个点；ProcessBench 上后者高出 8.1 个点。用最终答案奖励训练的求解模型没有变成验证器。
• 其他结果：N=16 时，LeanPRM-Verifier-4B 在 IMO-GradingBench 上选中正确证明的比例为 35.9%，随机为 32.4%，PRM800K 版本为 33.2%。0.6B 到 8B 在 LeanPRM-Bench、Hard2Verify、IMO-GradingBench 上训练后上升；8B 并不在每个外部基准上都高于 4B。
• 作者的结论：形式工具可以只在离线建数据时使用，从而训练检查自然语言的验证器，而不必做自动形式化。标签不需人工标注，语料可随形式陈述的供给增长。作者同时写明，增益有多少来自标签本身尚未与 LLM 裁判标签分开，负例来自 Claude 自身错误，留出集又与训练同管道。