LeanPRM：基于Lean的自然语言证明验证过程监督方法
LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification
AI总结：
本文提出LeanPRM框架，利用Lean证明助手为自然语言数学证明生成无人工标注的步骤级标签，训练的验证器在多个基准上性能显著优于基于PRM800K训练的模型。
摘要：
当前AI系统能够生成冗长且复杂的数学证明，但检查其每一步的有效性正成为瓶颈。学习得到的验证器可低成本检查证明，但其训练需要每一步的正确性标签，而开放式证明难以获取此类标签。现有方法要么依赖人工标注（成本高昂），要么从最终答案推导（证明无最终答案），且在Lean中形式化每个证明需要专家精力。本文提出LeanPRM框架，利用Lean证明助手为自然语言证明创建步骤级标签：模型生成自然语言证明及配对的形式化证明（无需Lean反馈），Lean为每一步标注，第二个模型仅丢弃形式语法导致的失败，使负标签标记数学错误。LeanPRM包含10634个证明、152K个标注步骤，无人工标注。在LeanPRM-Bench（200个证明的保留集）上，基于LeanPRM训练的Qwen3-4B验证器将精确步骤标签准确率从48.2提升至74.7，而相同基础模型在PRM800K上训练时准确率为60.3；在IMO级问题的N选最优选择中，其能选出更优证明，且在4个外部验证基准中的3个上优于PRM800K训练的验证器。在LeanPRM-Bench、Hard2Verify和IMO-GradingBench上，从0.6B到8B参数的各规模验证器，经LeanPRM训练后性能均提升。由于标签无需人工标注，LeanPRM可随形式化陈述的供应扩展，为人类难以检查的AI生成证明提供步骤级反馈路径。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
