OpenAI的数学解法尚未达到领域标准

本周，OpenAI 发布了其针对全球部分高难度数学难题的数百个解法。这家前沿实验室表示，为了确保此次发布不重蹈覆辙——即其模型此前解决领域内长期悬而未决的问题时曾引发争议——他们曾咨询由顶尖数学家组成的顾问团。

然而，OpenAI 并未完全达到这些标准，尤其是在数学家们强调人类必须理解数学结论这一问题上。考虑到新近发表的一篇论文指出，OpenAI 的模型表面上已解决的一个百万美元级难题，其自然语言解法与形式化表达之间仍存在巨大差距，这一点尤为令人担忧。

由普林斯顿大学高等研究院提供的“数学与人工智能顾问组”（AGMAI）由来自全球各机构的九位知名研究人员组成。

该组织在九月底发布了针对前沿实验室解决数学问题的准则。针对最新这批证明，AGMAI 发表声明称：“我们的建议被遵循的程度，最终需由数学界来评估。”

不过，该组织的首要建议是“停止在专有模型上测试高级数学问题”。而 OpenAI 的发布内容明确说明，其正在使用数学领域的公开研究难题来评估其专有模型。

当 TechCrunch 要求顾问组对 OpenAI 最新发布的证明进行更全面的评估时，对方未予回应。实验室显然遵循了部分原则，例如尽可能快地发布结果，并包含模型如何得出结论的相关信息。但并非所有原则都得到了贯彻：在 719 份手稿中，仅有 10 份公开了模型的思维链。

针对那些人们无法理解的内容，数学家们建议对证明进行形式化——但 OpenAI 发布的证明中，仅有 42% 经历了这一过程。

归根结底，OpenAI 在发布证明时，是否真的按照 AGMAI 原则承担了“确保人类理解随之跟上”的责任，仍然是个未知数。AGMAI 曾建议 OpenAI 资助人类数学家的工作——毕竟，要让这些解法真正有意义，离不开人类的参与。

一直批评 OpenAI 做法的知名数学家陶哲轩在成果发布后在社交媒体上写道：现在问题是“由 AI 提示词工程师自主解决的，这些人对更广泛的数学领域本身并无兴趣，一旦最初目标被‘解决’就撒手不管，而且对 AI 输出的理解不足以回答相关提问、做报告，或与学界其他人展开交流”。

本周，剑桥大学和伦敦国王学院的数学家们发布的一篇论文，正是对前沿实验室这种做法的质疑，也集中体现了这个问题。

AI 模型解数学题时，会先生成一个“自然语言”解释，再尝试用 Lean 把结果表达出来。Lean 是一种编程语言，理论上可以通过把证明编译成代码来验证其正确性。

但模型把自然语言证明转成代码的过程可能出问题。这篇论文记录了至少两处不一致：在 OpenAI 提交的一个源自 Navier-Stokes 方程（描述流体复杂行为）的题目解法中，自然语言证明与背后的 Lean 代码存在出入。

这些不一致未必能推翻任何一方的解法，但确实引出了一个疑问：我们能否在没有人参与的情况下，直接依赖模型把自己的解法形式化？这也是 AGMAI 要求 OpenAI“提供关联自然语言与形式化产物的机器可读元数据”的原因之一，而 OpenAI 在这两次发布中并没有做到。

这篇“翻译中迷失”论文的作者总结道：“正因为存在误译现象——正如这篇论文所指出的——OpenAI 的自然语言证明以及其他自动形式化的 Lean 证明，在原则上不应未经同行评审和 scrutiny 就直接采信，其他证明都要经过这样的流程。”

数学家强调，当新成果由人类发现时，他们会对其负全责，并通过论文、讲座和研讨会等形式与更广泛的学术社区互动。这一过程深化了对解决方案的理解，能够发掘出可迁移到其他问题中的解题策略，并促进新知识在实际领域的应用。 当模型被提示去解决一个难题并输出一份答案时，“在发布之初，人类对它们尚不透彻理解，而现在才是工作的开始，”哈佛大学的数学教授 Melanie Wood 对 TechCrunch 说道。