OpenAI 10 月 6 日在 GitHub 公开一批由内部未发布模型产出的数学手稿,隔天撤回其中 3 篇。根据该项目的更新记录,原因是一篇论文出现正负号错误,导致一项关键论证失效,另外两篇以同一构造为基础的论文也随之撤回。
一处符号错误连带影响 3 篇论文
出错论文为《Algebraicity of Weil classes on split abelian eightfolds》。OpenAI 说明,这篇论文中的正负号错误让一个关于稳定化与迹相消的论证失效,而另外两篇论文都使用了同一构造。
一并撤回的另外两篇分别是《Algebraicity of Kuga–Satake Correspondences for K3 Surfaces》与《The rational Hodge conjecture for products of K3 surfaces》,后者讨论的是 K3 曲面乘积的有理霍奇猜想。被撤回的论文页面目前均附有说明缺口的公告,并链接到封存版本。
同日修订 14 篇手稿,新增 6 个 Lean 证明
同一天,OpenAI 还修订了另外 14 篇手稿,调整内容包括修补证明、更正命题、澄清假设与相互依赖关系,并同步更新 13 篇论文引用的版本。
项目当天还新增 6 个 Lean 形式化证明。Lean 是一种可让计算机逐步检查证明是否正确的程序语言。目前 719 篇手稿中,已有 300 篇的主要结果完成形式化,约为 42%。
OpenAI 研究员 Dan Roberts 在 X 上表示,后续还会继续新增形式化证明,并更新新发现的勘误。
约 4,000 道题目筛出 719 篇手稿
根据项目说明,这批手稿来自 OpenAI 使用开放研究问题评估内部模型的结果。OpenAI 表示,之所以这样做,是因为模型在既有数学评测上的表现已经饱和。
项目说明称,绝大多数结果由同一套流程产出,每个结果平均使用 3 小时的 ChatGPT Pro 思考运算。评估期间,模型总共处理约 4,000 道题目,随后按重要性整理成目前的 372 个系列、719 篇手稿。
OpenAI 也在说明中承认,并非所有结果都有 Lean 证明,「部分未形式化的结果可能有问题」。
数学界发声批评发布方式
这批手稿公开后也引发数学界反弹。人类数学协会于 10 月 7 日发表声明,随后由菲尔兹奖得主陶哲轩以客座文章形式转载到个人博客。
这份声明由该协会的通讯工作小组署名。声明指出,数学家并没有要求进行这项发布,并批评 OpenAI 称其从「数学与人工智能咨询小组」获得正当性的说法,因为该小组在首份声明开头就表示,前沿 AI 公司不应该用内部模型测试高等数学难题。
声明写道:「我们拒绝 OpenAI 所称此次发布推动了这门学科的说法,并呼吁数学家与大众以应有的怀疑看待这种发表模式。」声明还称:「一次发布超过 700 份档案不是在展现学术,而是在展现权力。」并呼吁数学家停止与 OpenAI 合作。
陶哲轩在文章开头注明,这是一篇来自该协会的客座文章。部分留言者也提醒,不应将协会立场直接视为陶哲轩个人观点。

