我们正在发布由内部前沿模型产生的一系列新数学结果。为改进与数学界分享结果的方式,我们一直咨询位于高等研究院(Institute for Advanced Study)的独立数学与人工智能顾问组(Advisory Group on Mathematics and Artificial Intelligence)以制定最佳实践,并参考其建议与公开推荐来指导本次发布。此次结果发布于GitHub(GitHub)仓库,附论文修订与引用协议,同时分享许多证明在Lean(Lean)编程语言中的形式化,并将持续更新。
正文
我们正在发布由一个内部前沿模型产生的大量新数学成果。
为改进与数学界分享成果的方式,我们咨询了独立的高等研究院数学与人工智能顾问组以制定最佳实践,并参考其建议与公开推荐来指导本次发布。
本次发布将结果公布在 GitHub 仓库中,附上论文修订与引用规范。我们仍在探索其他符合委员会准则的社区托管方案,未来则承诺通过引用、数学阐述和结果呈现来进一步提升论文质量,便于理解。
作为仓库的一部分,我们用 Lean(一种可让计算机校验数学证明的编程语言)形式化了多处证明,并将持续更新。
为促进透明开放,我们还在仓库中公开了取得成果的更多细节,包括 10 份模型推理摘要、以 ChatGPT Pro 使用量估算的算力消耗,以及尝试问题数量的统计。平均每个结果约消耗相当于 ChatGPT Pro 思考三小时的算力。
我们希望这一进展推动人类知识前沿,促成数学进一步突破,并将资助一系列围绕理解 AI 重大成果的研讨会、会议和特别项目,详情近期公布。
我们想让科学家直接掌握最先进能力,正负责地发布产生这些结果的模型。因此持续在数学与其他科学上评估内部前沿模型十分重要,以加速开发推动这些领域的工具。我们将继续采纳社区反馈,更新未来重大科学发现的披露标准。
评论
讨论整体是惊讶与怀疑并存:多数人对这批结果的规模和"直接放上 GitHub"表示赞赏,但分歧主轴在于它是科学开放的新范式,还是被数学界公开施压后才做出的公关止损;对结果是否经过实质人工审查,质疑声同样集中。
认为公开预印本是科学范式的转变
- 绕开收费期刊、直接放到公开仓库,被视为科学传播方式的进步(较多人) > 真高兴它发在 GitHub 而不是某个收钱的守门期刊上,这才是科学的新时代。(@binlog)
- 也有人强调,能让他们与数学界接触本身就是公共施压起了作用,尽管是被公开羞辱后才发生(较多人)
认为这是被公开羞辱后做出的公关止损
- 有人觉得如果这算主要回应,那并没有打到 OpenAI 真正该被打的地方(较多人) > 如果这就是他们的主要回应,我不觉得这一下打到了 OpenAI 该被打的地方。(@rafterydj)
- 与外部机构提出的要求放在一起看,这份发布被形容为"东西给你、要求一概不理、模型还会照常发布"(较多人)
质疑结果没有经过足够的人工审查,很可能有硬伤
- 覆盖领域过广,不可能做哪怕勉强够格的抽查,有人预测其中某个结果会出错而宣传反噬(较多人) > 这么多领域这么多结果,他们不可能做哪怕勉强够格的抽查。(@mathisfun123)
- 有人直接发问:真正研究这些问题的数学家是否审过,还是根本没人读得懂(较多人)
认为形式化证明不能替代对定理表述的检查
- Lean 只在定理被正确表述的前提下才算证明证书,而横跨这么多问题,表述正确本身就很可疑(较多人) > 有 Lean 证明的那些,也可能是定理被错误表述了。(@nautilus12)
- 也有建议:哪怕只是初步审阅,也应该把审阅过结果的人名署在论文上(少数人)
认为此前嘲笑模型缺乏创造力的人已经被打脸
- 过去很多人以"模型只会找反例、不会证明猜想"来贬低其创造力,这种说法没能撑过几个月(较多人) > 那点自我安慰没撑过三个月吧?(@yewenjie)
- 讽刺性的总结是"随机鹦鹉又一次预测出了下一个 token",代表了一种社区情绪(少数人)
看重具体结果的数学分量,尤其 Unique Games
- Unique Games 猜想是复杂性理论的奠基性猜想,大量不可近似性结果都建立在它之上,证明成立是大事(较多人) > 这个猜想是复杂性理论里的核心假设,很多不可近似性结果都依赖它。(@enoether)
- 有人列出这批成果在公开问题榜单上的排名,涉及有理数域上的 Hilbert 第十问题、Unique Games、Anderson 模型扩展态、Penrose 不等式、Landau–Siegel 零点不存在性、Baum–Connes、Hadwiger、玻色–爱因斯坦凝聚等(较多人)
- Barnette 猜想也在其中,而该评论者几个月前用当时最好的模型攻过它并失败,因此认为这一条尤其值得关注(较多人)
担心数学博士和职业数学家被直接碾过
- 读到一半的博士研究可能已被预印本写完,整条研究路线需要重做,这是最现实的冲击(较多人) > 假设我是个博士读到一半的学生,手上正好有这些预印本之一的半成品,我该怎么办?(@open592)
反对外部机构要求停止在专有模型上测试前沿数学
- 这类呼吁被解读为以保护从业者岗位为由阻挡进展,类比是"不会为了保住医生的饭碗而留着疾病"(少数人) > 如果换成疾病,我们难道也要为了保住医生的饭碗而留着疾病吗?(@aaraujo002)
好奇这些成果何时落到工程与科学应用上
- 有人是工程/生物/机器学习背景,关心其中是否有结果能立刻用上,哪怕只解决一个长期问题也好(少数人)
- 也有一条玩笑式提问:这能不能让建数据中心的数学算得通(少数人)
有价值的补充
- 仓库公开了推理轨迹,可以读到模型解题的中间过程和初始提示示例。
- 官方说明称每个结果平均消耗约等于三小时 ChatGPT Pro 的思考算力,这一点被认为相当惊人。
- 三机单位作业调度那篇给出的复杂度上界是 (L+2)^150020,指数夸张,且用的是多带图灵机这种老式计算模型;评论者说自己当天无力验证,但纯粹为了这个指数也希望它成立。
- 有人快速比对公开问题榜单,称其中 90 个被宣称完全解决,最高排位包括第 22 位的 Hilbert 第十问题(有理数域)与第 29 位的 Unique Games。
- 有评论追问参与过 Navier–Stokes 风波的研究者是否仍在 OpenAI,显示出社区对上次争议的余波仍在关注。