指数时间假设被 OpenAI 模型推翻了？

10 月 26 日，OpenAI 在 openai/math 仓库中发布了论文《The Exponential Time Hypothesis is False》。据该论文，一个未公开的 OpenAI 内部模型推翻了指数时间假设（ETH），这是计算复杂性理论的基本假设之一。一个独立的计算机科学家小组（其中包括该假设的两位提出者）正在审查这篇论文及其 Lean 形式化证明。

什么是指数时间假设？

ETH（Exponential Time Hypothesis）假设：3-SAT 问题，即判断一个每个子句含三个变量的逻辑公式能否被满足，对于 n 个变量无法在快于 2^Ω(n) 的时间内判定。简单地说：每多一个变量，时间就呈指数增长，再巧妙的算法也改变不了这一点。

这一假设由 Russell Impagliazzo 和 Ramamohan Paturi（与 Francis Zane 合作）提出。数以百计的论文以 ETH 为基础，证明图论、数据库或计算生物学中的某个问题“不可能”被更快地解决（正如 The Next Web 所提到的）。

OpenAI 的模型到底证明了什么？

论文给出了一个确定性算法，能精确计数 k-CNF 公式的所有满足赋值，适用于任意固定的 k ≥ 2。它使用多项式空间，运行时间为 (n + m)^O(1) · 2^(n/(log n)^(1/2+o(1)))，即亚指数时间。仅 3-SAT 的情形就足以推翻 ETH。

有意思的是，这个算法不只回答“是”或“否”，而是计算解的个数。论文由此推出了更多结论：

1. 用于计数图着色、独立集和完美匹配的亚指数时间算法，
2. 在亚指数时间内对 Max-k-SAT 做任意精度的近似，
3. 针对 E^NP 类的逻辑电路规模的新下界。

据 The Next Web，模型在 10 月 16 日找到了证明，第二天就已在 Lean（一种让计算机检查证明的形式化语言）中完成验证。在仓库的变更记录中，OpenAI 表示论文是连同 Lean 形式化一起上线的。

谁在检验这个证明？

负责审查和解释该证明的小组由 Russell Impagliazzo、Ramamohan Paturi（UC San Diego）和 Ryan Williams（MIT）领导。根据仓库的变更记录，正是应这个小组的要求，材料才被立即公开，以便所有人都能检验。Williams 在 X 上写道，OpenAI 的一个内部模型给出了“claimed refutation of ETH”，即声称的对 ETH 的反驳。

研究人员没有签署任何保密协议，也不为此收取报酬（据 The Next Web）。他们要求 OpenAI 公开全部原始数据，并资助一场讨论该结果影响的会议，公司同意了。不过他们在公开信中强调，他们的参与并不代表对结果的确认（“should not be taken as certification of the claim”），并补充说，如果证明正确，“it will change an important part of theoretical computer science”。

这在 AI 领域算新鲜事吗？

这并不是 OpenAI 第一次发布此类成果。我们知道，10 月 6 日该公司就在同一个仓库里上传了 700 多篇由模型生成的数学论文。仓库的 README 中写道，模型拿到了约 4000 个开放问题，每个结果平均耗费了 ChatGPT Pro 级别的三小时“思考”。

新的是，10 月 26 日 OpenAI 一次公布了三项结果，并且为每一项选择了不同的路径（Unite.AI 对此有介绍）：

1. ETH：论文和 Lean 证明均已公开，由 Impagliazzo、Paturi 和 Williams 领导的开放小组进行检验。
2. 所有维度上的 Sogge“local smoothing”猜想：据 OpenAI，由它可以推出挂谷猜想和 Stein 限制猜想，同样附 Lean 证明发布。
3. 四维杨-米尔斯理论和 QCD 的存在性（克雷研究所千禧年大奖难题之一）：目前还没有任何材料。由诺贝尔奖得主 David Gross 领导的小组决定自行撰写这一结果。

OpenAI 还表示，不希望为其模型的发现获得科学荣誉，功劳应归于理解并阐述这些发现的人。公司还向西蒙斯基金会捐赠了 500 万美元，用于举办关于 AI 生成成果的研讨会和会议。

需要注意什么？

第一，验证的进展。Lean 形式化是一个强有力的信号，但始终需要检查 Lean 中写下的定理是否真的与论文正文表述一致。OpenAI 自己也在 README 中写道，部分未经形式化的结果可能有错误，并在 10 月 7 日因其中一个证明的符号错误撤回了三篇论文。所以在小组完成工作之前，我们还是对这个结果保持审慎。

第二，这个结果并不意味着什么。作者明确写道，不能由此推出所有 NP 问题都有亚指数时间算法。因此这并没有解决 P 与 NP 问题，运行时间仍然比任何多项式增长得都快。

第三，速度。理论学家研究了 20 多年的结果，据称是模型在一次内部评估中找到的。如果得到证实，这大概会是迄今为止 AI 在理论计算机科学中独立做出发现的最有力例证。顺带一提，形式化证明这个话题也再次回到视野中，我在写 Claude 的形式化验证时谈过它。

常见问题

什么是指数时间假设？

它是复杂性理论中的一个假设：对于 n 个变量，3-SAT 无法在少于 2^Ω(n) 的时间内求解。由 Impagliazzo 和 Paturi 与 Francis Zane 共同提出。

OpenAI 解决了 P 与 NP 问题吗？

没有。该算法是亚指数时间的，但不是多项式时间的，作者也指出这一结果并不适用于所有 NP 问题。

推翻 ETH 的证明已经得到确认了吗？

还没有。虽然已有 Lean 形式化证明，但由 Impagliazzo、Paturi 和 Williams 领导的独立小组才刚开始审查，并强调他们的参与不代表确认。

是哪个 OpenAI 模型做到的？

一个未公开的内部模型。OpenAI 在仓库 README 中没有给出它的名称。