OpenAI 数学解题未达 AGMAI 标准：形式化证明与自然语言解存在鸿沟，缺乏人类理解验证

本周，OpenAI 发布了数百份声称已解决全球最困难数学问题的方案。这家前沿实验室表示，他们咨询了一个由精英数学家组成的顾问小组，以避免重演此前其模型解决该领域一个长期悬而未决的问题时所引发的争议。

但 OpenAI 未能达到这些标准，尤其是在数学家们强调人类必须理解数学结果这一要求方面。这一点尤其令人担忧，因为一篇新论文指出，对于 OpenAI 模型据称已解决的百万美元级难题，其自然语言表述的解决方案与形式化表达的解决方案之间存在差距。

“数学与人工智能顾问小组”（Advisory Group on Mathematics and Artificial Intelligence, AGMAI）由普林斯顿大学高等研究院主办，成员包括来自世界各地机构的九位知名研究人员。

该组织于九月底发布了针对前沿实验室解决数学问题的指南。在关于最新一批证明的声明中，AGMAI 表示：“最终，评估我们的建议是否被成功遵循，取决于数学界。”

然而，该组织的首要请求是“停止在专有模型上测试高级数学问题”。而 OpenAI 的发布明确说明，它正在使用开放性的数学研究问题来评估其专有模型。

当 TechCrunch 向该顾问小组询问对 OpenAI 最新证明发布的更详细评估时，对方未予回应。显然，OpenAI 遵循了其部分原则，包括尽快发布结果以及提供模型如何得出结论的相关信息。但并非所有原则都得到遵守：在 719 份手稿中，仅有十份包含了模型的思维链（chain of thought）发布内容。

对于人们无法理解的论文，数学家们建议应对证明进行形式化处理——但 OpenAI 发布的证明中，仍有 42% 未经过这一过程。

归根结底，目前仍不清楚 OpenAI 在发布其证明时是否真正遵循了 AGMAI 原则中关于“确保人类理解随之而来”的责任。AGMAI 建议，OpenAI 应资助那些致力于使实验室解决方案具有实际意义的人类数学家的工作。

著名数学家陶哲轩（Terence Tao）曾批评 OpenAI 的做法，他在社交媒体上写道：“问题正由 AI 提示工程师自主解决，而这些人一旦初始目标被‘解决’，便对更广泛的领域本身失去兴趣；他们对 AI 输出的理解也不够深入，无法就结果回答问题、发表演讲或与该领域的其他成员进行互动。”

本周，来自剑桥大学和伦敦国王学院的数学家们发表了一篇论文，质疑前沿实验室应对这些挑战的方式，上述问题便是例证。

当 AI 模型解决数学问题时，它们首先生成一份“自然语言”解释，然后尝试将该结果用 Lean 表达出来——Lean 是一种编程语言，理论上可通过将证明编译为代码来确认其准确性。

然而，模型将自然语言证明转化为代码的过程可能存在缺陷；这篇论文记录了至少两处差异，出现在 OpenAI 针对源自纳维-斯托克斯方程（描述流体复杂行为）的问题所提供的解决方案中，即自然语言证明与背后的 Lean 代码之间存在不一致。

这些差异并不一定否定任一解决方案的正确性，但它们确实引发了一个问题：我们能否在没有人类参与的情况下，单纯依赖模型来形式化其自身的解决方案？这也是 AGMAI 要求 OpenAI “包含关联自然语言和形式化产物的机器可读元数据”的原因之一，而该前沿实验室在这些发布中并未做到这一点。

《迷失在翻译中》（"lost in translation"）论文的作者在结论中指出：“鉴于这种误译现象——正如本文所强调的——OpenAI 的自然语言证明以及其他自动形式化的 Lean 证明，不应在未经历与其他证明相同的同行评审过程和严格审查的情况下，就被初步视为可信。”

数学家们强调，当人类发现新成果时，他们会对此负责，并通过论文、报告和研讨会与更广泛的学术社区展开交流。这一过程不仅加深了对解决方案的理解，还能提炼出可用于解决其他问题的策略，并使新知识得以应用于实际领域。

当模型被提示去解决一个难题并输出答案时，“在发布的那一刻，人类尚未真正理解这些结果，而这正是工作的开始。”哈佛大学数学教授梅拉妮·伍德（Melanie Wood）告诉 TechCrunch。