OpenAI、Anthropic 模型证伪长期存在的指数时间假设

OpenAI 和 Anthropic 均发布了由 AI 驱动的研究结果，声称证伪了计算复杂性理论中的长期猜想——指数时间假设。

10月26日，OpenAI 宣布其模型生成了一份证明，表明指数时间假设是错误的。该假设于21世纪初提出，断言 3-SAT 无法在亚指数时间内求解——这意味着，一些常见的逻辑谜题无法比穷举所有可能答案快得多地解决。

由于该假设已被广泛接受，并被数百篇论文用于推导众多领域中的条件计算难度结果，证伪它将使其中相当一部分结果失效，并迫使研究人员重新评估算法、图论和计算生物学等领域问题的计算难度。

这家 AI 公司表示，其模型于10月16日生成了这份自然语言证伪，并于次日将其在 Lean 数学证明助手中形式化；两项成果均已发布在一个公开的 GitHub 仓库中。

OpenAI 表示，这项工作正由一个外部团队进行审查，该团队由加州大学圣迭戈分校的 Russell Impagliazzo 和 Ramamohan Paturi——该假设最初的两位提出者——以及 MIT 的 Ryan Williams 领衔。

Williams 在 X 上表示，研究人员仍在弄清楚这一发现的实际影响。

Williams 说：“按照目前的进展速度，我们有理由相信，未来12个月内可能会看到关于实际 SAT 求解的重大进展。也可能完全看不到类似进展。我确实不知道。”

与此同时，Anthropic 也发布了一篇论文及 Lean 4 形式化证明，称某种确定性算法能够求解 3-SAT，而这将证伪指数时间假设。该公司表示，其内部 Claude 研究模型于10月16日发现了核心算法——这与 OpenAI 模型取得该发现的时间是同一天——整个过程使用了1400万输出 token，未获得人类输入。

Anthropic 指出：“这一结果纯粹是渐近意义上的，并未说明如何在实践中求解公式。”

与此同时，OpenAI 还公布了另外两项由 AI 生成的结果：调和分析中关于所有维度的局部平滑猜想的证明，以及某些量子场论存在性的数学严谨证明，其中包括量子色动力学和纯 Yang-Mills 理论。