当 OpenAI发布本周发布了数百个针对世界上一些最难的数学问题的所谓解决方案时，这家前沿实验室表示，它已咨询了一个由顶尖数学家组成的顾问小组，以避免争议上一次其模型解决了该领域一个长期存在的问题时所引发的争议。
但 OpenAI 未能达到这些标准，尤其是在数学家们强调需要对数学结果有人类理解的地方。这一点尤其令人担忧，因为一篇新论文凸显了 OpenAI 模型表面上解决的一个百万美元问题的自然语言表述与形式化表述之间的差距。
数学与人工智能顾问小组（AGMAI）由普林斯顿大学高等研究院主办，由来自世界各地机构的九位知名研究人员组成。
该组织发布了指导方针于九月底针对解决数学问题的前沿实验室。在关于最新一批证明的声明中，AGMAI 表示“最终要由数学界来评估我们的建议在多大程度上得到了成功遵循。”
然而，该组织的第一个要求是“停止在专有模型上测试高等数学问题”。OpenAI 的发布明确表示，它正在使用数学中的开放研究问题来评估其专有模型。
当 TechCrunch 要求对 OpenAI 最新发布的证明进行更彻底的评估时，该顾问小组没有回应。该实验室显然遵循了其部分原则，包括尽快发布结果，并包含有关模型如何得出结论的信息。但并非所有原则都遵循了：719 份手稿中只有 10 份包含了模型思维链的发布。
对于人们不理解的论文，数学家们建议应将证明形式化——但 OpenAI 发布的证明中只有 42% 没有经过这一过程。
最终，OpenAI 在发布其证明时，是否按照 AGMAI 原则“承担起确保人类理解能够跟进的责任”，仍不清楚。AGMAI 建议 OpenAI 应资助人类数学家的工作，这些数学家将需要以任何真正有意义的方式让该实验室的解决方案变得可理解。
“问题正由 AI 提示者自主解决，而这些人一旦最初的目标被‘解决’，就对更广泛的领域本身毫无兴趣，并且对 AI 输出的理解不足以回答关于结果的问题、做报告，或以其他方式与该领域的其他部分互动，”Terence Tao，一位批评 OpenAI 做法的著名数学家，写道在发布后在社交媒体上。
这个问题的一个例证是一篇论文本周由剑桥大学和伦敦国王学院的数学家发布，质疑前沿实验室应对这些挑战的方式。
当 AI 模型解决数学问题时，它们首先创建“自然语言”解释，然后尝试用 Lean 表达该结果，Lean 是一种编程语言，理论上通过将证明编译为代码来确认其准确性。
然而，模型将其自然语言证明翻译为代码的方式可能存在问题；这篇论文记录了至少两处不一致，分别存在于自然语言证明与 OpenAI 针对一个源自 Navier-Stokes 方程的问题所提供的解决方案背后的 Lean 代码之间，该方程描述流体的复杂行为。
这些不一致不一定能否定任一解决方案，但它们确实提出了一个问题：我们是否可以简单地依赖模型在无人参与的情况下将自己的解决方案形式化。这是 AGMAI 要求 OpenAI“包含将自然语言与形式化产物关联起来的机器可读元数据”的原因之一，而该前沿实验室在这些发布中并未这样做。
“由于误译现象——正如这篇论文所强调的——OpenAI 的自然语言证明以及
其他自动形式化的 Lean 证明不应在未经同样同行评审过程的情况下被初步信任，并且
“其他证明所受到的审查，”《迷失在翻译中》一文的作者总结道。
数学家们强调，当新结果由人类发现时，他们会对其负责，并通过论文、演讲和研讨会与更广泛的社群交流。这一过程增进了对解法的理解，找到了可用于解决其他问题的策略，并使新知识能够应用于实际领域。
当模型被提示去解决一个难题并给出一个解法时，“在发布的那一刻，并没有人类对它们的理解，而现在工作才刚开始，”哈佛大学数学教授 Melanie Wood 对 TechCrunch 表示。
当您通过我们文章中的链接购买时，我们可能会赚取一小笔佣金。这不会影响我们编辑的独立性。
Tim Fernholz 是一名记者，撰写有关技术、金融和公共政策的文章。他密切报道了私营航天产业的崛起，并著有《火箭亿万富翁：Elon Musk、Jeff Bezos 与新太空竞赛》。此前，他曾在全球商业新闻网站 Quartz 担任高级记者十余年，职业生涯始于华盛顿特区的政治记者。 您可以通过发送电子邮件至以下地址联系 Tim 或核实其外联信息[email protected]或通过 Signal 向 tim_fernholz.21 发送加密消息。