LeanPRM：用形式化证明为自然语言数学推理提供逐步监督

导语

大型语言模型已经能够生成很长、很复杂的数学证明，但“看起来合理”并不等于每一步都正确。对于开放式证明，系统不能只检查最终答案，因为证明往往没有一个简单的最终答案可供对照；如果让人类逐步审核，成本又会随着证明长度快速上升。如何获得规模化、可靠的过程监督，成为数学推理系统的重要瓶颈。

LeanPRM提出了一条结合自然语言与形式化验证的路径：让模型先写出自然语言证明，同时生成配套的Lean证明，再由Lean证明助手逐步检查，从而自动产生步骤级标签。

核心方法

• 双轨生成：模型在没有Lean即时反馈的情况下，同时产出自然语言证明和形式化证明，避免把训练过程变成单纯的代码调试。
• Lean自动判定：形式化证明中的每个步骤都接受Lean检查，系统据此得到正负监督信号。
• 过滤语法噪声：形式化表达失败不一定代表数学推理错误。研究使用第二个模型识别这类由语法、表达或形式化对齐造成的失败，尽量保留真正反映数学错误的负标签。
• 构建验证数据：LeanPRM包含10,634份证明和约15.2万个带标签步骤，全程不依赖人工标注。

实验结果

在包含200份留出证明的LeanPRM-Bench上，使用LeanPRM训练的Qwen3-4B验证器，逐步标签的精确率从基础模型的48.2%提升至74.7%。作为对比，使用PRM800K训练的同规格验证器达到60.3%。在IMO级问题的best-of-N证明选择中，LeanPRM也能帮助系统挑选出更好的证明；在四个外部验证基准中的三个上，它超过了PRM800K版本。研究还报告称，从0.6B到8B的不同规模验证器都能从该训练数据中获益。

意义与局限

LeanPRM的价值不只是增加了一组数学数据，而是提供了一个可扩展的标签生产机制。形式化系统承担“可执行检查器”的角色，语言模型则负责把自然语言推理与形式化表达连接起来。这种分工有望降低过程奖励模型对人工逐步审阅的依赖，也为长链条推理的自动评估提供更细粒度的信号。

不过，方法仍依赖自然语言证明与Lean证明之间的配对质量，并需要额外模型区分数学错误和形式化失败。Lean检查通过也主要说明对应形式化陈述在给定环境下成立，不能自动解决自然语言表述是否完整、是否忠实映射原意等问题。因此，LeanPRM更适合作为验证器训练和筛选工具，而不是对所有数学推理质量的一次性判决。

总体来看，LeanPRM展示了形式化证明助手如何从“最终裁判”转变为过程监督数据的生产器，为训练更可靠的数学推理验证器提供了可行方向。

来源：Hugging Face Daily Papers