OpenAI、AIシステムがLeanで形式化されたナビエ–ストークス反証を生成したと主張
OpenAIは、社内AIシステムがナビエ–ストークス方程式の有限時間特異点を見つけたと述べるが、独立した数学者による検証は依然として不可欠だという。
OpenAIは、社内AIシステムが三次元の非圧縮性流体運動に有限時間特異点が生じうることを示す解析的証明を作成し、ナビエ–ストークスの存在と滑らかさの問題に取り組んだと述べている。同社は文書化された論証とLeanでの形式化を公開したが、入手可能な証拠だけではその主張は独立に検証されていない。
この発表が重要なのは、ナビエ–ストークス問題が7つのミレニアム懸賞問題の一つであり、2000年にClay Mathematics Instituteによって特定された数学的難問群だからだ。正しい解決は、自動化された数学研究の限界だけでなく、人間の研究者が何十年も解けなかった問題に対してAIシステムをどのように試験するかにも影響を与える。
OpenAIの投稿が、この報道の主な情報源である。付随する配信記事には、利用可能な資料内に追加の本文は含まれていないため、システムの性能、規模、結果に関する最も強い主張はベンダー報告によるものだ。
OpenAIが解決したと主張する内容
OpenAIは、同社のシステムが、滑らかで初期状態では静止している流体が、滑らかな外力を受けつつ有限エネルギーを保ったまま、有限時間で特異点を形成する問題設定を確立したと述べている。同社の説明では、この結果はナビエ–ストークス問題の公式な定式化における「C」と「D」の命題を証明するものであり、すべての解が正則なままであることを証明するのではなく、普遍的な滑らかさを否定することに相当する。
提案されているメカニズムは、渦が内側へ螺旋を描きながら軸方向に引き伸ばされるというものだ。中心領域が収縮するにつれ、数学モデル内で流体速度は無限に増大する。OpenAIによれば、この構成は、加速度、圧力、運動量移送、粘性の各項が大きくなりながら、精密に相殺し合うことに依存している。外力は滑らかなままであるため、主張されている破綻は無限大の力を直接加えたものではなく、流体力学そのものによって生じる。
ナビエ–ストークス方程式は、ニュートンの運動法則を用いて流体を連続体としてモデル化する。エンジニアや科学者は、航空機設計、天気予報、血流解析などでこれを利用している。未解決の問題は、一定密度の滑らかな三次元非圧縮性流れが、あらゆる時刻で滑らかであり続けなければならないのかという点だ。
大規模なマルチエージェント実験
OpenAIによれば、この作業は、2つのミレニアム懸賞問題が解決されたという噂を同社が耳にした9月1日に始まった。その後、AIエージェントを調整するシステムに、すべての未解決問題と関連するいくつかの問いを調査させた。
同社は、ナビエ–ストークスの取り組みにおよそ1万体の同時実行エージェントが関与したと述べている。これらのエージェントはグループに分けられ、異なる問題設定を与えられ、キャッシュされたインターネット版やコード実行を含むツールの利用を許可された。OpenAIは、最も有望な作業を統合する前に、証明と反証の両方の変種を探ったと述べている。
OpenAIは、より広いプロジェクトで490万件のメッセージが生成され、約3000億の出力トークンが使用されたとも報告している。ナビエ–ストークスの取り組みだけに限ると、270万件のメッセージと約1300億の出力トークンが使われたという。これらの数値は同社の内部実験を示すものであり、有用な数学的推論の独立監査済み指標ではない。
同社によれば、エージェントは約88時間の作業の末、9月5日にナビエ–ストークスの結果に到達した。Leanによる形式化と検証には、OpenAIによればGPT-6 Astraを通じてさらに17時間かかった。同社は、探索中に異なるエージェント群の洞察を統合するためにCodexを使用したとしている。
形式検証は証拠であり、最終的な承認ではない
Leanの成果物は、形式化によって、従来の研究草稿では見過ごされうる仮定の欠落や無効な手順を明らかにできるため、OpenAIの開示において重要な要素である。しかし、それだけで、形式化された主張が公式のミレニアム懸賞問題の定式化と正しく一致しているか、または実装に定義、導入された補題、仮定の誤りがあるかは決着しない。
OpenAIは証明の記述とLean形式化を公開したが、提供された証拠にはClay Mathematics Instituteや独立した数学者によるレビューは含まれていない。同社は、この結果でミレニアム賞を主張する意図はないと明言している。その違いは重要だ。公開されたAI生成証明は研究上の主張であり、賞の認定には専門家による精査と、研究所の規則に基づく承認が必要になる。
時期の問題も慎重な帰属を必要とする。OpenAIは、Anthropicの従業員であるLevent Alpögeと、ニューヨーク大学の数学教授Tristan Buckmasterに関連する噂を耳にした後に作業を始めたと述べている。同社は、彼らの作業は同じナビエ–ストークスの結果ではなく強制Eulerに関するものであり、両者は方法と正確な結論の両方で異なっていたと述べている。OpenAIは、公開前に彼らの特定のユーザーデータや作業へアクセスしていないとしつつ、匿名化された製品データがモデル改善に寄与した可能性を排除できないとも認めている。
この結果がAI開発者にとって意味しうること
AI開発者にとって注目すべき変化は、単にモデルが数学テキストを生成したということではない。OpenAIは、多数のエージェントが独立に定式化を探り、中間結果を交換し、ソフトウェアツールを使い、候補証明を形式検証システムに渡すワークフローを説明している。これは単一のチャットボット応答というより、自動化された研究パイプラインに近い。
このアプローチは、そのコストと運用リスクも浮き彫りにする。何千もの同時エージェントと何千億もの生成トークンは、価値の高い研究ベンチマークでは実用的かもしれないが、通常のソフトウェア製品の経済性とは大きく異なる。開発者は、並列探索が本当に新しい洞察を生むのか、それとももっともらしいが重複した推論の量を増やしているだけなのかを測定する必要がある。
企業の購入者にとって、この出来事は、モデルが結果を提案できることと、組織がそれを信頼できることの違いを再認識させる。科学や工学のワークフローでは、再現可能な成果物、機械検証可能な証明、専門家レビュー、明確な仮定の記録が、ベンチマークスコアやエージェント実行の規模より重要だ。Lean形式化はそのプロセスを支援しうるが、ドメイン知識の必要性をなくすものではない。
この発表は競争上のシグナルでもある。OpenAIは、社内モデルがGPT-6 Astraより高性能で、訓練はまだ継続中だと述べている。これらの能力比較はOpenAIによるものなので、確定した市場指標ではなく、社内またはベンダー報告の主張として扱うべきだ。
今後注目すべき点
最初のシグナルは、公表された証明とLeanコードの独立した検証であり、とりわけその構成が公式なナビエ–ストークスの記述にあるすべての条件を満たしているかどうかだ。微妙に異なる定義域、外力条件、あるいは特異点の概念に依存する形式証明では、同じ問題は解決されない。
次の注目点は、数学者が結果を再現し、欠落部分を見つけるか、あるいは形式化がコンパイルし議論を忠実に符号化していることを確認するかどうかだ。Clay Mathematics Instituteの反応も、この作業が認定基準を満たすかを明確にする。
研究者はまた、OpenAIがモデルのバージョン、プロンプト、ツールの境界、計算資源の حسابを含め、マルチエージェント探索を再現できるだけの実装詳細を公開するかどうかにも注目すべきだ。そうした情報がなければ、報告されたエージェント数やトークン総数は文脈を与えるにとどまり、同様のシステムを構築するチームにとっての指針は限られる。
Creati.ai の視点
OpenAIの発表は、まだ確定した数学的事実ではなく、重要な能力の主張として理解するのが最も適切だ。エージェントの協調、コードツール、Lean形式化の組み合わせは、AI支援研究の有望な方向性だが、中心的な結果はなお、それを生み出した会社の外部での精査に依存している。
開発者にとっての実務的な教訓は、見出しよりも狭く、しかし有用だ。高度なAI研究システムには、検証層、明示的な問題仕様、独立したレビューが必要である。もし今回の結果の周囲でそうした管理が機能するなら、この出来事は機械支援数学の重要な事例研究になるかもしれない。そうでなければ、流暢な証明や形式的に見える成果物が数学的検証の代わりにはならない理由を示すことになる。
