当 OpenAI 发布本周声称解决世界上最难数学问题的数百个方案时，这家前沿实验室表示已咨询由精英数学家组成的顾问小组，以避免重蹈此前模型解决该领域长期问题所引发争议的覆辙。
但 OpenAI 未能完全达到这些标准，尤其是在数学家强调“需对数学结果有人类理解”这一点上。一篇新论文突显出自然语言表述与 OpenAI 模型声称解决的百万美元级问题形式化解决方案之间的差距，这尤其令人担忧。
AGMAI 指南与 OpenAI 的执行差距
由高等研究院主办的“数学与人工智能咨询小组”（AGMAI）由来自全球各机构的九位知名研究人员组成。该组织于9月底发布了供前沿实验室参考的指南，并在关于最新一批证明的声明中表示：“最终由数学界来评估我们的建议是否被成功遵循。”
然而，该组织的首要请求是“停止在专有模型上测试高级数学问题”，而 OpenAI 的发布内容明确指出其正在使用数学领域的开放研究问题来评估专有模型。
当 TechCrunch 要求 AGMAI 对 OpenAI 最新的证明发布进行更全面评估时，该顾问小组未予回应。尽管该实验室遵循了部分原则（如尽快公布结果、提供模型推理信息），但并非所有原则都得到落实：在包含的719份手稿中，仅有10份公布了模型的思维链；对于人们无法理解的论文，数学家建议应对证明进行形式化处理，但在 OpenAI 发布的证明中，仅有42%经过了这一过程。
归根结底，目前尚不清楚 OpenAI 是否在发布证明时按照 AGMAI 的原则“承担起确保人类理解随之跟进的责任”。AGMAI 建议 OpenAI 应资助那些将使实验室解决方案在实际意义上变得有意义的人类数学家的工作。
著名数学家陶哲轩曾批评 OpenAI 的做法，他指出：“问题正由 AI 提示者自主解决，一旦他们的初始目标被‘解决’，他们对更广泛的领域本身便不再感兴趣，并且他们并不足够理解 AI 的输出以回答关于结果的问题、发表演讲或与其他领域成员互动。”
自然语言与代码形式的“翻译”风险
这一问题在本周由剑桥大学和伦敦国王学院数学家发布的一篇论文中得到了例证，该文质疑了前沿实验室应对这些挑战的方式。
当 AI 模型解决数学问题时，通常先创建“自然语言”解释，再尝试用 Lean（一种编程语言）表达该结果，理论上通过编译为代码来确认证明准确性。然而，模型将自然语言证明转换为代码的方式可能存在缺陷。这篇论文记录了 OpenAI 针对源自描述流体复杂行为的纳维-斯托克斯方程问题所提供的解决方案中，自然语言证明与背后的 Lean 代码之间至少存在两处差异。
这些差异虽不一定否定任何一种解决方案，但引发了疑问：我们是否真的可以仅仅依赖模型在没有人类参与的情况下形式化其自身的解决方案？这也是 AGMAI 要求 OpenAI “包含将自然语言和形式化工件相关联的可机器读取元数据”的原因之一，而这家前沿实验室在这些发布中并未做到这一点。
《迷失在翻译中》论文的作者得出结论：“由于误译现象——正如本文所强调的那样——OpenAI 的自然语言证明以及其他自动形式化的 Lean 证明，不应在未经历与其他证明相同的同行评审过程和审查的情况下被初步信任。”
人类理解仍是数学验证的核心
数学家们强调，当新成果由人类发现时，他们会对此负责，并通过论文、演讲和研讨会与更广泛的社区互动。这一过程不仅增加了对解决方案的理解，还能找到可用于解决其他问题的策略，并允许将新知识应用于实际领域。
哈佛大学数学教授梅兰妮·伍德告诉 TechCrunch：“当一个模型被提示去解决一个难题并吐出一个解决方案时，在发布时并没有人类对它们的理解，而现在工作才刚刚开始。”
更正：本文最初错误报道了高等研究院与普林斯顿大学的关系。IAS 与该大学没有隶属关系。