LeanPRM:用 Lean 自动标注 15.2 万步骤,4B 验证器准确率 48.2→74.7
Pavel_Izmailov · x · 2026-11-07
Pavel Izmailov 团队发布论文 LeanPRM：用 Lean 证明助手为自然语言数学证明生成步骤级正确性标签，全程无需人工标注。
- 做法：让一个模型同时写出自然语言证明与配对的 Lean 形式化证明，由 Lean 判定每一步正误，再用第二个模型过滤掉仅因形式语法导致的失败，使负标签真正对应数学错误。
- 规模：含 10,634 条证明、152K 个已标注步骤的数据集，外加 200 条证明的评测集 LeanPRM-Bench。
- 效果：基于 Qwen3-4B 训练的验证器在 LeanPRM-Bench 上步骤标注准确率从 48.2 提升到 74.7，而用人工标注的 PRM800K 训练仅得 60.3；在 IMO 级难题的 best-of-N 选择上也优于 PRM800K 验证器（4 项任务中 3 项胜出）。
- 动机：作者希望将 Lean 与「形式到非形式泛化」作为未来监督超人类模型的方案之一，解决逐步校验长证明的瓶颈。
所属事件:LeanPRM：用 Lean 合成数据训练数学证明验证器(3 条相关)→
「研究」频道最新
- Meta 实时数字人技术细节曝光:蒸馏 60 倍加速实现实时无限视频生成 — altryne · 2026-11-07
- 《生成式 AI 数学基础小书》免费覆盖 VAE、扩散、GAN 到能量模型 — kalyan_kpl · 2026-11-07
- Kenneth Stanley 谈 AGI 必需的开放性：给它设计 benchmark 本身是难题 — GregKamradt · 2026-11-07
- GLASS 方法预告:用图聚类与 LLM 无需人工编码即可给开放式回答打分 — GolinoHudson · 2026-11-07
- 实测 LLM 直改权重：改得动但留不住,20 步微调即抹除 — kevinpl07 · 2026-11-07
- FlexiTac 触觉传感器入选 CoRL 2026,发布 AI 辅助设计工具 FlexiTac-Gen — Haoyu_Xiong_ · 2026-11-07