HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs
该论文介绍了 Hermes，一种新型工具辅助智能体，它通过将非形式化推理与 Lean 中的形式化验证证明交织在一起，使大语言模型在数学推理方面比现有方法更准确、更高效且更具可验证性。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下你正在尝试解决一个非常困难的数学谜题。你有一位才华横溢但有点丢三落四的助手（即大语言模型，或 LLM），他擅长头脑风暴和撰写长篇且富有创造性的解释。然而，这位助手有时会犯一些小的逻辑错误，或者产生一些听起来很有道理但并不真实的“幻觉”。
另一方面，你有一位严厉、不屈不挠的数学法官（一个名为 Lean 的形式化证明系统）。这位法官绝不会出错，但它非常刻板。它无法理解你的创意头脑风暴；它只接受结构完美、形式化的代码。如果你给它一个混乱的解释，它只会回答：“错误”。
Hermes 是一个新工具，它充当了这两者之间的翻译员和质量控制经理。它让你的创意助手可以自由发挥，但每隔几步就会停下来询问严厉的法官：“这一步确实是真的吗？”
以下是 Hermes 的工作原理，分为几个简单的部分：
1. 问题所在：“长途跋涉” vs. “严格考试”
- 旧方法（非形式化推理）： 你的助手尝试在一个长长的思维流中解决整个问题。它灵活且快速，但如果它在早期走错了路，它可能会在意识到错误之前，沿着错误的方向走很长一段路。这就像闭着眼睛开车，寄希望于不会撞墙。
- 另一种方法（形式化证明）： 你的助手从一开始就尝试编写严格的代码。它非常准确，但由于过程过于缓慢且困难，助手经常会卡住或放弃。这就像是在盖房子时，在铺设每一块砖之前，都要根据蓝图逐一检查每一块砖。
2. Hermes 的解决方案：“检查点”系统
Hermes 结合了两者的优点。它允许助手写出几步创意解释，然后暂停以运行一个“检查点”。
- 翻译员（形式化模块）： 当助手说，“因此，角度是 45 度”时，Hermes 会将这句话翻译成法官能理解的严格代码。
- 法官（证明模块）： 严厉的法官会检查该代码。
- 如果通过： 太棒了！Hermes 会将这一步保存到记忆库中，并告诉助手：“你做得很好，继续吧。”
- 如果失败： 法官会说：“不对，那是错的。” Hermes 会告诉助手：“停！你在这里犯了一个错误。回去并修正它。”
- 记忆库： 因为数学问题通常包含很长的逻辑链，Hermes 会记住所有通过检查的步骤。这确保了助手不会忘记它已经证明过的规则，从而保持整个论证的一致性。
3. 为什么它更好（结果）
论文在各种 AI 模型上，针对高难度的数学竞赛（如 AIME 和 HARDMath2）对 Hermes 进行了测试。
- 准确性： Hermes 让 AI 变得聪明得多。在最难的问题上，它将 AI 的成功率提高了高达 40%。它阻止了 AI 自信地给出错误的答案。
- 效率： 你可能会认为每一步都进行检查会很慢且昂贵。令人惊讶的是，与那些尝试生成 5 个或 10 个不同答案并从中挑选最佳答案的方法相比，Hermes 实际上更快速且廉价（就计算能力而言）。这就像是走一条经过验证的直接路径，而不是在迷宫里尝试 10 条不同的路线。
- 清晰度： 不同于其他仅说“这个答案有 80% 的概率是正确的”方法，Hermes 对特定步骤给出明确的“是”或“否”，这使得人们更容易看出答案为什么正确或错误。
核心结论
Hermes 就像是为你的创意数学助手配备了一个智能、自动化的编辑，实时检查它的工作。它并没有阻止助手进行创造性思考；它只是确保助手不会坠入悬崖。其结果是，一个不仅更准确，而且更高效、更易于信任的数学求解 AI。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。