OpenAI发布数百个数学难题解答，顾问小组：人类必须理解结果

发布前先请教了数学家

OpenAI 本周发布了数百个声称解决世界最难数学问题的方案。发布前，实验室咨询了一个由顶尖数学家组成的顾问小组，想避免上次模型解出长期未解问题时那种争议。

这个小组叫“数学与人工智能咨询小组”（AGMAI），由普林斯顿高等研究院主办，九名成员来自世界各地的研究机构。九月底，它发布了给前沿实验室用的数学问题解决指南。OpenAI 没能达到标准，最明显的是“人类必须理解数学结果”这一条。

几项请求没有落实

AGMAI 的第一条建议，是停止在专有模型上测试高级数学问题。OpenAI 的发布写明，它用数学领域的开放研究问题评估自己的专有模型。

OpenAI 确实跟进了部分建议，包括尽快发布结果，附上模型如何得出结论的信息。但有几点没有落实：719 份手稿里只有 10 份公开了模型的思维链；数学家建议，人类看不懂的文章应该把证明形式化，OpenAI 有 42% 的证明没有走这一步；AGMAI 还要求用机器可读元数据把自然语言版本和形式化版本关联起来，发布物里没有出现。

两种语言之间的缝隙

AI 解数学题，先给出自然语言解释，再用 Lean 编程语言表达结果。Lean 理论上通过编译代码来确认证明准确。

剑桥大学和伦敦国王学院的数学家本周发表论文，质疑前沿实验室处理这些题目的方式。论文记录，OpenAI 对 Navier-Stokes 方程衍生问题给出的方案里，自然语言证明和 Lean 代码至少有两处对不上。这些差异不一定推翻任何一边的结论，但带出一个真问题：没有人类参与，模型自己形式化自己的解答，还不足以被默认信任。

论文作者总结，正因为存在这种“误译”，OpenAI 和其他自动形式化的 Lean 证明，在没有经过与其他证明相同的同行评审和审查之前，不应该被默认信任。

目前还不清楚 OpenAI 会不会补齐这些材料。数百份方案停在“已经发布”的状态。

数学家的工作

陶哲轩批评道，问题由 AI 自主解决，用提示词驱动模型的人只盯着最初的目标；目标一旦“解决”，他们对更广泛的领域不再有兴趣，也不理解 AI 的输出，无法回答关于结果的问题、做报告，或以其他方式与领域内的人交流。

这与数学家习惯的节奏相反。人类做出一个结果，要通过论文、讲座和研讨会向整个社区交代来龙去脉，反复回答别人的问题。这套互动不是可有可无的程序：它让同行真正理解结论，找出可以复用的方法，也让新知识进入实际应用。AI 的输出跳过了所有这些环节。

哈佛大学数学教授 Melanie Wood 说，模型被提示解决难题并给出方案后，“在发布时没有人类理解，现在工作开始了”。

AGMAI 在针对这批证明的最新声明中说，最终要由数学界来评估建议被遵循的程度。小组没有回应 TechCrunch 对这次发布的深入评估请求。AGMAI 曾建议 OpenAI 资助人类数学家，让这些方案真正变得有意义；目前还不清楚 OpenAI 是否承担了“确保人类理解随之而来”的责任。