OpenAI と Anthropic が同じ日に、それぞれ別に指数時間仮説（ETH）を反証したと発表した。ETH は、3-SAT のような問題は入力の大きさについて指数より速くは解けない、という計算量の理論の仮説である。多くの「これ以上は速くならない」という結果の土台になってきた。反証が正しければ、計算量の理論の地図が大きく描き変わる。
ただし、いまの時点で確かなのは「主張が出た」ことまでだ。2社とも証明を Lean で検査したとしているが、人間で中身を確かめた人はまだいない。OpenAI は検証を外部の研究者に任せる。同じ公開に含まれる物理の結果は、原稿を委員会に書き直させるという。この結果をどう受け止めるかは、こうした検証の進め方で決まることになる。
同じ日に、2つのラボから別々に
OpenAI は、数学の成果を置いている github.com/openai/math と、その更新履歴で結果を示した（一次情報）。Anthropic の側は、同じ日に Claude が独立に ETH を反証したと伝えられている（OfficeChai）。Anthropic の数学者 Levent Alpöge は X に投稿した。AI の助けで得た結果を集める Hexagon にも、関連する原稿 2610.00577v1 が載っている。
報道は10月27日に出そろった。TechCrunch は「フロンティアのラボが ETH を反証したと言う。それは何を意味するのか」と題した解説を出した。Scientific American は、2社の証明が並んだことに科学者たちが驚いていると報じた。
同じ日に別々に、という点には2通りの読み方がある。2つの独立した系統が同じ結論に着いたのなら、正しさを支える状況証拠になる。一方で、どちらも人間がまだ読み切っていない以上、2本あることは検証を2倍に増やすだけだ、とも言える。どちらの読み方が当たっているかは、人間が証明を読んで初めて分かる。
Lean が保証するもの、しないもの
2社とも Lean での検査を済ませている。これは、10月6日の OpenAI の大量公開（Lean で形式化してあったのは約42%）と比べれば、一段強い出し方である。証明の手順に飛ばしや誤りがあれば、Lean のカーネルが通さない。
それでも、Lean が保証するのは「形式化した命題が、形式化した前提から導ける」ことまでだ。その命題が本当に ETH を書き表しているのか、計算のモデルや「指数より速い」の定義を取り違えていないのかは、Lean は答えない。計算量の理論の命題は、形式化のときに定義がずれやすい種類のものである。Thomas Hales が10月9日に Tao のブログで指摘したとおり、Lean のカーネル自体にも、この夏に健全性の不具合が続いた。「Lean で通った」は検証の終わりではなく、人間の検証を始めるための前提にすぎない。
OpenAI は検証を外に出し、物理は委員会に書き直させる
OpenAI は、ETH の結果の検証を外部の研究者に任せるとしている。同じ公開の中の物理の結果は、委員会に原稿を書き直させる。Scientific American はこの物理の結果を、OpenAI が100万ドルの懸賞がかかった量子の数学の問題で、人間の研究者を出し抜いた件として伝えている。
このやり方は、直前に出た批判と並べて読む必要がある。10月25日、数学と AI の助言グループ（AGMAI）は Tao のブログで、ラボが自分で選んだ数学者に AI の成果を確かめさせて発表させるやり方に反対した。確かめる材料に触れられる時期が人によって不公平になる、誰が確かめるかを数学の共同体が決められなくなる、選ばれた数学者の評判を借りて会社が批判から守られる、という理由である。
外部の研究者に任せるのは、この批判に沿う方向に見える。しかし、外部の研究者を誰がどう選ぶのか、材料がいつ誰に開かれるのかが示されなければ、批判された問題はそのまま残る。物理の結果を委員会に書き直させる場合も同じで、委員会の顔ぶれと、書き直した原稿をどう公開するかが問われる。
OpenAI の数学には、検証が追いつかなかった前例がある
OpenAI が10月6日に出した原稿は、公開の翌日に符号の誤りで3本を取り下げ、719本になった。数学者たちは原稿を書き直す拠点 oai-math-revised を立ち上げた。そこでは先行研究をきちんと引いたかをめぐる異議が出て、さらに1本が外れた。検証を終えた本数の集計は、今もない。成果を出した数学のモデルの名前も、明かされていない。
今回の ETH の主張は、この流れの上にある。数を出すことより、1本の結果を共同体がどう確かめるかが問われる局面に移った。しかも今回は、比べられるもう1本の証明が Anthropic から出ている。2本の証明が同じ道筋なのか、まったく違う方法なのかも、人間が読むまでは分からない。
次に見るべきこと
見るべき点は3つある。第一に、Lean の形式化した命題そのものを、計算量の理論の専門家が公に読んで、ETH を正しく書き表していると認めるか。第二に、OpenAI が外部の検証者をどう選び、材料をどこまで公開するか。物理の委員会の顔ぶれもこれに入る。第三に、Anthropic が同じ水準で材料を出し、2本の証明を突き合わせられるようにするか。
どちらかの証明に人間の検証が通るまで、この件は「計算量の理論が覆った」ではなく、「2つのラボがそう主張し、機械の検査は済んだ」として扱うのが正確である。
