10月13日、Scientific Americanが「OpenAI's blockbuster Navier-Stokes proof isn't what we thought it was」と題した記事を公開した。OpenAIのAIが成し遂げたとされるナビエ=ストークス問題の証明が、当初の説明とはまったく異なるアプローチに基づくものだったこと、そしてOpenAI自身もその実態を把握できていなかったことが、専門家の精査により明らかになった経緯を報じている。
ミレニアム問題の「証明」が揺れている
9月初旬、OpenAIは166ページの論文を公開し、数学史上最も難解な未解決問題の一つであるナビエ=ストークス問題に解答を与えたと発表した。ナビエ=ストークス方程式とは、水や空気をはじめとするあらゆる流体の動きを記述する方程式であり、クレイ数学研究所が懸賞金100万ドルをかけた「ミレニアム問題」の一つに指定されている。問題の核心は「滑らかな初期条件から始まった流体の解が、有限時間内に滑らかさを保ち続けるかどうか(存在と滑らかさ)」を証明することにあり、70年以上にわたって未解決のままだった。発表当時、この成果は数学界に衝撃を与えた。
しかしその後、複数の専門家グループが論文を精査した結果、証明のアプローチが当初の説明とはまったく異なっていたことが判明した。さらに深刻なことに、OpenAI自身も自社モデルがどのように証明を構築したかを正確に理解していなかったことが明らかになっている。
「スペイン・プログラム」を使ったと言っていたが、実際は違った
OpenAIが公開当初に示した説明では、この証明はスペイン人数学者のDiego CórdobaとLuis Martínez-Zoroaが考案したアプローチ(研究者の間では「スペイン・プログラム」と呼ばれる)に基づくものとされていた。スペイン・プログラムは、流体の速度が理論上「無限大」に達してしまう状況(「ブローアップ」と呼ばれる)を人工的に構築することで、滑らかな解が有限時間で崩壊する——つまり「存在と滑らかさ」が成立しないことを示す戦略だ。
しかし、スイス連邦工科大学ローザンヌ校(EPFL)の数学者Gonzalo Cao-Laboraは「詳細を見ると、異なるアプローチだ」と述べた。OpenAIのモデルはブローアップ手法を採用していたものの、そこで用いられた「非物理的な力」の構築方法がスペイン・プログラムとはまったく別物だったのだ。
この混乱の背景には、LLMの「ブラックボックス」的性質がある。証明の論理は定理証明支援系(proof assistant)である**Lean**でコード化されており、各ステップの論理的正しさは機械的に検証できる。しかし、約1万体のエージェントが1300億トークン・88時間かけて構築した推論の全体像は、専門家たちが別のLLMを用いて解読を試みている段階だ。プリンストン高等研究所の数学者Camillo De Lellisは「明確に検証可能な数学的事実の問題ではなくなっている」と述べており、このエージェント群が実際にたどった推論は、おそらく永遠に完全には解明されないという見方もある。
公開前に起きていた「対立」
この誤認は、深刻な研究倫理上の争いも引き起こした。
ニューヨーク大学の数学者Tristan Buckmasterは、OpenAIの競合であるAnthropicの社員Levent Alpögeとともに、約1年かけてスペイン・プログラムの実装研究を進めていた。OpenAIのモデルによる発表はその研究と方向性が重なっており、両者は「自分たちの成果と同じ路線を踏み台にされた」と受け取った。
さらに、BuckmasterはOpenAIが発表前に「懐柔と圧力」によって疑惑を公表しないよう求めたと主張している(OpenAI側はこの主張を否定している)。Buckmasterは最終的に疑惑を公表し、非常に公開的な対立へと発展した。この騒動の根本的な原因は、OpenAIが自社モデルの証明内容を発表前に正確に把握できていなかった点にある。
AIが数学界に突きつけた根本的な問い
この一件が示す本質的な問題は、AIが生成した証明を人間が追いきれなくなりつつあるという現実だ。
OpenAIは先週、さらに約400件の数学的成果をまとめてコミュニティに公開した。記事によれば、その中の少なくとも十数件は、AI以前の時代であれば人間の数学者がフィールズ賞(4年に一度の国際数学者会議で授与される数学界最高の賞)を受賞できるレベルの成果だという。しかし、それを検証できる専門家の数はそのペースに到底追いつかない。
「証明は正しいのかもしれない。しかし、その正しさを人間が確かめる手段が失われつつある」——この状況は、「数学とは何か」「証明とは何か」という学問の根幹に関わる問いを投げかけている。
詳細はOpenAI's blockbuster Navier-Stokes proof isn't what we thought it wasを参照していただきたい。