当OpenAI 发布 数百项据称解决了世界一些最难数学问题的方案,该前沿实验室表示,它已咨询了一个由精英数学家组成的顾问小组,以避免 这场争议 这与上一次其一个模型解决该领域长期悬而未决的问题时所引发的关注相提并论。
但OpenAI未能达到这些标准,尤其是在数学家强调需要对数学结果有人的理解这一点上。一篇新论文强调了OpenAI的模型表面上解决的一个百万美元问题在自然语言解法与形式化表达的解法之间的差距,这尤其令人担忧。
由普林斯顿大学高等研究院主办的数学与人工智能咨询小组由来自世界各地机构的九位知名研究人员组成。
该组织发布了 指南 针对9月底在解决数学难题的前沿实验室。AGMAI在关于最新一批证明的声明中表示:“我们的建议在多大程度上得到了成功遵循,最终由数学界来评估。”
然而,该组织的第一个请求是“停止在专有模型上测试高级数学问题”。OpenAI的发布内容明确表示,它正在使用数学领域的开放研究问题来评估其专有模型。
当TechCrunch要求该咨询小组对OpenAI最新的证明发布进行更全面的评估时,小组没有作出回应。该实验室显然遵守了其中一些原则,包括尽快发布结果,以及提供模型如何得出结论的相关信息。但并非所有原则都得到遵守:在719篇论文中,仅有十篇发布了模型的思维链。
对于人们无法理解的论文,数学家们建议应对证明进行形式化——但 OpenAI 发布的证明中仅有 42% 尚未经过这一流程。
归根结底,仍然不清楚 OpenAI 在发布其证明时,是否按照 AGMAI 原则承担了“确保人类理解能够跟上”的责任。AGMAI 建议 OpenAI 应帮助资助人类数学家的工作,而这些数学家对于使该实验室的解决方案在任何实际意义上变得有意义是必不可少的。
“问题正被AI提示词工程师自主解决,他们一旦‘解决’了最初目标就对更广泛的领域本身失去兴趣,并且对AI输出的理解不足以就结果回答问题、做报告或以其他方式与领域内的其他人交流,”曾批评OpenAI方法的知名数学家陶哲轩说。 写道 发布后在社交媒体上。
那个问题的一个例证是 一篇论文 由剑桥大学和伦敦国王学院的数学家本周发布,质疑前沿实验室应对这些挑战的方式。
当 AI 模型解答数学问题时,它们首先会用“自然语言”写出一个解释,然后再尝试用 Lean 来表达该结果——Lean 是一种编程语言,理论上可以通过将证明编译为代码来确认其正确性。
然而,模型将自然语言证明转化为代码的方式可能存在问题;本文记录了OpenAI针对一道源自描述流体复杂行为的Navier-Stokes方程的问题所提供的解答中,自然语言证明与Lean代码之间至少存在的两处不一致。
这些差异并不一定推翻其中任何一个解决方案,但它们确实提出了一个问题:我们是否可以在没有人工参与的情况下,仅仅依赖模型来将其自身的解决方案形式化。这正是AGMAI要求OpenAI“包含将自然语言与形式化产物关联起来的机器可读元数据”的原因之一,而这家前沿实验室在这些发布中并未做到这一点。
“由于误译现象——正如本文所强调的——OpenAI 和的 NL 证明以及
其他经自动形式化的 Lean 证明在未经同样的同行评审流程之前,不应被默认信任,并且
“‘迷失于翻译’一文的作者总结道:‘……其他证明所受到的审查。’”
数学家们强调,当人类发现新成果时,他们会对这些成果负责,并通过论文、演讲和研讨会与更广泛的社区进行交流。这一过程加深了对解的理解,找到了可用于解决其他问题的策略,并使新知识得以应用于实际领域。
哈佛大学数学教授Melanie Wood告诉TechCrunch,当一个模型在被提示解决一个难题后输出一个解决方案时,“在发布之时并没有人类对这些解答的理解,而现在工作才刚刚开始。”
