OpenAI的数学解答尚未达到数学界标准

本周，当 OpenAI 发布数百个据称针对世界上一些最难数学问题的解答时，这家前沿实验室表示，它曾咨询一个由精英数学家组成的顾问小组，以避免上一次其某个模型解决了该领域一个长期存在的问题时随之而来的争议。

但 OpenAI 未能达到这些标准，尤其是在数学家强调需要对数学结果具备人类理解之处。一篇新论文指出，一个据称已由 OpenAI 模型解决的百万美元问题，其自然语言解答与形式化表达的解答之间存在差距，此后这一点尤其令人担忧。

数学与人工智能顾问小组（AGMAI）由普林斯顿大学高等研究院主办，由世界各地机构的九位杰出研究人员组成。

该组织于9月底发布了面向解决数学问题的前沿实验室的指南。在关于最新一批证明的声明中，AGMAI 表示：“最终要由数学界来评估我们的建议在多大程度上被成功遵循。”

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

当 TechCrunch 请求对 OpenAI 最新的证明发布进行更全面的评估时，该顾问小组未予回应。这家实验室显然遵循了其中一些原则，包括尽快发布结果，以及纳入模型如何得出结论的信息。但并非所有原则都是如此：719 篇文稿中仅有 10 篇包含了模型思维链的发布。

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

归根结底，目前仍不清楚 OpenAI 在发布其证明时，是否依照 AGMAI 原则承担了“确保人类理解将随之而来”的责任。AGMAI 建议，OpenAI 应当帮助资助人类数学家的工作，而这些数学家是使该实验室的解答在任何真正意义上具有意义所必需的。

“问题正由一些 AI 提示者自主解决，一旦他们最初的目标被‘解决’，他们对更广泛的领域本身便不再感兴趣，而且他们对 AI 输出的理解也不足以回答有关该结果的问题、做报告，或以其他方式与该领域的其余部分互动，”曾批评 OpenAI 做法的著名数学家陶哲轩在发布后于社交媒体上写道。

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

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

然而，模型将其自然语言证明翻译成代码的方式可能存在问题；本文记录了至少两处差异，存在于自然语言证明与支撑 OpenAI 所给解答的 Lean 代码之间，该解答针对的是一个源自描述流体复杂行为的纳维-斯托克斯方程的问题。

这些差异并不必然否定其中任一解答，但它们确实提出了疑问：我们是否可以在没有人类参与的情况下，单纯依赖模型来形式化其自身的解答。这也是 AGMAI 要求 OpenAI“纳入可将自然语言与形式化产物关联起来的机器可读元数据”的原因之一，而这家前沿实验室在这些发布中并未这样做。

“由于误译现象——正如本文所强调的——OpenAI 的自然语言证明以及
其他自动形式化的 Lean 证明，在未经与其他证明相同的同行评审流程和
审查的情况下，不应被初步采信，”“迷失在翻译中”一文的作者总结道。

数学家强调，当新成果由人类发现时，他们会对其负责，并通过论文、演讲和研讨会与更广泛的社群交流。这一过程增进了对解答的理解，找到了可用于解决其他问题的策略，并让新知识得以应用于实际领域。

当模型被提示去解决一个难题并吐出一个解答时，“在发布之时，人类对它们尚无理解，而现在工作才开始，”哈佛大学数学教授 Melanie Wood 告诉 TechCrunch。

当您通过我们文章中的链接购买时，我们可能会赚取少量佣金。这不会影响我们的编辑独立性。

Tim Fernholz 是一位撰写科技、金融与公共政策的记者。他密切报道了私营航天产业的兴起，并著有 火箭亿万富翁：Elon Musk、Jeff Bezos 与新太空竞赛。 此前，他在全球商业新闻网站 Quartz 担任高级记者超过十年，并在华盛顿特区以政治记者的身份开始职业生涯。 您可以通过向 [email protected] 发送电子邮件，或通过 Signal 向 tim_fernholz.21 发送加密消息，来联系 Tim 或核实来自 Tim 的联络。

查看简介