30年来の未解決予想、中国のモデル、そして機械検証された証明

30年来の未解決予想、中国のモデル、そして機械検証された証明

10月15日、Shanghai AI Laboratory（上海人工智能実験室）は、研究チームが Ghys 予想の三次元の場合を証明したと発表した。これは1995年から未解決のままだった力学系における未解決問題である。研究は同実験室の自社モデル Intern-S2 を用いて進められ、完成した証明は Peking University（北京大学）のチームによって Lean 上で形式的に検証された。

重要なのは、難問が一つ解けたというだけではない。今回の発表が、ある種の数値ではなくプロセスを軸に組み立てられている点だ。モデルが導出を生み、研究者がどの攻め筋に注意を注ぐかを決め、証明支援系があらゆる段階を検証する。この組み合わせこそ業界が2年間約束してきたものであり、ここにきて論文まで付いた。

この予想が問うていること

Étienne Ghys がこの問題を提示したのは1995年である。大まかに言えば、カオス的な力学系の振る舞いがその幾何学的分類を決められるか、言い換えれば、運動がその運動の起きている空間の形を教えてくれるか、という問いである。

解けたのは一般の場合ではない。チームが証明したのは余次元1の場合、すなわち三次元の設定であり、これは30年間未解決のままだった。この区別は主張を誠実に読むうえで重要だ。予想全体はより広いままだが、これまで誰も突破できなかった特定の場合については決着した。

最初の試行で400ページが出た

共同作業の仕組みは結果よりも興味深い。人間とAIの研究が一分単位で実際にどう進むかを示しているからだ。

Intern-S2 がこの問題を最初に探索したとき、約400ページの導出レポートを生み出した。それは答えではない。候補となる推論の山であり、有用なものもあればそうでないものもある。既知のことを想起させるのではなく、本当に未解決の問題を考えさせるようにモデルに求めたときに得られるのは、まさにこういう形の出力である。

そこから、作業は7ラウンドの継続的推論を経た。問題グラフ、すなわち部分命題とそれらが互いにどう依存するかの地図は、15ノードから389ノードへと成長した。蓄積された出力は約1000ページに達し、数十の異なるアプローチを含んでいた。各段階で数学者たちは、モデルにはできないことを行った。提案を見て、どの突破口が有望かを判断し、次のラウンドを方向づけたのだ。

この判断を提供したのは、実験室の客員研究員で Greater Bay University の教授である Xu Disheng と、博士課程の頃からこの予想を追い続けてきたポスドク研究者 Zhang Jiesong である。Zhang の論文は9月29日に arXiv に投稿され、10月13日に改訂された。単著であり、AI 利用の申告が付されている。モデルは複数ラウンドの対話を通じてアイデアと論証の発展を助け、数学的な部分は本人が独立に検証した、という内容である。

これを単なる物語以上にする部分

AI が数学を解いたという主張は安い。今回に重みがあるのは、証明が形式化されたからだ。

Bin Dong と Ruochuan Liu が率いる Peking University のチームは、自社の SHEAF フレームワークを用いて、4つの主要定理と、その論証が依存する Ghys による補助的結果をすべて形式化した。形式化とは、定義・仮定・推論をコンピュータが検査できる言語に翻訳することであり、書き手の論証のあらゆる段階を、訓練された読者に補わせるのではなく明示的に書き出さなければならない。

この作業には約5日かかり、最大100のエージェントが並行して働き、約55万行の Lean コードを生み出した。Lean は対話型定理証明器である。誰がどれほど自信があるかは気にしない。論理を検査し、証明を受け入れるか、受け入れないかのどちらかである。

SHEAF はタスクを定義・命題・依存関係からなる有向グラフとして整理し、別々のエージェントがつながった部分を担当できるようにし、どの命題に証明があり、どれがまだ必要かをチームが追跡できるようにした。これは真に新しい種類の分業であり、このフレームワークは既存の力学系の形式化ライブラリの穴も埋めなければならなかった。この証明に必要な道具立てが、当時はそもそも存在しなかったからである。

人とモデル、それぞれ別の仕事

実験室が説明するこの分業は額面どおり受け取る価値がある。どちらの側にとってもお世辞にならない形だからだ。

モデルは文献を洗い、命題を細かく分解し、証明の分岐を並行して探索し、論理的な段階を検査し、大量のアイデアを素早く試した。人間は方向を定め、どのアプローチを追う価値があるかを判断し、次のラウンドの労力をどこに振るかを決める裁定を下した。

どちらの半分も似ていない。モデルの貢献は規模とスタミナである。何十もの袋小路を記憶に保持しても、意欲を失わない。人間の貢献はセンスであり、100ページの一見もっともらしい推論を見て、どの3段落が重要かを知る能力である。

中国のメディアが大きく取り上げた逸話も付いている。国内モデルが解いたと聞いた力学系の専門家が、好奇心から同じ問題を GPT-6 に投げたところ、到達できなかったという。狭く読めば、これは一つの問題における二つのシステムの比較にすぎず、ほとんど何も証明しない。競争力学についてのシグナルとして読めば、投資を動かす類の細部である。

なぜ形式的検証が賭け金を変えるのか

この2年のほとんどにおいて、AI 支援数学のボトルネックは候補となる論証の生成ではなかった。モデルはもっともらしい推論を生み出すのが得意である。ボトルネックは、そのどれが正しいかを知ることだった。証明の検査は遅く、専門家を要し、並列化しにくいからだ。

Lean はこれを反転させる。ある命題が形式化されてしまえば、検証は安く速く、しかも信頼できる。社会的なものでなく機械的なものだからだ。55万行が高くつく部分であり、チームと100のエージェントが5日でそれを生み出せたことが、ここでの真の前進である。生成側のボトルネックがすでに緩んでいたのと同じように、検証側のボトルネックも緩みつつあることを示唆している。

実験室は、このワークフローを自社の科学発見プラットフォーム上で再利用可能な数学検証モジュールとしてパッケージし、モデル、エージェント、データ、実験装置をつなぐと述べている。また、Wuhan University（武漢大学）のチームがこのプラットフォームを使って電気化学合成の開発サイクルを5年から10年から、1年から2年に短縮した、という以前の成果にも言及している。

ここから何を読み取るか

正直な要約はこうだ。これは本物の結果であり、本物の証明を伴い、それを生み出したワークフローは依然として非常に人手に依存している。7ラウンドの専門家による舵取りは、モデルが独力で走っていることではない。AI 利用の申告付きの単著論文は、モデルが功績を主張していることではない。

変わったのは、ループが閉じたことだ。モデルは誰も解いていない問題で意味を持つだけの推論を生み出せる。人間はそれを導ける。そして証明支援系は、誰かが要約を信じる必要なく結果を認証できる。これはパイプラインであり、デモではない。そしてケイパビリティを実践に変えるのはパイプラインである。

次の問いは、これが形式化がそもそも可能な場合を超えて一般化するかどうかである。幾何と力学系には、機械検査に向いた構造がいくつかある。科学の残りの多くにはそれがない。そして AI が研究助手としての約束を本当に試されるのは、生物学、材料、医学といった、より乱雑な領域においてである。Ghys の結果は、この道具が機能しうると告げている。どれほど頻繁に機能するかは、まだ告げていない。