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

当 OpenAI 本周发布数百个声称可解决世界上一些最难数学问题的方案时，这家前沿实验室表示，它已咨询了一个由精英数学家组成的顾问小组，以避免上次其模型解决该领域一个长期存在的问题时引发的争议。

但 OpenAI 未能达到这些标准，尤其是在数学家们强调需要对数学结果有人类理解的地方。这一点尤其令人担忧，因为一篇新论文凸显了 OpenAI 模型表面上解决的一个百万美元问题的自然语言表述与形式化表述之间的差距。

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

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

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

当 TechCrunch 要求对 OpenAI 最新发布的证明进行更全面的评估时，该顾问小组没有回应。该实验室显然遵循了其部分原则，包括尽快发布结果，并包含模型如何得出结论的信息。但并非对所有证明都是如此：719 份手稿中只有 10 份包含了模型思维链的发布。

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

最终，仍不清楚 OpenAI 在发布其证明时是否按照 AGMAI 的原则“负责确保人类理解会随之而来”。AGMAI 建议 OpenAI 应资助人类数学家的工作，这些数学家将被需要以使该实验室的解决方案在任何真正意义上具有意义。

“问题正由 AI 提示者自主解决，一旦他们的初始目标被‘解决’，他们对更广泛的领域本身毫无兴趣，并且对 AI 输出理解不足，无法就结果回答问题、发表演讲或以其他方式与该领域的其他人互动，”曾批评 OpenAI 方法的知名数学家陶哲轩在发布后于社交媒体上写道。

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

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

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

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

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

数学家们强调，当人类发现新结果时，他们会对其负责，并通过论文、演讲和研讨会与更广泛的社区互动。这一过程增进了对解决方案的理解，找到了可用于解决其他问题的策略，并使新知识能够应用于实际领域。

当模型被提示解决一个难题并给出解决方案时，“在发布时并没有人类对它们的理解，而现在工作才刚刚开始，”哈佛大学数学教授Melanie Wood告诉TechCrunch。

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

Tim Fernholz是一位撰写科技、金融和公共政策文章的记者。他密切报道了私营航天产业的崛起，并著有《火箭亿万富翁：埃隆·马斯克、杰夫·贝索斯和新太空竞赛》。此前，他曾在全球商业新闻网站Quartz担任高级记者十余年，并在华盛顿特区开始了他的政治记者生涯。 您可以通过发送电子邮件至[email protected]或通过Signal向tim_fernholz.21发送加密消息来联系Tim或核实其外联信息。

查看个人简介