ETHの反証をOpenAIとAnthropicが同日発表、計算量の式と検証状況を原典で確かめた

「OpenAIのAIが計算複雑性理論で重要な予想であるETHを反証した」という話が、学者とOpenAIのやりとりを模したポストで流れてきた。
ChatGPTに尋ねると、10月26日にOpenAIが実際に発表した話だという。
ただ、ChatGPTの解説には計算量の式が書かれている一方で、どこまでが原典どおりなのか分からなかった。
そこでOpenAIの発表と論文、Leanの形式証明、検証を任された研究者の投稿を開いて、式といきさつを確かめてみた。
調べていくうちに、ChatGPTの説明にはなかった事実がもう1つ出てきた。発表の数時間後には、Anthropicも同じ計算量のETH反証を公開していた。

ETHは3-SATについての予想

ETH（Exponential Time Hypothesis、指数時間仮説）は、3-SATという問題の解きにくさについての予想だ。
3-SATでは、 $n$ 個の真偽値変数 $x_1, \ldots, x_n$ と、「3個以下のリテラルの論理和（OR）」を節として論理積（AND）でつないだ論理式が与えられる。
リテラルは変数 $x_i$ かその否定 $\lnot x_i$ のことで、たとえば $(x_1 \lor \lnot x_2 \lor x_3) \land (\lnot x_1 \lor x_4)$ のような式になる。すべての節を同時に真にする真偽値の割り当てがあるかどうかを判定する問題で、NP完全問題の代表例として知られている。

もっとも単純な解き方は全探索で、変数ごとに真か偽かの2通りを試す。
割り当ては全部で $2^n$ 通りあり、1つずつ論理式に代入すれば必ず答えが出る。
割り当て1つの確認には式の長さに比例する時間がかかるので、全体ではおおよそ $2^n \cdot \mathrm{poly}(n, m)$ になる（ $\mathrm{poly}(n, m)$ は $n$ と節数 $m$ の多項式因子）。

全探索より速いアルゴリズムは昔から知られている。
OpenAIの論文の関連研究の節に挙がっている代表的な手法を、底を2に直した指数と並べると次のようになる。

アルゴリズム	種類	計算時間	底を2に直した形
全探索	決定的	$2^n$	$2^{1.000n}$
Schöningの局所探索（1999年）	乱択	$(4/3)^n$	$2^{0.415n}$
Liu（2018年）	決定的	$1.32793^n$	$2^{0.409n}$
PPSZ系の改良（Jiang・Caiのプレプリント）	乱択	$1.307031578^n$	$2^{0.386n}$

どれも全探索より速いが、 $n$ が1増えると時間が一定の倍率で伸びる形のままになっている。
ETHは、これより速い形にはならないという予想だ。
ImpagliazzoとPaturi（2001年）の定義では、3-SATを $O(2^{\delta n})$ 時間で解く決定的アルゴリズムが存在する $\delta$ の下限を $s_3$ と置き、ETHを $s_3 > 0$ と定めている。
言い換えると、ある正の定数 $\delta$ があって、どんなアルゴリズムも $2^{\delta n}$ より速くはならないという主張だ。

反証するには、逆に「どんなに小さい $\delta > 0$ を選んでも、 $O(2^{\delta n})$ 時間で3-SATを解くアルゴリズムがある」と示せばよい。
計算時間が $2^{o(n)}$ のアルゴリズムが1つあれば反証になる。
$o(n)$ は「 $n$ で割ると、 $n$ を大きくしたときに0へ近づく量」のことで、指数部を $n$ で割った値がいくらでも小さくなるため、どの $\delta$ に対してもいずれ $2^{\delta n}$ を下回る。

論文が主張している計算量

OpenAIの論文「The Exponential Time Hypothesis is False」は、3-SATの充足判定だけでなく、真にする割り当ての個数を数える問題（# $k$ -SAT、シャープ・ケー・サット）を解くアルゴリズムを示している。個数が分かれば、それが0より大きいかで判定もできる。
各節が $k$ 個以下のリテラルからなる論理式（ $k$ -CNF）を対象にし、 $k \ge 2$ を固定したまま $n$ を大きくしていく設定だ。論文の日付は10月17日で、10月25日に改訂されている。

論文要約（アブストラクト）の計算時間は次の式で、使うメモリは $n$ と $m$ の多項式サイズに抑えられる（ $O_k(1)$ は $k$ に依存する定数）。

(n+m)^{O_k(1)} \, 2^{\,n/(\log n)^{1/2+o(1)}}

定理1.1では、これを具体的な2つの上界として書いている（ $\log$ は自然対数）。

条件	計算時間の上界
一般の $k$ -CNF	$(n+m)^{O_k(1)} \, 2^{O_k(n \log\log n / \sqrt{\log n})}$
節の数が $m \le Dn$ （ $D$ は定数）のとき	$(n+m)^{O_{k,D}(1)} \, 2^{O_{k,D}(n / \sqrt{\log n})}$

節の数が変数の数の定数倍の範囲になる場合は $2^{O(n/\sqrt{\log n})}$ で、一般の場合には $\log\log n$ の因子が加わる。

数を数えるアルゴリズムなので、#3-SATに $2^{\Omega(n)}$ 時間かかるとする#ETH（数え上げ版のETH）も同時に否定している。
対象には $k = 2$ も含まれる。2-SATの充足判定は線形時間で解けるが、解の個数を数え上げる#2-SATは#P完全で指数時間かかる。判定問題なら簡単でも数え上げになると急激に難しくなるため、論文でもWahlströmの $O^*(1.2377^n)$ 時間のアルゴリズムが比較対象に挙がっている。

指数部が本当に o(n) に入るか

指数部を $n$ で割ると、 $1/\sqrt{\log n}$ や $\log\log n/\sqrt{\log n}$ になる。
$\log n$ は $\log\log n$ よりずっと速く増えるため、どちらも $n \to \infty$ で0に近づく。
Leanで形式化された上界（後述する $(\log\log n)^2$ の形）も含め、Pythonの数式処理ライブラリSymPyで極限を計算してみた。

import sympy as sp
n = sp.symbols('n', positive=True)
L = sp.log(n)
for e in [n/sp.sqrt(L), n*sp.log(L)/sp.sqrt(L), n*sp.log(L)**2/sp.sqrt(L)]:
    print(e, sp.limit(e/n, n, sp.oo))

3つとも極限は0になった。
どの形でも計算時間は $2^{o(n)}$ に入り、多項式因子 $(n+m)^{O(1)}$ が掛かっても、3-SATでは重複しない節の数が $n$ の多項式で抑えられるため結論は変わらない。提示された式の形を見る限りは、たしかに $2^{o(n)}$ の枠に入っている。

指数時間未満でも実用上速くならない理由

$2^{o(n)}$ は指数部の伸び方が $n$ より遅いというだけで、実際の計算規模が小さいことを意味しない。
$O(\cdot)$ の定数を1と仮定して、指数部を $n$ で割った値をPythonの任意精度計算ライブラリmpmathで計算してみた（自然対数）。

$n$	$1/\sqrt{\log n}$	$\log\log n/\sqrt{\log n}$	$(\log\log n)^2/\sqrt{\log n}$
$10^{3}$	0.381	0.735	1.421
$10^{6}$	0.269	0.706	1.855
$10^{9}$	0.220	0.666	2.018
$10^{100}$	0.066	0.358	1.950
$10^{1000}$	0.021	0.161	1.249
$10^{10000}$	0.0066	0.066	0.665

$n = 10^9$ でも、もっとも減少が速い $1/\sqrt{\log n}$ が0.22にしかならない。
PPSZ系アルゴリズムの0.386と大差なく、隠れている定数次第では大小が入れ替わる可能性もある。右端の列のLean版の上界の形では、1を下回るのは $\log n \approx 5504$ 、つまり $n \approx 10^{2390}$ を超えてからだった。

Anthropicの論文は、自分たちの上界について定数まで含めて同じ計算をしている。
$m = 5n$ の3-CNFでも全探索の $2^n$ を下回るのは $n > 10^{10000}$ からで、 $n$ だけで書いた上界では $n > 10^{10^8}$ からだという。全探索は $n = 100$ でも現実的でないため、この計算規模では実用上のアルゴリズムとしては機能しないと論文自身が明記している。OpenAIの発表も、理論上の進歩を実用的な改善に変えるには追加の研究が必要だとしている。

発表までの経緯

OpenAIの発表「Working with academic communities to build scientific understanding」と、公開リポジトリ openai/math の更新履歴、Anthropicの論文から時系列を整理すると次のようになる。

日付（米国時間）	出来事	出典
9月9日	OpenAIのモデルが純粋ヤン・ミルズ理論の存在証明を自然言語で出力	OpenAI発表
9月18日	同じくQCD（量子色力学）の存在証明を出力	OpenAI発表
10月6日	OpenAIが内部モデルの数学論文を一括公開（721本・373系統のトピック）	リポジトリのREADME
10月7日	うち3本を符号の誤りで撤回	history.md
10月16日	OpenAIのモデルがETHの反証を自然言語で出力	OpenAI発表
10月16日	Anthropicの内部Claudeモデルが中心となるアルゴリズムを発見	Anthropic論文
10月16日	OpenAIがヤン・ミルズ存在証明のLean形式化を完了	OpenAI発表
10月17日	OpenAIがETH反証をLeanで形式化	OpenAI発表
10月18〜19日	局所平滑化予想の証明を出力し、翌日にLean形式化	OpenAI発表
10月26日	OpenAIが3件を発表し、ETHの論文とLean証明をGitHubで公開	OpenAI発表、リポジトリ
10月26日夜	Anthropicが論文とLean証明を anthropics/formal-math で公開	リポジトリのコミット

OpenAIのリポジトリへの反映はUTCで10月26日21時18分、Anthropicのコミットは10月27日3時7分で、日本時間ではそれぞれ10月27日6時18分と12時7分だった。約6時間の差で公開されたことになる。
Anthropicの論文によると、Claudeは出力1400万トークンを使い、人間の介入なしにアルゴリズムを見つけ、論文の体裁はAnthropicの研究者がClaudeの出力を元に整えた。同じ論文は、OpenAIの内部モデルも同時期に似た結果を証明したとするプレプリントを引用している。
TechCrunchの記事は、Anthropic所属の数学者Levent Alpöge氏がOpenAIの結果は既存の研究に基づいていると指摘し、その数時間後にAnthropicが独自の反証を出したと伝えている。

Anthropicの README に書かれている計算量は $2^{O(n \log\log n/\sqrt{\log n})}$ で、OpenAIの定理1.1の一般の場合と同じ形だ。定理1はさらに、節の数 $m$ で書いた上界 $2^{O(km/\sqrt{\log m})}$ との小さいほうを取る形になっている。
2つの論文は手法の説明も異なり、OpenAIの論文はスパースなパリティ検査と多項式補間、Anthropicの論文はテンソルネットワークの縮約を用いている。

検証は誰がどうやるのか

OpenAIは今回、ETHを含む3件の結果を同時に発表し、それぞれ外部の専門家に取りまとめ役（shepherd）を頼んで公開方針も分けた。

分野	結果	公開のしかた
数学	局所平滑化予想を全次元で証明し、掛谷予想とSteinの制限予想も導く	AIの出力をそのまま公開し、研究者が各自で検証する
計算機科学	ETHの反証	外部の研究者グループが解説を担当し、AIの出力も即時公開
物理	QCDと標準模型の統一的な拡張が4次元で存在することの証明	外部グループに任せ、AIの出力は当面公開しない

ETHの検証グループは、UCサンディエゴのRussell Impagliazzo氏とRamamohan Paturi氏、MITのRyan Williams氏が率いている。Impagliazzo氏とPaturi氏は、Francis Zane氏とともにETHを提唱した研究者本人たちだ。Williams氏はETHを強めた各種の仮説（SETHなど）を否定してきた研究者で、OpenAIの論文も2016年に同氏がMerlin–Arthur版のSETHを否定したことに触れている。

外部との協力には4つの原則が掲げられている。参加者は秘密保持契約（NDA）を結ばなくてよく途中の成果も自由に話せること、OpenAIは学術上のクレジットを求めないこと、参加は任意かつ無報酬で、参加者の結論は本人の見解でありOpenAIを代弁しないことだ。

Williams氏はXで、この件を「claimed refutation」（反証の主張）と呼んだ。続く投稿では、秘密保持契約も報酬もないため途中の発見を自由に共有できること、PDFやLeanソースを含むETHの生データをすぐに公開するようOpenAIに求めたこと、影響を受ける研究コミュニティのための会議への資金提供も求め、OpenAIが両方に同意したという。OpenAIの発表では「会議への資金提供を約束した」と書かれており、金額や全額負担かどうかには触れていない。

3人が研究者向けに出した公開書簡には、「Our involvement should not be taken as certification of the claim.」（自分たちの関与を主張の正しさのお墨付きと受け取らないでほしい）という一文がある。3人は書簡で、証明をどう分担して確かめるか、AIが出した結果の早期アクセスやクレジットの扱いをどうするか、という2つの議論を呼びかけている。書簡末尾の資料一覧には、OpenAIの資料とともにAnthropicの反証へのリンクも貼られている。

Leanで通ったのに検証がいる理由

Leanは、定義と定理の文を書くと、証明がその文を本当に導いているかを自動で確かめる証明支援系だ。ただし機械が確かめるのは「書かれた文が証明された」ことにとどまり、その文が論文の主張やETHそのものを正しく表しているかは人が読んで確かめる必要がある。
Anthropicの README はこの点を明記しており、主張を書いたファイル MainResults.lean はMathlib以外を読み込まず短くしてあり、論文との違いは付録Eに列挙したので読者が自分で照合する構成になっている。

両社とも、Leanの開発組織が公開している Comparator という仕組みで検証の条件を固定している。主張だけを書いた「チャレンジ」ファイルと証明のファイルを分け、証明済みの定理の文がチャレンジと一致するか、使ってよい公理が決めた範囲に限定されているかを確かめる。Leanでは新しい公理を勝手に宣言すれば偽の命題でも証明できてしまうため、標準の数学的公理系から外れないよう縛る必要がある。両社の設定で許されている公理は、Leanの標準的な propext、Quot.sound、Classical.choice の3つだけだ。都合のよい公理を持ち込む不正は、これで防げる。
Anthropicはさらに、独立に書かれた別の検証カーネル nanoda でも証明を検査している（OpenAIの設定では標準カーネルを使い nanoda は無効になっていた）。ここではどちらのLeanプロジェクトもビルドしておらず、リポジトリの記述と設定ファイルを確認した。

ETHをLeanでどう書いたかも両社で異なる。
Anthropicは $s_3$ を定義して ETH : Prop := 0 < s 3 と書き、その否定 ETHIsFalse を定理として証明した（計算モデルはMathlibのチューリング機械）。
OpenAIのチャレンジ SubexponentialSAT.lean は、「1台の機械がどんな $k$ -CNFでも解の個数を正しく出力し、決めた時間と多項式個のテープセル（記憶領域）で止まる」という定理の形で書いており、ETHの否定はこの定理から導かれる。

Lean版の上界と論文版との差

OpenAIのリポジトリの形式化の範囲の説明によると、Leanで証明されたのは次の上界だ（ $L$ は入力の符号化のビット長）。

(L+1)^{O_k(1)} \, 2^{O_k(n (\log\log n)^2 / \sqrt{\log n})}

論文の一般の場合と比べると、 $\log\log n$ が1乗から2乗に強まっている。論文の本文も、有理関数による補間の議論では指数部が $n(\log\log n)^2/\sqrt{\log n}$ になり、より良い2つの上界は付録のテンソル縮約で示すと書いている。
この形でも指数部を $n$ で割れば0に収束するため、Lean版だけでもETHを否定できる。論文の主張どおりの細かい上界は、少なくともETHの部分についてはLeanでは形式化されていない。

正しかった場合の影響

両社の論文と報道から、影響の範囲を整理した。

対象	結果が正しい場合	根拠
ETH	否定される	両論文
SETH（強指数時間仮説）	否定される	SETHはETHを前提とするため、ETHが偽ならSETHも偽
#ETH、Gap-ETH、NSETH	否定される	OpenAI論文（Gap-ETHは近似版、NSETHは非決定性版）
直交ベクトル仮説	否定されない	Anthropic論文（内積0のペアの有無を判定する問題）
P≠NP予想	解決しない	両論文
NP完全問題一般	$2^{o(n)}$ で解けるとは限らない	OpenAI論文
実用のSATソルバー	速くならない	Anthropic論文、OpenAI発表
暗号	直接の影響はない	TechCrunchの報道

SETHは「 $k$ を大きくすると $k$ -SATは $2^{(1-\varepsilon)n}$ より速く解けない」という、ETHより強い予想だ。強い予想は弱い予想を含むので、ETHが偽ならSETHも偽になる。
一方で、多くの下界の導出が前提にしている直交ベクトル仮説は、SETHから導かれる側の仮説で、今回の結果では否定されないとAnthropicの論文は書いている。同論文によると、ETHかそれを含意する仮説だけを前提に結果を示した論文が800本以上あるという。

NP完全問題同士は多項式時間で相互に変換できるが、OpenAIの論文は、 $2^{o(n)}$ という計算時間は一般の多項式時間の変換では保たれないと注意している。変換で変数の数が $n^2$ 個に増えると、 $2^{o(n^2)}$ は $2^{o(n)}$ の形を保てないからだ。そのため、すべてのNP完全問題が指数時間を下回るわけではない。グラフの彩色数や完全マッチングの数え上げのように、変数の数がほとんど増えない変換で3-SATに直せる問題には、 $2^{o(n)}$ のアルゴリズムが得られると論文は書いている。

暗号について、Williams氏はTechCrunchの取材に、アルゴリズムの改良で特定の鍵長の暗号が破れたとみなされる可能性はあると答えた。そのうえでOpenAIのDan Roberts氏に影響を尋ねたところ、OpenAIは調査の結果、暗号が破れることにはならないと自信を持っていたという。RSA暗号は素因数分解の難しさに依存しており、素因数分解はNP完全ではない別の問題で、一般数体篩という専用の準指数時間アルゴリズムが以前から知られている（過去にRSA-260の分解の記事で計算規模を調べた）。Williams氏は同じ取材で、計算機科学者は皆P=NPの可能性をもう少し真剣に見積もり直すべきだろうとも話し、OpenAIのアルゴリズムが到達できる最良のものだとは思わないと述べている。

同時に発表された残りの2件

数学の結果は、Sogge氏が1991年に提起した局所平滑化予想（調和解析の未解決問題）を全次元で証明したというもので、波が一点に集中してもその集中は一瞬しか続かないという内容だ。正しければ掛谷予想とSteinの制限予想が導かれる。2次元はGuth・Wang・Zhangが2019年に、掛谷予想の3次元はWang・Zahlが2025年に証明していた。こちらは論文とLean証明がリポジトリで公開されている。

物理の結果は、4次元でゲージ場とフェルミオン（物質を構成する素粒子）を含む相互作用のある量子場理論が数学的に厳密に存在することの証明だ。QCDと、標準模型を含む大統一理論が対象で、途中で純粋ヤン・ミルズ理論の存在も示しているという。ヤン・ミルズ理論の存在はミレニアム懸賞問題の一部にあたる。David Gross氏が率いるグループが取りまとめて自分たちで書き直す方針となり、AIの出力は公開されていない。この件はまだ原典のテキストが確認できる状態になっていない。

回ってきた説明と原典の差

最初に出てきたChatGPTの説明は、OpenAIの発表と論文の大筋とは合っていた。日付（10月16日に反証、10月17日にLean、10月26日に発表）、検証グループの3人、秘密保持契約なし・無報酬、Lean版の上界が論文より弱いこと、P≠NPが解決しないことは原典どおりだった。原典と照らして違っていた点や、説明になかった内容は次のとおりだ。

説明の記述	原典で確かめた内容
計算量は概ね $2^{O(n/\sqrt{\log n})}$	この形は節の数が $m \le Dn$ の場合。一般には $2^{O(n\log\log n/\sqrt{\log n})}$
ETHは「指数時間より本質的に速く解けない」という予想	正確には、ある $\delta > 0$ について $O(2^{\delta n})$ では解けないという予想（ $s_3 > 0$ ）。既存の $1.307^n$ も指数時間に入る
会議のスポンサーを全額持つ（元のポスト）	OpenAIは会議への資金提供を約束したとだけ書いている
SATソルバーの実用上の高速化は未確定	Anthropicは自分たちの上界が $n > 10^{10000}$ まで全探索の計算時間を下回らないと計算し、実用には現れないと明記している
（元のポストやChatGPTでは言及なし）	Anthropicも数時間後に同じ計算量の反証とLean証明を公開し、10月16日に見つけたとしている
（元のポストやChatGPTでは言及なし）	Lean検証は両社ともComparatorで公理を標準の3つに制限している