OpenAI 请外部专家核查其 AI 在数学、计算机科学与物理领域生成的证明
OpenAI asks outside experts, including a Nobel laureate, to check proofs its AI produced in math, computer science, and physics
OpenAI 称其内部模型在数学、计算机科学和物理三个领域产出证明,包括推翻计算复杂性理论中的指数时间假设(ETH)、证明局部光滑猜想在所有维度成立,以及证明四维量子场论的存在性。公司已把数学和计算机科学证明翻译成 Lean,并请外部专家担任 shepherd 独立核查,其中物理部分由 2004 年诺贝尔物理学奖得主 David Gross 领衔的团队负责。OpenAI 表示不主张科学发现署名,并承诺公开原始数据、向 Simons 基金会投入 500 万美元资助相关研讨会。
推荐理由
精选AI 评分 93
原文梳理了 OpenAI 三项 AI 生成证明的领域背景与外部核查安排,读者可据此理解争议焦点和验证难点。
主题
正文 · AI 翻译
OpenAI表示,其内部模型推翻了计算机科学中的一个核心假设,并证明了千禧年大奖难题之一的一部分,以及其他成果。外部专家现在将判定这些证明是否成立。
OpenAI在一篇博客文章中列出了来自数学、计算机科学和物理学的三项成果。该公司称,其内部AI模型产出了这些证明。OpenAI称这些手稿是一种仍待理解的原始研究数据。
因此,OpenAI请外部专家担任这些成果的“牧羊人”。根据他们的建议,公司对每个领域采取了不同的处理方式。OpenAI表示,它还将数学和计算机科学的证明翻译成了Lean。
Lean是一种编程语言,可让计算机检查证明的每一步。但这并不保证结果没有错误。Lean只检查证明是否确立了用Lean写下的那个陈述。专家仍需判定该陈述是否真正抓住了原本要解决的问题。
如果OpenAI是对的,计算机科学中的一个核心假设就是错的
计算机科学成果的核心是指数时间假设(ETH)。它涉及布尔可满足性问题,即SAT。SAT处理的是一个逻辑公式,其变量只能为真或假。问题是,你能否设定这些变量,使整个公式的结果为真。
如果只有几个变量,你可以直接尝试每一种组合。但每增加一个变量,可能性就翻倍。若有100个变量,你面对的就是一个31位数。
简而言之,ETH说的是不存在真正的捷径。你可以加快试错,但在最坏情况下,计算时间仍呈指数增长,每增加一个变量就按固定倍数增加。
OpenAI称,可满足性问题与P versus NP问题密切相关。那就是那个著名的未解问题:一个解可以被快速检验的问题,是否也能被快速求解。对于SAT,检验很容易,因为你只需代入一个候选答案并做计算。难的是找到一个可行的答案。
SAT被视为这类困难问题的教科书式例子。一种快速求解它的方法会立刻让成千上万个其他问题也能被快速求解。大多数专家认为不存在这样的方法。这一信念的简写是“P不等于NP”。
ETH比这一猜想走得更远。它说的不仅是SAT很难,还说明了它有多难。如果ETH被推翻,P仍可能不同于NP,因此困难问题不会自动变容易。
ETH此前被广泛接受为真。图论、计算生物学、数据库和计算几何领域的数百篇论文都建立在它之上。例如,它们表明,如果ETH成立,某个问题不可能在某一时间之内被求解。
现在OpenAI称其系统已证明ETH为假。如果该证明成立,那些论文就失去了基础。它们的结果不会自动变错,但将不再被证明。
OpenAI称,这一结果可能帮助研究人员找到更好的算法。不过,要将其转化为实际收益仍需大量研究。
实际回报尚不明确,但理论上的影响会很大
SAT在实践中非常重要。例如,被称为SAT求解器的专用程序会检查芯片设计中的错误并测试软件。
它们如今常常已经能处理拥有数百万变量的公式。这是因为来自现实应用的公式通常比ETH所处理的最坏情况容易得多。只加快最坏情况并不会自动帮助这些程序。
麻省理工学院教授Ryan Williams在X上表达了同样谨慎的态度。当有用户问普通开发者会最先注意到什么时,Williams说目前还没有人知道。他说,按目前的速度,实际SAT求解在12个月内取得重大进展是可能的。“或者我们可能什么也看不到。我真的不知道,”他承认道。
这一结果还会在复杂性理论本身激起涟漪,特别是电路研究,电路是由AND、OR和NOT等简单逻辑门组成的网络。Williams说,如果OpenAI的结果成立,那么可以推出某一类要求极高的问题无法用小电路求解。这里的“小”是指,当输入长度翻倍时,电路最多需要大约两倍的门数。
提出ETH的人正在检查它是否错了
Williams将与加州大学圣地亚哥分校的Russell Impagliazzo和Ramamohan Paturi一起独立核查并解释这一结果。Impagliazzo和Paturi最初与Francis Zane共同提出了ETH。Williams写道,该团队没有签署任何保密协议,无偿工作,并计划在过程中分享阶段性发现。
在一封公开信中,三人还明确表示,他们的参与并不代表对这一主张的认可。他们写道,如此重大的结果需要仔细、独立的审查。
应团队要求,OpenAI正在公布所有原始数据,包括书面证明和Lean证明。该公司还承诺资助一场会议,讨论这一结果对该领域的意义。
一个存在数十年的波动猜想如今可能在所有维度上成立
这一数学结果涉及一个关于波(如声波、光波或地震波)的猜想。数学家Christopher Sogge于1991年提出了它。
波可以集中在一个点上,就像放大镜焦点处的光一样。该猜想认为,这种极端集中只会短暂持续。按时间平均来看,波的行为比极端情形所暗示的更平滑、更均匀。这就是它被称为局部光滑猜想的原因。
在此之前,它只在二维情形下得到证明,即像水面这样的表面上的波。Guth、Wang和Zhang在2019年做到了这一点。OpenAI表示,其模型现在已经为每个维度都给出了证明,包括空间中的波,以及维度更多的假想空间中的波。
OpenAI表示,这一结果的意义超出了波。由于局部光滑猜想是该领域如此基础的问题,另外两个著名猜想可由它推出。它们是几何学中的Kakeya猜想和傅里叶分析中的Stein限制猜想。傅里叶分析将声音等信号分解为各个振荡。证明局部光滑猜想会自动同时证明这两个猜想。
Kakeya猜想表明,即便是这些后续结果也有多难。Wang和Zahl直到2025年才仅对三维情形证明了它。据OpenAI称,这两个猜想现在都将在所有维度上得到解决。
与其他两项结果不同,没有专门团队在牵头推进这一证明。OpenAI表示,它确实联系了一位外部专家,讨论这种合作方式。不过,根据此人的建议,公司直接公布了证明文本和Lean证明。这样,研究人员可以自行决定如何核查这一结果。
OpenAI希望将量子场论置于坚实的数学基础之上
这一物理成果触及粒子物理学的根基。物理学家用OpenAI称之为现代理论物理学中最重要的框架——量子场论——来描述基本粒子及其之间的作用力。它的预测极其精确,但这些理论缺乏精确的数学基础。
于是,物理学家转而使用近似方法,例如一个不断被细化的假想点阵。这是否会产生一个唯一且自洽的理论,即该理论在数学意义上是否“存在”,仍是一个未解的问题。它是否正确描述了自然,则是另一个问题。
OpenAI表示,其AI已证明某些量子场论在四维中(即三维空间加时间)存在。迄今为止,还没有人在粒子相互作用的四维理论中完成过这样的证明。
强相互作用力处于其核心。它将夸克束缚成质子和中子,后者进而将原子核维系在一起。传递这种力的粒子被称为胶子。该证明涵盖三个层层递进的理论。
最底层是杨-米尔斯理论。它只描述胶子,不包含夸克。它与七个千禧年大奖难题之一相关,每个难题都由克莱数学研究所提供100万美元奖金。
该问题分为两部分。第一部分是证明杨-米尔斯理论在数学上存在。第二部分是证明它具有所谓的质量间隙。OpenAI明确表示,它只解决了存在性部分。这意味着该千禧年难题不会被完全解决。
质量间隙指向一个谜题。在方程中,胶子没有质量,而由无质量粒子传递的力通常会延伸到很远。由无质量的光所传递的电磁力就是一个例子。相比之下,强相互作用力只在极小的距离上起作用,例如在原子核内部。物理学家对此的解释是,胶子会聚集成确实具有质量的结构,而且即使其中质量最小的也不是无质量的。零与那个最小可能质量之间的差距被称为质量间隙。计算机模拟支持这一点,但还没有人从数学上证明它。
第二步是量子色动力学(QCD)。它加入了夸克,并给出了对强相互作用力的完整描述。
OpenAI表示,这两种理论之所以能在数学上存在,主要归功于渐近自由。这意味着粒子越接近,强相互作用力就越弱。即使点阵变得越来越精细,这也使数学处理保持可控。
第三步通常是粒子物理学的标准模型。它描述了四种基本力中的三种,即除引力之外的一切。不过,据OpenAI称,它无法被推广到任意小的距离,因为它的一些力在短距离上会变强而不是变弱。
这就是为什么该证明涵盖的是最简单的宏大统一理论。它把三种力归结为一种,并包含标准模型的力和物质粒子。与强相互作用力一样,这种统一力在短距离上可以变弱。不过,还没有实验证实这类理论。
如果该证明成立,那么这三个步骤都将拥有数学基础。这不会改变物理学的任何预测。OpenAI希望这将使量子场论成为一门数学上严谨的学科。
由David Gross领导的一个小组将负责这项工作。Gross因其在渐近自由方面的工作分享了2004年诺贝尔物理学奖。该小组还包括Michael Douglas、Arthur Jaffe、Igor Klebanov和Nikita Nekrasov。Jaffe曾参与撰写关于杨-米尔斯理论的千禧年大奖难题。
OpenAI表示,它已将杨-米尔斯证明翻译成Lean。不过,与计算机科学小组不同,这个小组目前暂不公开AI的材料,并计划自行撰写成果。
OpenAI的审查流程本身也引发了质疑
OpenAI承认这一流程存在权衡。公司写道,谁先选出第一批shepherd,就会帮助决定谁先参与进来,而有些人最终会比其他人更早了解更多情况。OpenAI还表示,目前尚不清楚这三种方式中哪一种效果最好。
OpenAI表示,它并不主张对这些发现有科学署名权。功劳应归于解释这些结果的小组。公司似乎是在回应Navier-Stokes公关灾难之后的批评。
OpenAI还承诺向Simons基金会提供500万美元,用于资助关于AI成果的研讨会和会议。
Williams的小组还利用其公开信呼吁展开超越审查本身的更广泛讨论。问题在于如何验证AI突破、谁能获得这些突破,以及谁应获得功劳。