AI 推翻了「指數時間假說」？從排聚會名單講起

10 月 26 日，OpenAI 和 Anthropic 在同一天宣布，自家的內部模型證明了「指數時間假說」（Exponential Time Hypothesis，ETH）是錯的。¹² 這個假說從 1999 年提出到現在，一直是理論電腦科學最常用的前提之一，光是 Anthropic 讓 Claude 做的文獻搜尋，就找到八百多篇論文，至少有一個結果只在 ETH 或更強的假設下才成立。²

這篇想回答兩個問題：ETH 到底說了什麼，為什麼那麼多研究靠它；AI 又是用什麼辦法推翻它的。先說結論：如果證明站得住，這是理論電腦科學很大的意外，但它不會讓任何實際的程式變快；而且到我寫這篇的時候，還沒有任何人類審查完這兩份證明。

文中有四個可以動手玩的小工具，抽象的地方建議點一點。「給數學好的讀者」是摺疊區塊，放公式和精確的敘述，跳過也不影響閱讀。

排聚會名單

假設你要決定 A、B、C、D 四個朋友誰來參加聚會，每個人只有「來」和「不來」兩種狀態。大家各有要求，每條要求只提到三個人：

• 條件 1：A 來，或 B 不來，或 C 來
• 條件 2：B 來，或 C 不來，或 D 來
• 條件 3：A 不來，或 C 不來，或 D 不來

每條要求列的三件事，只要有一件成立就算過關。問題是：有沒有一種安排，能讓所有要求同時過關？

試一組看看：A 來、B 來、C 不來、D 不來。條件 1 靠「A 來」過關，條件 2 靠「B 來」，條件 3 靠「C 不來」。三條都過了，所以有解。

這就是 3-SAT，電腦科學裡最有名的難題之一。名字裡的 3，指每條要求最多提到三個人。每條要求裡面用的是「或」，所以每條都留了幾條路可走；困難就在這些選擇互相牽制，這裡選了 A 來，可能讓別條要求少一條路。

四個人只有 $2^4 = 16$ 種安排，一個一個試很快。換成 100 個人，安排方式就有 $2^{100}$ 種，大約是 $1.3 \times 10^{30}$。一台電腦每秒檢查十億種，要跑四十兆年左右，大約是宇宙年齡的三千倍。

學界賭的是什麼

「一個一個試」需要 $2^n$ 步。從 1980 年代起，研究者不斷找到更聰明的做法，可是每一次進步都只是把底數變小：$1.618^n$、$1.5^n$、$1.334^n$，到 2018 年確定性演算法的紀錄是 $1.328^n$，隨機演算法則是 $1.308^n$。²

底數變小在實務上差很多。$1.328^{100}$ 大約是 $2 \times 10^{12}$，每秒十億步的話半小時就跑完。可是這種演算法仍然是「指數」的：人數每多一個，時間就乘上 1.328，多 100 個人，時間就乘上 $2 \times 10^{12}$。

ETH 賭的是這件事改不了。它說：存在某個大於 1 的底數，任何演算法在最壞情況下都壓不到它下面。底數也許能從 1.308 再往下降一點，但永遠降不到 1。

這個賭注比更有名的 P ≠ NP 還強。P ≠ NP 只說 3-SAT 沒有「多項式時間」的演算法，也就是時間不可能像 $n^2$、$n^{100}$ 這樣成長。在多項式和指數之間，還有一大片空間，例如 $2^{\sqrt{n}}$：它比任何多項式都慢，卻比任何 $c^n$ 都快。ETH 說 3-SAT 不會落在這片中間地帶。

研究者會接受這麼強的賭注，是因為它很好用。要證明某個問題「沒有快速演算法」，現有的數學工具幾乎做不到；退一步證明「如果 ETH 成立，這個問題就不可能比某個速度快」，就容易得多。圖論、資料庫、計算生物裡很多「這已經是最好的做法」的結論，都是這種條件句。ETH 一倒，這些條件句的前提就沒了，結論也就不再告訴我們任何事。

先換個問題：不找解，改成數解

兩份證明都從同一個轉彎開始：不去問「有沒有解」，改問「有幾組解」。數到 0 就是沒有解，所以會數就會判斷。

數解聽起來比找解更難，好處是它可以寫成算術。把每條要求寫成一個算式：過關時等於 1，不過關時等於 0。把所有要求的算式乘起來，只有每條都過關的安排會得到 1，其他都是 0。把每一種安排的乘積加總，就是解的個數。

前面「自己排排看」最下面那 16 格，就是這個加總：每一格是一種安排的乘積，加起來就是解的個數。

這樣一來，問題變成「怎麼算一個很大的加總」。加總可以重新分組、可以交換順序，這是代數的強項。

拆開來數

接下來的想法很直觀。把每個人畫成一個點，兩個人出現在同一條要求裡，就在他們之間連一條線。

如果這張圖剛好分成兩群，兩群之間只有兩條線相連，事情就簡單了：把線一端的兩個人狀態固定下來，總共只有 4 種可能；每一種可能下，兩群各自數自己的解，乘起來，再把 4 種情況加總。原本要一起試的組合，被拆成兩個小得多的問題。下面的工具可以按「逐一固定紅點」看這個過程。

麻煩在「纏成一團」那種圖，切換過去、把人數拉大看看。隨機產生的難題通常長得像一團亂麻，數學上叫「擴展圖」（expander）：不管怎麼切成兩半，跨過切口的線都跟人數成正比。這時候光是「固定跨過去的人」就有指數多種可能，拆開來數並沒有省到本質上的時間。過去用分而治之的辦法，只能改進指數前面的常數，原因就在這裡。²

允許負數

Anthropic 的模型找到的突破，是一個改寫線的辦法。

把要求分成很多小群，排成棋盤的格子。棋盤上任選兩列兩行，交叉出一個長方形的四個角，左上 $x$、右上 $y$、左下 $u$、右下 $v$。如果這四個角之間有兩條斜對角的線，就表示「$x$ 要跟 $v$ 對齊」而且「$y$ 要跟 $u$ 對齊」。如果把每一列合併成一群，上下兩群之間就得對齊兩份資訊。

模型用了一條 1818 年由 Degen 發現的「八平方恆等式」，它跟八元數（octonion）的乘法有關。² 這條恆等式能把「兩條斜線」改寫成兩項相加，而且每一項裡都有正負號。把上下兩列各合成一群時，其中一項只要求兩群對齊「$x$ 和 $y$ 合起來的一份摘要」，資訊量少了一半；另一項還是要對齊兩份，要換成左右兩行合併才便宜。下面可以自己挑 $x$、$y$、$u$、$v$，確認兩項加起來永遠等於原式。

改寫後的單一項不再代表任何真的解，有些項甚至是負數。這有點像記帳時先記一筆借出、再記一筆還回：中間的帳目看起來對不上，最後的總數卻一分不差。整個證明只需要最後的加總正確，中間每一項是不是「有意義」並不重要。

細算下來，每次改寫加上重新分組，群與群之間要對齊的資訊大約剩下原本的 $\frac{11}{12}$。² 省下的只有十二分之一，關鍵在於這一步可以重複：分組、改寫、再分組，每一層都乘上一次 $\frac{11}{12}$。疊了 $\ell$ 層，指數大約縮成 $(\frac{11}{12})^{\ell}$ 倍。不管你要求的 $\delta$ 多小，只要疊夠多層，總能壓到它下面。這正是推翻 ETH 需要的。

OpenAI 的證明走的是另一條路。它把每個變數換成帶一個參數的「替身」，在參數取某些值的時候，各群之間只剩少數幾個共享的數值；算出這些值之後，再用內插法把參數為 0 的答案還原回來，那就是真正的解數。³ 兩條路的共同點是：用代數把加總重新分組，讓各群之間需要對齊的資訊少到比 $n$ 慢一點點地成長。已經有學者 Shiva Kintali 寫出 OpenAI 證明的簡化版。⁴

到底快了多少

新演算法的時間大約是 $2^{n/\sqrt{\log n}}$ 這個等級。分母的 $\sqrt{\log n}$ 長得極慢，$n$ 是一百萬時也才 4.5 左右，所以它只比 $2^n$ 好一點點，而且前面還藏著天文數字的常數：光是第一層的群數就是 $9 \times 2^{96}$。

Anthropic 的論文自己算過：一般的 3-SAT 公式，$n$ 要超過 $10^{10000}$，這個演算法的保證才會贏過一個一個試；不限要求條數的版本，要超過 $10^{10^8}$。而 $n = 100$ 的時候，一個一個試就已經跑不完了。論文的原話是：「我們的結果對實際解公式沒有任何幫助。」²

所以有幾件事沒有改變：

• P 和 NP 是否相等，仍然未知。 新演算法還是比任何多項式都慢。
• 實際的 SAT 求解器不會變快。 晶片驗證、排程用的那些工具，靠的是針對真實資料的技巧，跟最壞情況的理論保證是兩回事。
• 不是所有 NP 問題都跟著變快。 把別的問題轉換成 3-SAT 時，變數可能變多，這點微小的優勢就被吃掉了。能直接受惠的是獨立集、團、點覆蓋、支配集這類能用差不多數量的變數轉換的圖論問題。²

AI 是怎麼做出來的

依 Anthropic 的說法，核心演算法是 10 月 16 日由一個內部研究用的 Claude 模型找到的，過程輸出了 1,400 萬個 token，沒有任何人類參與；之後研究人員和 Claude 一起改寫，才成為現在的論文。² OpenAI 那邊說，它的模型同一天寫出自然語言證明，隔天完成形式化。⁵ 兩家都說彼此是各自獨立做出來的。

論文附錄有一節，事後重建了「為什麼會想到八平方恆等式」：如果你想找一種比較便宜的方式改寫那兩條斜線，順著兩個自然的猜測走下去，就會走到 Hurwitz 在 1898 年處理過的平方和問題，而它最極端的解，正好是二、四、八平方恆等式。² 用到的零件都是數學家熟悉的舊東西，新的是把兩百年前的代數恆等式，接到計算複雜度的問題上。

兩家都把證明寫進了 Lean。Lean 是一種「證明助理」程式，會逐步檢查證明的每一個推論是否合法，人眼看漏的錯它不會放過。Anthropic 的 Lean 證明有 1,050 個模組，通過了 Lean 的核心、另一個重播檢查器，以及一個獨立實作的檢查器 nanoda。²

Lean 的保證有兩個缺口，Anthropic 的論文自己寫得很清楚：

• 敘述對不對，機器不能檢查。 Lean 保證證明符合「寫下來的那個敘述」，至於那個敘述是不是真的等於「ETH 是錯的」，得由人讀過才能判斷。這有點像會計師把每一筆帳都核對過，卻沒辦法替你確認查的是不是對的那家公司。
• 目前沒有人類檢查過。 這份 Lean 證明是 AI 寫的，由同一批模型的其他實例審閱；論文寫明，在撰稿時沒有已知的人類檢查過它。²

人類的審查才剛開始。當年提出 ETH 的 Russell Impagliazzo 和 Ramamohan Paturi，加上 MIT 的 Ryan Williams，組了一個公開的工作小組來檢驗 OpenAI 的證明，並且明說參與審查不代表背書。應他們的要求，OpenAI 公開了全部材料，也答應出資辦一場研討會。⁶

所以呢

現在能確定的是：兩家實驗室各自宣稱推翻了 ETH，用的辦法不同，都附上了機器檢查過的證明，細節也公開了。還不能確定的是：這些形式化的敘述是不是真的說了它們想說的話，以及人類專家讀完以後會不會找到問題。

如果證明站得住，受影響的是理論：八百多篇論文裡依賴 ETH 的結論要重新檢查，「3-SAT 一定要指數時間」這個幾十年的直覺也得改掉。Hacker News 上有人提到，早年像 Knuth 那一輩的研究者，常常遇到某個問題突然冒出意想不到的快速演算法；後來的世代比較習慣證明「這件事做不快」。這次的結果，可能讓鐘擺往回盪一點。

實務上的東西不會變。你手機裡的加密、工廠的排程軟體，明天都一樣。

接下來幾個月，要看的是 Impagliazzo、Paturi 和 Williams 的小組，以及其他讀過這些證明的人怎麼說。