跳到正文
The Decoder:AI News· Maximilian Schreiner·· 2 小时前精选AI 评分79

OpenAI 请外部专家核查其 AI 在数学、计算机科学和物理学领域产出的证明

OpenAI asks outside experts, including a Nobel laureate, to check proofs its AI produced in math, computer science, and physics

AI 导读

The Decoder 报道 OpenAI 请外部专家担任"shepherds"核查其 AI 在计算机科学、数学和物理学领域的三项证明结果,并将部分证明翻译成 Lean 供计算机逐步验证。

推荐理由

文章梳理了三项数学级结果与专家核查安排,并点出 Lean 只能验证形式化陈述这一局限。

正文 · AI 翻译

因此,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 个月内取得重大进展是有可能的。“或者我们可能什么也看不到。我真的不知道,”他承认道。

这一结果还会在复杂性理论本身引发连锁反应,特别是电路研究——电路是由 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 表示,这一结果的意义超出了波本身。由于局部平滑猜想是该领域的基础性猜想,另外两个著名猜想可由它推出。它们分别是几何学中的挂谷猜想和傅里叶分析中的 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 曾参与撰写关于 Yang-Mills 理论的千禧年大奖难题。

OpenAI 表示,它已将 Yang-Mills 证明翻译成 Lean。不过,与计算机科学团队不同,该团队目前暂不公开 AI 的材料,并计划自行撰写成果。

OpenAI 的评审流程本身也引发质疑

OpenAI 承认这一流程存在权衡。公司写道,谁先挑选首批评审者,就会帮助决定谁先参与其中,而有些人会比其他人更早了解到更多信息。OpenAI 还表示,目前尚不清楚这三种方法中哪一种效果最好。

OpenAI 表示,它并不为这些发现主张科学功劳。功劳应归于解释结果的团队。该公司似乎是在回应 Navier-Stokes 公关灾难之后的批评。

OpenAI 还承诺向 Simons Foundation 提供 500 万美元,用于资助关于 AI 成果的研讨会和会议。

Williams 的团队还利用其公开信呼吁展开超越评审本身的更广泛讨论。问题在于如何验证 AI 突破、谁能获得这些突破,以及谁应获得功劳。

来源:The Decoder:AI News · the-decoder.com