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

OpenAI 请外部专家担任“牧羊人”，核查其 AI 在计算机科学、数学和物理学领域产出的三项证明。根据专家建议，公司对每个领域采取了不同的处理方式，并将数学和计算机科学证明翻译成 Lean。Lean 是一种编程语言，可以让计算机检查证明的每一步，但它只检查证明是否按照 Lean 中所写的那样确立了该陈述，专家仍需判断该陈述是否真正抓住了预期的问题。 计算机科学方面的结果围绕指数时间假设（ETH）展开，涉及布尔可满足性问题 SAT。ETH 曾被广泛接受为真，图论、计算生物学、数据库和计算几何领域的数百篇论文都建立在它之上。OpenAI 表示其系统已证明 ETH 是假的。MIT 教授 Ryan Williams 将与 ETH 提出者 Russell Impagliazzo 和 Ramamohan Paturi 一起独立核查并解释这一结果，三人表示参与并不代表认可该主张。应团队请求，OpenAI 正在公布所有原始数据，包括书面证明和 Lean 证明，并承诺资助一场会议。 数学结果涉及数学家 Christopher Sogge 于 1991 年提出的局部平滑猜想，此前只在二维情况下得到证明。OpenAI 表示其模型现已为每个维度给出证明，并称该结果可推出几何学中的挂谷猜想和傅里叶分析中的 Stein 限制猜想。与另外两项不同，没有专门团队主导这项证明的核查，OpenAI 直接公布了证明文本和 Lean 证明。 物理学成果触及量子场论基础。OpenAI 表示其 AI 已证明某些量子场论在四维中存在，涵盖杨-米尔斯理论、量子色动力学（QCD）和最简单的 大统一理论 三个层层递进的理论。OpenAI 明确表示只解决了杨-米尔斯理论的存在性部分，未证明质量间隙，因此该千禧年难题并未被完全解决。由 David Gross 领导的团队将负责推进这项工作，该团队目前暂不公开 AI 的材料，并计划自行撰写成果。 OpenAI 承认评审流程存在权衡，并承诺向 Simons Foundation 提供 500 万美元，用于资助关于 AI 成果的研讨会和会议。