OpenAI本周发布了数百个自称解决世界上最难数学问题的方案。该前沿实验室表示，自己曾咨询一个由顶尖数学家组成的顾问小组，以避免上一次其模型解决一个长期悬而未决的数学问题时引发的争议。

但OpenAI并未达到这些标准，尤其是在数学家强调需要人类理解数学结果的部分。这一点在一篇新论文发表后显得更令人担忧。该论文指出，OpenAI模型据称解决的一个价值100万美元的问题，其自然语言表述与正式表达之间存在差距。

数学与人工智能咨询组（Advisory Group on Mathematics and Artificial Intelligence，简称AGMAI）由普林斯顿大学高等研究院主办，成员包括来自全球各机构的9位知名研究人员。

该组织在9月底发布了面向前沿实验室解决数学问题的指导原则。AGMAI在针对最新一批证明的声明中表示：“最终，是否成功遵循了我们的建议，仍需由数学界来评估。”

不过，该组织的首要请求是“停止在专有模型上测试高级数学问题”。而OpenAI的发布明确写道，其正在使用数学领域的开放研究问题来评估自己的专有模型。

当TechCrunch就OpenAI最新的证明发布寻求更详细评价时，顾问组没有回应。该实验室显然遵循了其中一些原则，包括尽快发布结果，以及提供模型得出结论方式的信息。但并非全部都做到了：719篇手稿中，只有10篇附带了模型思维链的披露。

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

总体而言，OpenAI是否在发布证明时按照AGMAI原则“承担确保人类理解会随之而来的责任”，目前仍不清楚。AGMAI建议，OpenAI应帮助资助人类数学家的工作，因为这些数学家将需要让实验室的解法在任何实际意义上变得有意义。

“问题正被那些对整个领域本身毫无兴趣的AI提示词操作者自主解决；一旦他们最初的目标被‘解决’，他们就不再关心，而且他们对AI输出的理解也不足以回答问题、做报告，或以其他方式与领域中的其他人互动，”知名数学家Terence Tao在发布后于社交媒体上写道。Tao此前曾批评OpenAI的做法。

这一问题在本周发布的一篇论文中得到了体现。该论文由剑桥大学和伦敦国王学院的数学家撰写，质疑前沿实验室处理这类挑战的方式。

当AI模型解决数学问题时，它们首先会生成一段“自然语言”解释，然后再尝试将结果写入Lean。这是一种编程语言，理论上可以通过将证明编译为代码来确认其准确性。

不过，模型把自然语言证明翻译成代码的方式可能存在问题；这篇论文记录了OpenAI就一个源自纳维-斯托克斯方程的问题所提供解法中，自然语言证明与Lean代码之间至少两处不一致。纳维-斯托克斯方程用于描述流体的复杂行为。

这些不一致并不一定能否定任一版本的解法，但它们确实引发了疑问：我们是否可以在没有人类参与的情况下，仅仅依赖模型自行形式化其解答。这也是AGMAI要求OpenAI“加入可机器读取的元数据，以对应自然语言和形式化产物”的原因之一，但该前沿实验室在这些发布中并未这样做。

“由于存在误译现象——正如这篇论文所强调的——OpenAI以及其他自动形式化的Lean证明，在没有与其他证明同样的同行评审流程和审视之前，原则上不应被信任，”《迷失在翻译中》这篇论文的作者总结道。

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

哈佛大学数学教授Melanie Wood告诉TechCrunch，当模型被提示去解决一个难题并吐出一个解答时，“在发布时并不存在人类理解，而现在工作才刚刚开始”。