OpenAI 宣称其 AI 证明 ETH 为假等三项重大结果,邀请外部专家审查
OpenAI asks outside experts, including a Nobel laureate, to check proofs its AI produced in math, computer science, and physics
OpenAI 请外部专家担任"shepherds"审查其 AI 产出的三项证明,并已将部分证明翻译成可逐步机器验证的 Lean 语言。
文章梳理了 OpenAI 三项数学、计算机科学与物理证明声明的内容,以及各领域专家独立的审查方式与保留态度。
因此 OpenAI 请外部专家担任这些结果的“牧羊人”。根据他们的建议,该公司对每个领域采取了不同的处理方式。OpenAI 表示,他们还将数学和计算机科学的证明翻译成了 Lean。
Lean 是一种编程语言,可以让计算机检查证明的每一步。不过,这并不能保证结果没有错误。Lean 只检查证明是否确立了用 Lean 语言写出的那个命题。至于该命题是否真正抓住了原本想解决的问题,仍需专家来判断。
如果 OpenAI 是对的,那么计算机科学的一个核心假设就是错的
这个计算机科学结果的核心是指数时间假说(ETH)。它涉及布尔可满足性问题,即 SAT。SAT 处理的是一个逻辑公式,其变量只能为真或假。问题是,你能否设置这些变量,使整个公式结果为真。
变量只有几个时,你可以直接尝试每一种组合。但每新增一个变量,可能的数量就翻一倍。有 100 个变量时,你面对的已经是一个 31 位的数字。
简单来说,ETH 认为不存在真正的捷径。你可以加快试错的速度,但在最坏情况下,计算时间仍然呈指数增长,每增加一个变量就按固定倍数增加。
OpenAI 表示,可满足性问题与P 与 NP 问题密切相关。那是一个著名的未解问题:一个解可以被快速验证的问题,是否也能被快速求解。以 SAT 为例,验证很容易,因为你只需代入一个候选答案并进行计算。难的是找到一个有效的答案。
SAT 被视为这类难题的教科书式范例。如果找到一种快速求解它的方法,数千个其他问题也会随之变得容易求解。大多数专家认为这样的方法并不存在。这一信念的简写就是“P 不等于 NP”。
ETH 比这一猜想走得更远。它不仅说 SAT 很难,还说出了有多难。即使 ETH 被推翻,P 仍可能不同于 NP,因此难题不会自动变得容易。
ETH 曾被广泛认为是正确的。图论、计算生物学、数据库和计算几何领域的数百篇论文都建立在其之上。例如,这些论文表明,如果 ETH 成立,某个问题就不可能以低于某一时间的速度求解。
如今 OpenAI 称其系统已证明 ETH 是错误的。如果这一证明成立,那些论文就失去了基础。它们的结果不会自动变成错误,但将不再是已被证明的。
OpenAI 表示,这一结果或许能帮助研究人员找到更好的算法。不过,要将其转化为实际收益,仍需要大量研究。
实际收益尚不明朗,但理论上的冲击将是巨大的
SAT 在实践中非常重要。例如,被称为SAT 求解器的专用程序可以检查芯片设计中的错误并测试软件。
这些程序如今经常处理拥有数百万个变量的公式。这是因为来自现实应用的公式通常比 ETH 所处理的最坏情况容易得多。仅加快最坏情况的处理速度并不能自动帮助这些程序。
MIT 教授 Ryan Williams 在X 上表达了同样谨慎的态度。当有用户问普通开发者最先会注意到什么时,Williams 表示目前没人知道。他说,按照当前的进度,实用的 SAT 求解有可能在 12 个月内取得重大进展。“也可能什么都不会发生。我真的不知道,”他坦言。
这一结果还将波及复杂性理论本身,尤其是对电路的研究——电路是由与门、或门和非门等简单逻辑门构成的网络。Williams 说,如果 OpenAI 的结果成立,那么可以推出某类非常苛刻的问题无法用小电路解决。这里的“小”是指当输入长度翻倍时,电路所需的门数量最多大约翻一倍。
提出 ETH 的人正在检验它是否错了
Williams 将与 UC San Diego 的 Russell Impagliazzo 和 Ramamohan Paturi 一起独立检验并解释这一结果。Impagliazzo 和 Paturi 当初是与 Francis Zane 共同提出 ETH 的。Williams 写道,这个团队没有签署任何保密协议,是无偿工作,并计划随时分享阶段性发现。
在一封公开信中,三人还明确表示,他们的参与并不意味着对该主张的认可。他们写道,如此重大的结果需要仔细、独立的审查。
应该团队的要求,OpenAI 正在公布所有原始数据,包括书面证明和 Lean 证明。该公司还承诺出资举办一场会议,探讨这一结果对该领域的意义。
一个有几十年历史的波 conjecture 可能在所有维度上都成立
这一数学结果涉及一个关于波的猜想,例如声波、光波或地震波。数学家 Christopher Sogge 于 1991 年提出了这个猜想。
波可以集中于一个点,就像光通过放大镜的焦点。该猜想认为,这种极端的集中只能持续很短的时间。从时间上平均来看,波的表现比极端情况所暗示的更平滑、更均匀。因此它被称为局部平滑猜想(local smoothing conjecture)。
此前,它只在二维情况下被证明过,即水面等表面上的波。Guth、Wang 和 Zhang 在 2019 年完成了这项工作。OpenAI 表示,其模型现在已经给出了适用于所有维度的证明,包括空间中的波,以及维度更多的假想空间中的波。
OpenAI 表示,这一结果的影响超出了波的范围。由于局部平滑猜想是该领域的基础,另外两个著名的猜想可以由它推出。它们分别是几何学中的挂谷猜想(Kakeya conjecture)和傅里叶分析中的 Stein 限制猜想。傅里叶分析将声音等信号分解为单个振荡。证明局部平滑猜想会自动证明这两个猜想。
挂谷猜想显示了即便这些后续结果有多么困难。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 承认这一流程存在权衡取舍。该公司写道,由谁来挑选首批指导者,就有助于决定谁最先参与其中,有些人会比其他人更早知道更多内容。OpenAI 还表示,目前尚不清楚这三种方法中哪一种效果最好。
OpenAI 表示,它并不声称对这些发现拥有科学上的功劳。功劳应归于解释这些结果的团队。该公司此举似乎是在回应Navier-Stokes 的公关灾难之后受到的批评。
OpenAI 还承诺向西蒙斯基金会(Simons Foundation)捐款 500 万美元,用于资助关于 AI 研究成果的研讨会和会议。
Williams 的团队还利用其公开信呼吁开展超越评审的更广泛讨论。问题包括如何验证 AI 的突破、谁可以使用这些成果,以及谁应当获得功劳。
来源: The Decoder · the-decoder.com