OpenAI 数百份数学证明被指未达学界标准

本周，OpenAI 发布了数百个据称针对一些世界上最难数学问题的解答。这家前沿实验室表示，它已就避免其模型上一次解决该领域一个长期悬而未决的问题时所引发的争议咨询过一个由顶尖数学家组成的顾问小组。

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

由普林斯顿大学高等研究院主办的数学与人工智能顾问小组（Advisory Group on Mathematics and Artificial Intelligence）由来自世界各地九所知名研究机构的杰出学者组成。

该组织于九月底发布了供前沿实验室解决数学问题遵循的指导原则。在一份关于最新一组证明的声明中，AGMAI 表示："我们的建议在多大程度上得到成功落实，最终要由数学界来评估。"

然而，该组织的首要请求是"停止在专有模型上测试高难度数学问题"。而 OpenAI 的发布材料明确写道，它正在利用开放的数学研究问题评估其专有模型。

当 TechCrunch 请其对 OpenAI 最新的证明发布做出更全面的评估时，该顾问小组未作回应。该实验室显然遵循了其部分原则，包括尽快发布结果，以及提供模型得出结论的推理过程信息——但并非所有原则都得到了执行：在 719 篇稿件中，只有 10 篇公开了模型的思维链。

对于人们难以读懂的论文，数学家们建议应将证明形式化——但 OpenAI 发布的证明中，仅有 42% 经过了这一过程。

归根结底，目前仍不清楚 OpenAI 是否在按 AGMAI 原则行事，承担"确保随后出现人类理解"的责任。AGMAI 建议 OpenAI 应当资助人类数学家的工作，因为这些数学家是真正使实验室的解答变得有意义所必需的。

曾批评过 OpenAI 这一做法的知名数学家 Terence Tao 在发布后于社交媒体上写道："问题正被那些对更广泛数学领域本身毫无兴趣的 AI 提示工程师自动解决——一旦他们的最初目标被'解决'，他们就对 AI 输出理解得不够深入，无法就相关结果回答问题、举办讲座或以其他方式与领域同行交流。"

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

当 AI 模型解答数学问题时，它们首先生成一段"自然语言"解释，然后尝试将该结果用 Lean 表达出来。Lean 是一种编程语言，理论上能通过把证明编译成代码来确认其正确性。

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

这些不一致之处未必能否定任何一方的解决方案，但它们确实提出了一个问题：我们能否在不借助人工参与的情况下，直接依赖模型来将其自身的解决方案形式化。这也是 AGMAI 要求 OpenAI "包含将自然语言与形式化构件相关联的机器可读元数据"的原因之一——而这家前沿实验室在此次发布中并未这样做。

《迷失在翻译中》一文的作者总结道："由于翻译错误现象——正如本文所强调的——OpenAI 的自然语言证明以及
其他自动形式化的 Lean 证明，在未经与其他证明相同的同行评审流程以及
严格审查之前，不应被想当然地信任，"

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

哈佛大学数学教授梅拉妮·伍德告诉 TechCrunch，当模型被要求解决一个难题并吐出一个解决方案时，"在发布时并没有人对它们形成理解，而工作才刚刚开始"。

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

蒂姆·费恩霍尔茨是一位撰写科技、金融和公共政策报道的新闻记者。他密切关注私营航天产业的崛起，是《火箭亿万富翁：埃隆·马斯克、杰夫·贝佐斯与新太空竞赛》一书的作者。此前，他曾在全球商业新闻网站 Quartz 担任高级记者超过十年，并在华盛顿特区以政治记者身份开启职业生涯。 您可以通过发送电子邮件至 [email protected]，或通过 Signal 向 tim_fernholz.21 发送加密信息，来联系或验证蒂姆的对外联络。

查看简历