o1/Claude集体翻车！陶哲轩等60+顶尖数学家合力提出新数学基准 - 通信人家园

大模型们，至少需要再战个几年吧。

之所以引入这个基准，是因为大模型越来越多地碾压现有的数学基准

通常需要专业数学家花费数小时甚至数天的努力

如果模型在达到标记限制之前没有提交最终答案，它将收到一个最终提示，要求立即提交最终答案；
如果在收到该提示后模型仍然无法提供正确格式化的最终答案，则该尝试被标记为不正确。

之所以引入这个基准，是因为大模型越来越多地碾压现有的数学基准。有趣的问题是，尽管从许多方面（/evals）来看，大模型正逐步跻身顶级专家行列（如数学和编码等），但你不会雇用他们而不是让他们从事最琐碎的工作
如果你把问题描述整齐地放在盘子里，他们就能解决复杂的封闭式问题，但他们很难连贯地把长长的、自主的、解决问题的序列串联起来，而人却会觉得非常容易。
这是莫拉维克悖论的变相，他在30多年前就观察到，对人类来说容易/困难的事情，与对计算机来说容易/困难的事情，在非直觉上可能大相径庭。
例如，人类对计算机下国际象棋印象深刻，但国际象棋对计算机来说却很容易，因为它是一个封闭的、确定性的系统，具有离散的行动空间、完全的可观测性等等。
反之亦然，人类可以系好鞋带或叠好衬衫，而且根本不需要考虑太多，但这是一项极其复杂的传感运动任务，对硬件和软件的技术水平都是挑战。
这就像不久前OpenAI发布的魔方一样，大多数人都把注意力集中在解魔方本身（这是微不足道的），而不是用机器人的手转动魔方的一个面这一实际难度极高的任务。
因此，我非常喜欢这个FrontierMath基准，我们应该制作更多的基准。但我也认为，如何为所有 “容易 “但其实很难的东西创建评估是一个有趣的挑战。
很长的语境窗口、连贯性、自主性、常识、有效的多模态输入/输出…… 我们如何建立良好的 “初级工作 “评估？就像你对团队中任何初级实习生的期望。

陶哲轩梦想的就是这样的东西，可以连接到LEAN（微软研究院推出的一款定理证明器），让数学家成为编辑、顾问，偶尔处理一些真正困难的部分，而其余部分则自动化且可证明正确。
很难说一个在这次基准测试中能够达到80%的LLM对数学家来说没有用处。