OpenAI 称一款秘密 AI 模型仅凭一条提示词就攻克了数百道公开数学难题——数学家们要求拿出证据

OpenAI 于周二在 GitHub 上发布了 722 篇数学手稿，全部由该公司尚未发布的内部模型生成。OpenAI 的一位发言人 表示，几乎所有内容都来自交给单个 AI 智能体的单个提示，尽管有些可能经过了多次尝试。

这是一个大胆的说法，也可能是数学领域的一个潜在重大突破。但并非所有人都对此买账，或者相信这种炒作。

“除非他们发布模型并且人们能够复现他们的结果，否则我认为任何关于用单个智能体一次性解决问题的说法都应被视为未经证实，”麻省理工学院数学家安德鲁·萨瑟兰对《科学美国人》表示。“我们应该要求出示证据，”他说。

这些论文被归入372个相关结果的“家族”，一个家族可以将一个主要定理与配套论证、推论或替代证明打包在一起。因此，722是手稿的数量，而不是已解决问题的数量。OpenAI表示，它向该模型提出了大约4000个问题，并保留了它认为足够重要、值得发表的输出。

根据OpenAI的说法，平均每个结果使用了大约相当于三小时ChatGPT Pro思考算力的资源。上个月的纳维-斯托克斯方程声明看起来则截然不同，当时有10000个协调智能体工作了88小时。

OpenAI发布了其中10个结果的精简推理摘要。尽管如此，根据该代码库中的形式化目录，722篇论文中只有162篇附有经过计算机检查的主要结果。这约占整个集合的22%，它们被翻译成Lean——一种机械地检查每一步逻辑的软件。

OpenAI 自己表示，并非所有手稿都有 Lean 形式化，并且“一些未形式化的结果可能存在问题”。换句话说，他们发表的很多内容可能是错误的。

通过 Lean 检查只能确认证明是从 Lean 中写出的陈述推导出来的。它并不能表明该陈述与原始问题相符，也不能表明结果是新的或重要的，而这正是数学家现在必须判断的部分。

而这正是研究人员感到惊讶的地方。

“现在的情况是，AI 可以在没有提示它的人类能够理解、验证或对其负责的情况下，输出数学论证，”新泽西州普林斯顿高等研究院在一份声明中表示。“我们认为，人类对数学的理解仍然至关重要。在这个新时代，我们如何努力实现一种新范式，将人类对数学的理解作为负责任学术产出的一部分？”

不过，其他人，比如 Abhishek Saha 教授，则相当兴奋。“这对数学来说是非常重要的一天，”他写道，但指出大多数问题属于“现有项目中的非凡进展”或“令人惊讶的突破”类别。

这意味着该集合中的大多数问题都很有趣，但并非像千禧年问题那样不可能或具有颠覆性。那个位置只留给 722 个问题中的一个：准黎曼猜想。

此次发布也未达到高等研究院一个咨询小组在9月29日所建议的标准：即每个结果的模型名称、提示词、思维链摘要、所用时间以及计算成本。OpenAI公布了平均计算数据和10份推理摘要，但没有公布提示词，并表示仍在努力以负责任的方式发布该模型。

多伦多大学数学家Daniel Litt持相反观点，认为没有理由要求该公司对这些数学问题的答案保密。

Anthropic上个月在其经Lean检验的费马大定理证明上采取了不同做法，将全部1300万行内容公开发布在GitHub上。该证明形式化了Andrew Wiles于1995年发表的定理，而非声称取得了新结果。

OpenAI表示，随着获得Lean形式化，将逐步添加；目前，722份手稿中有162份具备Lean形式化。