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

然而,OpenAI的表现未能达到这些标准,尤其是在数学家们强调需要人类对数学结果的理解方面。这一点令人担忧,尤其是在一篇新论文指出OpenAI模型声称解决的百万美元难题的自然语言解答与形式化表达之间存在差距之后。

由普林斯顿大学高等研究院主办的数学与人工智能顾问组(AGMAI)由来自全球各地的九位知名研究人员组成。

该组织于九月底发布了针对前沿实验室解决数学问题的指导原则。在最新一批证明发布的声明中,AGMAI表示“最终由数学界评估我们的建议在多大程度上被成功遵循”。

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

AGMAI未对TechCrunch关于OpenAI最新证明发布的更深入评价作出回应。显然,OpenAI遵循了部分原则,包括尽快发布结果以及提供模型得出结论的相关信息。但并非全部:在719篇手稿中,仅有10篇包含了模型的思路链条。

对于人们难以理解的论文,数学家建议应对证明进行形式化处理,但OpenAI发布的证明中有42%未经过此过程。

总体来看,尚不清楚OpenAI是否真正承担了“确保人类理解随之而来”的责任,符合AGMAI的原则。AGMAI建议OpenAI应资助人类数学家的工作,因为这些数学家将负责使实验室的解决方案在实际中具有意义。

著名数学家、曾批评OpenAI方法的陶哲轩在发布后于社交媒体上写道:“问题由对更广泛领域不感兴趣的AI提示者自动解决,一旦他们的初步目标‘解决’,便不再关注,也无法充分理解AI输出以回答结果相关问题、进行讲座或与领域其他成员互动。”

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

当AI模型解决数学问题时,首先生成“自然语言”解释,然后尝试用Lean编程语言表达该结果,理论上通过将证明编译为代码来确认其准确性。

然而,模型将自然语言证明转化为代码的方式可能存在问题;该论文记录了OpenAI针对源自描述流体复杂行为的Navier-Stokes方程问题所提供解决方案的自然语言证明与Lean代码之间至少存在两处不一致。

这些差异并不必然否定任何一方的解决方案,但确实引发了是否能仅依赖模型自行形式化解决方案而无需人类参与的疑问。这也是AGMAI要求OpenAI“包含关联自然语言与形式化文档的机器可读元数据”的原因,而OpenAI此次发布未做到这一点。

“正如本文强调的误译现象,OpenAI的自然语言证明和其他自动形式化的Lean证明不应在未经同行评审和严格审查的情况下被默认信任,”“误译”论文的作者总结道。

数学家们强调,当人类发现新结果时,会承担责任并通过论文、讲座和研讨会与更广泛的社区交流。这个过程有助于加深对解决方案的理解,发现可用于解决其他问题的策略,并使新知识得以应用于实际领域。

哈佛大学数学教授梅兰妮·伍德告诉TechCrunch:“当模型被提示解决一个难题并输出解决方案时,发布时并没有人类对其的理解,而真正的工作才刚刚开始。”