指数時間仮説は OpenAI のモデルに反証されたのか？

10月26日、OpenAI はリポジトリ openai/math で論文「The Exponential Time Hypothesis is False」を公開しました。論文によると、名前の明かされていない OpenAI の社内モデルが、計算量理論の基本的な前提の一つである指数時間仮説（ETH）を反証したとのことです。この論文と Lean による形式化は、仮説の共同提唱者 2 人を含む独立した計算機科学者のグループが検証しています。

指数時間仮説とは？

ETH（Exponential Time Hypothesis）は、3-SAT 問題、つまり 3 変数の節からなる論理式を充足できるかどうかを判定する問題は、n 変数に対して 2^Ω(n) より速くは解けない、という仮説です。簡単に言えば、変数が 1 つ増えるごとに時間は指数的に増え、どんなに巧妙なアルゴリズムでもそれは変えられない、ということです。

この仮説を提唱したのは Russell Impagliazzo と Ramamohan Paturi（Francis Zane と共同）です。ETH の上には、グラフ、データベース、計算生物学などのある問題が「これ以上速くは解けない」ことを示す何百もの論文が成り立っています（The Next Web が指摘するとおり）。

OpenAI のモデルは具体的に何を証明したのか？

論文は、固定された任意の k ≥ 2 について、k-CNF 式の充足割り当てをすべて正確に数える決定的アルゴリズムを示しています。多項式空間で動作し、時間は (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 の反証とされるものを生み出したと書いています。

研究者たちは NDA に署名しておらず、報酬も受け取っていません（The Next Web による）。彼らは OpenAI に生データをすべて公開し、結果の影響を議論する会議に資金を出すよう求め、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 によると、モデルには約 4,000 の未解決問題が与えられ、1 つの結果あたり平均で ChatGPT Pro レベルの「思考」3 時間が費やされました。

新しいのは、10月26日に OpenAI が 3 つの結果を同時に発表し、それぞれに異なる道を選んだことです（Unite.AI が説明しています）。

1. ETH：論文と Lean の証明は公開済みで、Impagliazzo、Paturi、Williams のオープンなグループが検証しています。
2. 全次元での Sogge の「local smoothing」予想：OpenAI によると、ここから掛谷予想と Stein の制限予想が導かれます。こちらも Lean の証明付きで公開されました。
3. 4 次元における Yang-Mills 理論と QCD の存在（クレイ研究所のミレニアム懸賞問題の一つ）：資料はまだありません。ノーベル賞受賞者 David Gross が率いるグループが、自ら結果をまとめることにしました。

さらに OpenAI は、モデルの発見に対する科学的な功績は求めないと表明しています。称賛は、それを理解し記述する人々に与えられるべきだという立場です。また、AI が生み出した結果に関するワークショップや会議のために、Simons Foundation に 500 万ドルを寄付しました。

注意すべき点は？

第一に、検証の状況です。Lean による形式化は強いシグナルですが、Lean で書かれた定理が本当に論文の本文と同じことを述べているかは、常に確認が必要です。OpenAI 自身も README で、形式化されていない結果の一部には誤りが含まれうると書いており、10月7日には証明の一つに符号の誤りがあったため 3 本の論文を取り下げました。グループが作業を終えるまでは、この結果を慎重に受け止めましょう。

第二に、この結果が意味しないことです。著者らは、すべての NP 問題に準指数時間アルゴリズムがあるということにはならないと明記しています。つまり、これは P vs NP 問題の解決ではなく、実行時間は依然としてどんな多項式よりも速く増加します。

第三に、スピードです。理論家たちが 20 年以上取り組んできた結果を、モデルは社内評価の一環で見つけたとされています。もし確認されれば、AI が理論計算機科学で自律的に発見を行った、おそらくこれまでで最も強い例になるでしょう。ついでに、Claude による形式検証の記事で書いた形式的証明の話題も再び注目されています。

よくある質問

指数時間仮説とは何ですか？

計算量理論において、3-SAT は n 変数に対して 2^Ω(n) より短い時間では解けないとする仮説です。Impagliazzo と Paturi が Francis Zane とともに提唱しました。

OpenAI は P vs NP 問題を解いたのですか？

いいえ。アルゴリズムは準指数時間ですが多項式時間ではなく、著者らはこの結果がすべての NP 問題に当てはまるわけではないと指摘しています。

ETH の反証はすでに確認されたのですか？

まだです。Lean による形式化はありますが、Impagliazzo、Paturi、Williams の独立したグループが検証を始めたばかりで、関与は確認を意味しないと断っています。

どの OpenAI モデルがこれを行ったのですか？

名前の明かされていない社内モデルです。リポジトリの README でも OpenAI はその名前を挙げていません。