DeepMind「AlphaProof Nexus」発表　未解決のエルデシュ問題9件を解決、推論コストは数百ドル

半世紀以上も誰も解けなかった数学の難問を攻略するには、かつてなら天才数学者が何年も研究室にこもり、膨大な論文と格闘する必要がありました。

今やそのプロセスは、数時間のマシン稼働と数百ドルの計算コストで片付く時代に入りつつあります。

Google DeepMind は 5 月 26 日、数学証明を自動生成・検証する AI「AlphaProof Nexus」の論文を発表しました。提示された 353 件の未解決数学問題のうち、組み合わせ論やグラフ理論にまたがる 9 件のエルデシュ問題を自律的に解決。そのうち 2 件は、1970 年に提示されてから 56 年間にわたり誰も解けなかった難問でした。

さらに同システムは、「オンライン整数列大辞典（OEIS）」に登録されていた 44 件の未解決予想もあわせて証明してみせました。

LLMと形式検証ツール「Lean」の反復ループ

AlphaProof Nexus の強みは、LLM にありがちな「ハルシネーション（幻覚）」を完全にシャットアウトした点にあります。

DeepMind は大規模言語モデルを、厳密な証明支援システムである「Lean」と直結させました。LLM が証明のコードを書き出し、Lean がコンパイラのように論理の破綻がないかを厳密にマシン検証します。

不合格ならフィードバックをもとに再生成を繰り返し、Lean の検証を完全にパスするまでループを回します。フルバージョンのエージェントには探索を最適化する進化アルゴリズムも組み込まれました。

簡易版のエージェントでも同様の結果は出せたものの、計算コストは大幅に跳ね上がったといいます。結果として、半世紀級の未解決問題を 1 問あたりわずか数百ドルの推論コストで解き明かすことに成功しました。

OpenAI への迅速なカウンター

今回の発表はタイミングも象徴的でした。

直前の週には、OpenAI が 80 年前のエルデシュ予想を反証したと発表したばかりでした。OpenAI は数か月前に「10 件の新規問題を解決した」という主張を撤回した経緯があったため、名誉挽回の勝利として話題を集めていました。

その直後に DeepMind が繰り出したのが、形式検証付きで 9 件をまとめて片付けたという今回の報告です。

ただし、万能というわけではありません。これまでにない全く新しい数学的概念や構造の構築を必要とする問題については、依然として手が出せない限界も明記されています。

なぜ重要か

私たちは、この成果が AI のフロンティアを「既存テストの点数稼ぎ」から「未知の科学的発見」へと決定的に押し進めたと評価しています。

これまで数学オリンピックの模試などで性能を誇示していたモデル競争は、すでに過去のものになりつつあります。正解が用意されていない本物の未解決問題に対し、数百ドルという現実的な予算で確定的な解を出せるようになった意義は大きいです。

数学者にとっても、AI は仕事を奪う敵ではなく、極めて実用的なリサーチ助手になります。人間が新しい仮説や方向性を提示し、気の遠くなるような証明の探索と検証を AI に任せるという協業スタイルが現実味を帯びてきました。

完全に新しい体系を作り出すような創造性にはまだ遠いものの、厳密な検証エンジンと組み合わせることで AI を真の学術研究の道具に仕立て上げた DeepMind のアプローチは、極めて堅実で賢い前進と言えます。