Google DeepMindの数学証明システムAlphaProof Nexusが、Science誌に正式に掲載された。論文の筆頭著者はTsoukalas氏で、研究チームは全員DeepMindの所属だ。この研究は5月末にプレプリントとして公開されており、今回は査読を経た学術誌版となる。
成果は変わらない。システムは未解決のエルデシュ問題353件に挑み、9件を解決した。うち2件は56年間未解決だった。整数列データベースOEISでは、未解決の予想492件のうち44件を証明した。さらに、代数幾何におけるHilbert関数をめぐる約15年来の問いに答え、min-max最適化の既知の上界も改善している。
1つのGemini、1つのLeanコンパイラ
システムの土台はGemini 3.1 Proだ。モデルが形式言語Leanで証明を起草し、Leanコンパイラが1ステップ変わるたびに検証して、エラーメッセージを次の試行にそのまま返す。この間、人間が結果を確認するのは最後だけである。
論文では4つのバージョンが区別されている。
- A版：最も素朴な「生成→検証」ループ。大規模モデルが書き、コンパイラが判定する。
- B版：Aに、DeepMindの従来の証明器AlphaProofを組み込み、証明に欠けた断片を補わせる。
- C版：進化的な仕組みを加え、複数のサブエージェントが証明の草稿プールを共有し、Eloスコアで順位付けする。
- D版：上記すべてを重ね合わせたもので、エルデシュ問題に挑むために使われた。
結果で最も興味深いのは、A版も9件のエルデシュ問題をすべて独力で証明したことだ。ただし最も難しい数件では、かかった費用が大きくなる。The Decoderが引用する推論コストは1問あたり数百ドルである。著者らは論文で次のように述べている。
"power of compiler feedback in grounding LLM reasoning"
（コンパイラのフィードバックは、大規模モデルの推論を地に足の着いたものにする力を持つ。）
スペイン研究者のいくつかの留保
スペインのScience Media Centreは、論文公開当日に現地の研究者数人からコメントを集めており、意見は二つに分かれた。
UAMの研究者Pablo Haya Coll氏は、この手法は意義のある数学的発見を体系的に生み出せると見ている。UOCのJosep Curto氏は「a dazzling display of technical capability marred by significant methodological inconsistencies」と評した。技術的には目を見張るが、方法論には明らかな不整合がある、という趣旨だ。同氏は3点を挙げた。A版とD版が同じ問題を解いたことは、フレームワークの複雑さが発見能力を左右するとは限らないことを示す。コストは成功した実行分しか計上されておらず、B版とD版の計算にはAlphaProof自体の推論コストも含まれていない。そしてLeanが保証するのは、証明が「書き下された命題」に対して成り立つことだけで、その命題が元の問題を忠実に翻訳しているかどうかは、依然として数学者の手作業による確認が必要である。論文自身も形式化の誤りが生じたことを認めている。
ICMATの所長Javier Aramayona氏が懸念するのは別の点だ。「正しいと分かっているが、誰も完全には理解していない」結果が大量に現れ始めることで、数学研究における理解のプロセスや、若手研究者の育成過程が弱まりかねないという。バリャドリッド大学のTeodoro Calonge氏はさらに率直で、この分野にはまだかなりの改善の余地があると述べた。
著者自身も適用範囲を明記している。エルデシュ問題におけるAIの全体的な成功率は約1〜2%で、解けたのは比較的易しい問題が中心だ。Mathlibライブラリの蓄積が厚く、問題をサブゴールに分解しやすい組合せ論、凸最適化、整数論に集中している。大量の新理論の創出を要する問題には、システムはほとんど手が届かない。
今年の出来事をつなげて見る
5月、本サイトはOpenAIのモデルが80年来のエルデシュ予想を攻略したと報じた。9月には、数学者とOpenAIの間で功績の帰属をめぐる争いが起きた。10月6日、OpenAIはGitHub上でAI生成の数学原稿722本を一度に公開した。方法は、学術誌を経由せず、Apache 2.0ライセンスのオープンソースリポジトリを使うものだった。The Decoderによれば、その後、テレンス・タオ氏が率いる数学者グループがこのやり方のボイコットを呼びかけた。
両社のやり方の違いは、ここにはっきりと表れている。OpenAIは量が多く公開された形を選び、ふるいにかける作業をコミュニティに委ねた。DeepMindは件数ははるかに少ないが、1件ごとにLeanコンパイラを通し、さらに学術誌の査読も通した。後者は論文中でLeanの位置づけも控えめで、形式検証は原文で "can serve as a filter for determining which proofs merit human review"、つまりどの証明が人間の検討に値するかを決めるためのフィルターだとしている。
ざっと計算してみよう。1問数百ドルなら、エルデシュ問題9件の推論費用は、ポスドク1人の1か月分の給与をはるかに下回る。ただしCurto氏が指摘する基準で、失敗した実行とAlphaProofの呼び出しを加えれば、帳簿上の額がどれだけ膨らむかについて、論文は現時点で数字を示していない。DeepMindは証明と一部の説明をGitHubのalphaproof-nexus-resultsリポジトリに置いており、外部の数学者が1件ずつ検証できる。
参考資料：Science誌掲載論文、The Decoder、CocoLoop、スペインScience Media Centreの専門家コメント。論文本文で、エルデシュ問題353件中9件の解決、OEIS予想492件中44件の証明、4つのエージェント版の役割分担を確認した。