FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models
本文介绍了 FormalRewardBench，这是首个利用 250 对专家精心策划的偏好数据来评估形式化定理证明中奖励模型的基准，结果表明前沿大语言模型在证明质量评估方面优于专用定理证明器，并凸显了当前模型在区分正确证明与各种注入错误方面的局限性。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你正在教一个机器人解决数学问题。为了让机器人学会，你需要告诉它何时正确、何时错误。
长期以来，教导这些机器人（称为“神经定理证明器”）的标准方法是一个简单的交通灯系统：
- 绿灯：证明完美无缺。
- 红灯：证明错误。
这种方法行之有效，因为“交通灯”实际上是一个能以 100% 准确率检查数学的计算机程序。但存在一个大问题：它过于稀疏。如果机器人解决了难题的 99%，却在最后犯了一个极小的错误，它就会得到红灯。它之前做对的 99% 得不到任何肯定。这就像学生因为漏掉了一道题而在考试中得了"F"，其余部分的工作却得不到任何反馈。机器人会感到困惑，不知道如何改进。
为了解决这个问题，研究人员希望教会机器人一个奖励模型。你可以将其想象为一位类人教师，能够审视证明并指出：“这里做得很好，但那里出错了”，并给出 0 到 100 的分数，而不仅仅是通过或失败。
问题所在：你如何知道你的“类人教师”（即奖励模型）是否真的擅长评分？
通常，要测试一位教师，你必须将其放入课堂，观察他们教学数周，看学生是否进步。这既昂贵又缓慢。
解决方案：FormalRewardBench
本文的作者为这些“教师”机器人构建了一个标准化的评分考试。他们将其称为FormalRewardBench。
以下是他们构建该考试的方式：
- 资料来源：他们选取了 250 道真实的难题（来自国际数学奥林匹克竞赛等），并将其翻译成一种严格的计算机语言，即Lean 4。
- 陷阱：对于每一个正确的证明，他们利用超级智能 AI 生成了五种不同类型的虚假、错误证明。这些不仅仅是明显的拼写错误，而是旨在愚弄机器人的巧妙陷阱。
- “外科手术式打击”：仅更改一个微小的字母或数字，从而破坏逻辑。
- “巧言令色者”：添加冗长且听起来自信的解释，看似正确实则错误。
- “冒牌货”：用 Python 代码（对计算机有效）而非所需的数学语言（Lean）来编写解决方案。
- “困惑的学生”：使用正确的工具，但将其应用于错误的假设。
- “冗长的胡言乱语”：编写一个极其冗长复杂但根本存在缺陷的证明。
测试过程：
他们让各种 AI 模型查看一对证明（一个真实，一个虚假），并选出正确的那一个。他们测试了四种类型的“评判者”：
- 超级天才（前沿大语言模型）：庞大、通用的 AI 模型（如 Claude Opus 或 GPT-5）。
- 专业评分员（评判大语言模型）：专门训练用于挑选更佳答案的模型。
- 数学天才（通用大语言模型）：在数学和代码方面接受过大量训练的模型。
- 证明专家（定理证明器）：专门构建用于生成数学证明的模型。
令人震惊的结果：
论文发现了一个令人惊讶的反转：
- 专家失败了：最擅长撰写证明的模型（证明专家）实际上在评分证明方面表现最差。它们的得分约为 24%（仅略高于随机猜测）。事实证明，知道如何建造房屋并不意味着你知道如何检查其裂缝。
- 通才获胜：“超级天才”（通用 AI 模型）在识破虚假证明方面表现最佳，得分接近 60%。
- “巧言令色者”陷阱：许多模型很容易被“冗长的胡言乱语”或“巧言令色者”类型的证明所迷惑。即使数学是错误的，它们也偏爱冗长的解释。
核心结论：
论文得出结论：擅长创建证明并不自动意味着擅长评估证明。为了构建能够更好地帮助数学家的 AI，我们需要专门训练模型成为“批评者”或“评判者”，而不仅仅是“创造者”。
作者将此考试（FormalRewardBench）公开发布，以便其他研究人员可以测试他们自己的“教师”机器人，看看它们是否真的在识破错误方面有所进步。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。