AI与世界难题 · 数学 · arXiv · 2026-10-19
LeanPRM：基于 Lean 的自然语言证明验证过程监督
原标题: LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification
对 AI 撰写的长篇证明进行逐步验证，需要每一步的正确性标签，而这些标签靠人工获取成本高昂。LeanPRM 借助 Lean 证明助手为自然语言证明的每一步打标签，无需任何人工标注。基于它训练的 Qwen3-4B 验证器，在 LeanPRM-Bench 上的步骤标签准确率从 48.2 提升到 74.7，高于在 PRM800K 上训练所得的 60.3。