OpenAI 请外部专家核查 AI 在数学、计算机科学与物理领域生成的证明
OpenAI asks outside experts, including a Nobel laureate, to check proofs its AI produced in math, computer science, and physics

OpenAI 邀请外部专家担任“shepherd”,核查其 AI 在数学、计算机科学和物理三个领域生成的证明,并按各领域情况分别处理。数学与计算机科学的证明已被翻译成 Lean,计算机科学结果声称推翻了指数时间假设(ETH),数学结果声称证明了所有维度上的局部平滑猜想。
OpenAI 把三项 AI 生成的证明交给外部专家审阅,读者可据此了解 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 等简单逻辑门组成的网络。如果 OpenAI 的结果成立,Williams 表示,这意味着某些特定类型的非常复杂的问题无法用小电路解决。"这里的小"是指当输入长度加倍时,电路所需的门数最多增加一倍。
提出 ETH 的人正在检查它是否错误
Williams 将与加州大学圣地亚哥分校的 Russell Impagliazzo 和 Ramamohan Paturi 独立检查和解释结果。Impagliazzo 和 Paturi 最初与 Francis Zane 一起提出了 ETH。Williams 写道,该小组没有签署任何保密协议,是无偿工作,并计划分享他们的中期发现。
在一封 公开信 中,三人还明确表示他们的参与并不代表对这一主张的认可。他们写道,如此重大的结果需要仔细、独立的审查。
应该小组的要求,OpenAI 正在发布所有原始数据,包括 书面证明 和 Lean 证明。该公司还承诺资助一个会议,讨论这一结果对该领域的影响。
一个几十年的波动猜想现在可能适用于所有维度
这一数学结果涉及一个关于声波、光波或地震波的猜想。数学家 Christopher Sogge 于 1991 年提出了这一猜想。
波可以集中在一个点上,就像放大镜的焦点处的光一样。该猜想说这种极端集中只是短暂的。从时间上平均来看,波的行为比极端情况所暗示的更加平滑或均匀。这就是它被称为局部平滑猜想的原因。
Until now, it had only been proven in two dimensions, for waves on a surface like water. Guth, Wang, and Zhang did that in 2019. OpenAI says its models have now produced a proof for every dimension, including waves in space and in hypothetical spaces with even more dimensions.
OpenAI 表示,这一结果超出了波的范围。由于局部平滑猜想对该领域如此基本,另外两个著名的猜想也随之而来。它们是几何中的 Kakeya 猜想 和来自 傅里叶分析 的 Stein 限制猜想。傅里叶分析将声音等信号分解为单个振荡。证明局部平滑猜想将自动证明这两个猜想。
The Kakeya conjecture shows how hard even these follow-on results are. Wang and Zahl only proved it for three dimensions in 2025. According to OpenAI, both conjectures would now be solved in all dimensions.
与其他两个结果不同,没有专门的小组来指导这个证明。OpenAI 表示,它已经联系了一位外部专家来讨论这种合作。然而,根据该人士的建议,该公司直接发布了 证明文本 和 Lean 证明。这样,研究人员就可以自行决定如何检查结果。
OpenAI 希望将量子场论建立在坚实的数学基础上
这个物理学成果关系到粒子物理学的根基。物理学家使用 量子场论 来描述基本粒子和它们之间的力,OpenAI 称其为现代理论物理学中最重要的框架。它的预测极其准确,但该理论缺乏精确的数学基础。
相反,物理学家使用近似方法,例如一个他们不断使其更精细的 虚点格。这仍然是一个悬而未决的问题,即这是否会产生一个独特、一致的理论,这意味着在数学意义上该理论是否存在。它是否正确描述自然是一个独立的问题。
OpenAI 表示,其人工智能已经证明了某些量子场论在四维空间中存在,这意味着三维空间加一维时间。到目前为止,还没有人能在四维空间中为粒子相互作用的场论完成这样的证明。
强大的力处于其中心。它将夸克结合成质子和中子,而质子和中子反过来又使原子核结合在一起。胶子这种粒子携带这种力。该证明涵盖了三个相互关联的理论,就像台阶一样。
最底层的台阶是 杨-米尔斯理论。它只描述胶子,而不描述夸克。它与七项千禧年大奖难题之一有关,每一项都由克雷数学研究所提供 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 表示,他们不声称对发现享有科学信用。信用应该归功于解释结果的团队。该公司似乎是对《纳维-斯托克斯的公关灾难》后的批评做出的回应。
OpenAI 还承诺向 西蒙斯基金会 提供 500 万美元,用于资助关于 AI 结果的工作坊和会议。
Williams 的团队也利用其公开信呼吁进行更广泛的讨论,超越审查。问题是如何验证 AI 的突破,谁有权访问它们,以及谁应获得信用。
来源: The Decoder · the-decoder.com