CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean
本文介绍了 CAM-Bench，这是一个新的 Lean 4 基准测试，包含 1,000 个形式化的计算数学与应用数学问题，它通过利用依赖关系恢复流程来改编教科书习题，并分析大语言模型在需要局部上下文追踪和基础定理应用的任务上的表现，从而解决了现有评估中这些领域代表性不足的问题。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你正在试图教一个聪明但字面思维僵化的机器人学习数学。你有两种方法来测试它：
- “答案密钥”测试：你给机器人一个数学问题，它写下最终数字。如果数字正确，你就给它一颗金星。这就是目前大多数 AI 数学测试的运作方式。
- “逐步”测试：你要求机器人写出每一个逻辑步骤，就像教科书中的证明一样，然后你检查每一步是否在逻辑上无懈可击。这要难得多，但它能证明机器人实际上理解了数学，而不仅仅是猜出答案。
本文介绍了一种新的、超级严格的“逐步”测试，名为CAM-Bench。
问题：机器人只懂“奥林匹克”数学
目前，大多数针对数学 AI 的测试都像是奥林匹克谜题。它们是棘手的、自成一体的谜语（例如“证明如果 X 为真，则 Y 为真”）。AI 非常擅长这些，因为它们就像孤立的逻辑游戏。
但现实世界的数学——如工程、金融或物理——则不同。它通常不是一个整洁的谜语。它更像遵循食谱书里的菜谱。
- 菜谱（问题）假设你已经知道“煸炒”是什么意思。
- 它假设你拥有特定类型的平底锅（第三章中的定义）。
- 它假设你知道如何切洋葱（第一章中的算法）。
如果你只是把菜谱的最后一句（“制作汤”）交给机器人，它会感到困惑，因为它没有原作者假设你拥有的“局部上下文”（定义、工具、之前的步骤）。
CAM-Bench 旨在测试 AI 是否能处理这种“食谱风格”的数学，特别是在优化（寻找做某事的最佳方式）、数值线性代数（对巨大的数字网格进行数学运算）和数值分析（近似求解）等领域。
解决方案：“上下文侦探”流水线
作者们并没有直接从教科书中抓取问题并喂给 AI。他们构建了一个复杂的流水线（工厂生产线）来准备问题。将其想象成一名上下文侦探：
- 原始线索：他们从一本杂乱的教科书练习开始，上面写着：“使用算法 16.4 解决练习 16.76。”
- 侦探工作：该流水线回到书中，找出“算法 16.4"实际上是什么。它挖掘出隐藏在先前章节中的定义、公式和假设。
- 重构：它将所有这些分散的片段拼接成一个大的、自成一体的“非形式化定理”。这就像把一句写着“加入秘密酱汁”的菜谱重写为“加入由番茄、罗勒和大蒜制成的酱汁”。
- 翻译：最后，它将这个干净、自成一体的故事翻译成Lean，这是一种严格的计算机语言，充当一位超级挑剔的数学老师。如果逻辑中有任何微小的漏洞，Lean 都会拒绝它。
结果：AI 被困在“食谱”中
作者们在新的基准测试上测试了一些世界上最聪明的 AI 模型。以下是发生的情况：
- “答案密钥”差距：AI 模型实际上相当擅长用纯英语解决问题（得出正确答案）。但当它们必须用 Lean（严格语言）写出证明时，其成功率暴跌。
- 类比：这就像 AI 能在对话中告诉你如何烤蛋糕，但如果你要求它为一个无法猜测任何事物的机器人编写说明，机器人会把厨房烧掉。
- “局部上下文”失败：AI 不断忘记“局部规则”。它会尝试使用当前章节中不存在的工具，或者忽略微小的假设（例如“数字必须为正”），这些假设在教科书中是隐含的，但在该特定句子中并未明确陈述。
- “长链条”问题：真实的数学问题通常需要一长串小步骤（就像一块砖一块砖地建造房屋）。AI 模型经常在链条中间迷失，忘记它们正在建造什么，或者失去对长期目标的控制。
“智能体”升级
研究人员还尝试了一种更高级的方法，让 AI 像一个带着工具箱的人类侦探那样行动。AI 不再只是猜测答案，而是被允许：
- 在犯错时向计算机（Lean）寻求帮助。
- 检查自己的工作。
- 根据错误信息再次尝试。
这种“智能体”方法效果要好得多，使成功率提高了一倍。然而，它仍远非完美，而且运行所需的“脑力”（计算机令牌）成本要高得多。
底线
CAM-Bench 表明，虽然 AI 在解决数学谜语方面越来越擅长，但它在需要理解上下文、记住局部规则并逐步构建长逻辑论证的应用数学方面仍然举步维艰。
该论文得出结论，为了使 AI 在现实世界的数学中真正可靠，我们需要停止在孤立的谜语上测试它，转而开始在这些混乱的、富含上下文的“食谱”问题上测试它。目前的模型就像那些能死记硬背答案但尚未学会如何从零开始建造房屋的学生。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。