OpenAI 发布的数学证明尚未达到数学界 AGMAI 制定的标准

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

但 OpenAI 未能达到这些标准，尤其是在数学家们强调需要对数学成果进行人类理解的方面。这尤其令人担忧，因为一篇新论文指出，在 OpenAI 模型据称解决的某个百万美元问题中，其自然语言解答与形式化表达的解答之间存在差距。

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

该组织于九月底发布了针对解决数学问题的前沿实验室的指导原则。在关于最新这批证明的声明中，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 是一位撰写科技、金融与公共政策相关内容的记者。他长期密切关注私营航天行业的崛起，并著有《Rocket Billionaires: Elon Musk, Jeff Bezos and the New Space Race》一书。他曾在全球商业新闻网站 Quartz 担任高级记者十余年，职业生涯始于华盛顿特区的政治记者。 你可以通过发送邮件至 [email protected] 联系 Tim 或核实其联系，也可以通过 Signal 向 tim_fernholz.21 发送加密消息。

查看简介