arXiv cs.AI· Rodney Lafuente-Mercado, Salman Rahman, Jingyan Shen, James Shiffer, Saadia Gabriel, Pavel Izmailov·· 3 天前AI 评分39
LeanPRM：用 Lean 为自然语言证明生成过程监督标签
LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification
AI 导读
LeanPRM 利用 Lean 证明助手为自然语言数学证明自动生成步骤级标签，构建了含 10,634 条证明、152K 标注步骤且无需人工标注的数据集。基于 Qwen3-4B 训练的验证器在 200 条证明的 LeanPRM-Bench 上把步骤标签准确率从 48.2 提升到 74.7，而同一基座用 PRM800K 训练仅得 60.3。
正文 · AI 翻译
摘要：AI 系统如今能写出冗长而艰深的数学证明，而逐步核验其有效性正成为瓶颈。一个学习得到的验证器可以低成本地检查证明，但训练它需要为每一步都提供正确性标签，而对于开放式证明，这类标签很难获得。现有方法要么从人工标注者处获取标签，成本高昂；要么从最终答案中推导标签，而证明并没有最终答案；要么在 Lean 中形式化每个证明，这需要专家投入。我们提出 LeanPRM，一个利用 Lean 证明助手为自然语言证明创建步骤级标签的框架。模型在无 Lean 反馈的情况下，同时写出自然语言证明和与之配对的形式化证明。随后 Lean 为每一步打标签，第二个模型则剔除仅由形式化语法导致的失败，从而使负标签标记的是数学上的错误。LeanPRM 包含 10,634 个证明和 152K 个已标注步骤，且无需人工标注。在 LeanPRM 上训练的 Qwen3-4B 验证器，在 200 个证明的留出集（LeanPRM-Bench）上将步骤标签精确准确率从 48.2 提升到 74.7，而同一基座模型在 PRM800K 上训练时仅为 60.3。它还在 IMO 级问题上的 best-of-N 选择中选出更好的证明，并在四个外部验证基准中的三个上优于在 PRM800K 上训练的验证器。在 LeanPRM 上训练可提升从 0.6B 到 8B 参数各规模验证器在 LeanPRM-Bench、Hard2Verify 和 IMO-GradingBench 上的表现。由于这些标签无需人工标注，LeanPRM 可以随形式化陈述的供给而扩展，为人类难以检查的 AI 生成证明提供了一条获得步骤级反馈的路径。
| 评论： | 29 页，9 幅图。项目页面：此 https URL |
| 主题： | 机器学习（cs.LG）；人工智能（cs.AI）；计算机科学中的逻辑（cs.LO） |
| 引用为： | arXiv:2610.17697 [cs.LG] |
| （或 arXiv:2610.17697v1 [cs.LG] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.17697 arXiv 颁发的 DOI，经由 DataCite（待注册） |
提交历史
来自：Rodney Lafuente-Mercado [查看电子邮件]
[v1]
2026 年 10 月 13 日星期二 04:23:36 UTC（306 KB）
来源：arXiv cs.AI · arxiv.org