LeanPRM：用Lean为自然语言证明生成步骤级监督

LeanPRM用Lean自动生成步骤标签，无需人工标注即可训练证明验证器。

资讯摘要

论文提出LeanPRM框架，利用Lean证明助手为自然语言数学证明自动生成步骤级正确性标签：模型同时写出自然语言证明与配对形式化证明，Lean逐步标注，再由第二个模型剔除仅由形式语法导致的失败，使负标签对应数学错误。数据集含10,634个证明、152K个标注步骤，无需人工标注。作者报告，基于Qwen3-4B训练的验证器在200个证明的LeanPRM-Bench上步骤标签准确率从48.2提升至74.7，而用PRM800K训练同一基座模型为60.3。

要点速读

1. LeanPRM用Lean对配对形式化证明逐步打标签，再由第二模型过滤纯语法失败，全程无人工标注。
2. 数据集含10,634个证明、152K个标注步骤；作者报告Qwen3-4B验证器在LeanPRM-Bench上准确率由48.2升至74.7，PRM800K训练为60.3。
3. 作者报告该方法在IMO级问题的最佳N选优中选出更好证明，并在四个外部验证基准中的三个优于PRM800K训练验证器。

中文摘要由 AI 根据公开来源生成，可能存在理解偏差；具体能力、数字、开放时间等信息请以原文为准。
采集于 2026/11/5 08:00:38（北京时间）。 arXiv 日期为本次公告时间，论文初次投稿日期请查看原文版本记录。