GoogleのAI共同数学者：DeepMindのエージェント型数学ワークベンチ

2026年5月、Google DeepMindの研究者は、arXivのプレプリント「AI co-mathematician: Accelerating mathematicians with agentic AI」を公開し、発想、文献調査、計算、証明試行、理論構築を含む数学の作業サイクル全体をオーケストレーションするエージェント型AIワークベンチを紹介しました。

現在は限られた研究者にのみ提供されているAI共同数学者は、それ自体がソルバーやチャットボットではなく、非線形で雑多な数学のワークフローを統括する状態管理型のワークスペースです。並行する研究スレッドを管理し、不確実性を追跡し、失敗した試行も将来の参照のために保存します。出力はLaTeXで、数学・物理の研究分野で広く用いられる標準フォーマットです。

基盤はGemini 3.1です。現時点では、証明試行に内部的にGemini Deep Thinkを用い、計算的な探索にはPython実行と統合しています。現状では、DeepMindの専門的な数学エンジン（AlphaProof、AlphaEvolve、Aletheia）を内部コンポーネントとしては組み込んでいませんが、将来的に統合できる設計になっています。

AI共同数学者が重要な理由

数学者はLLMをさまざまな目的で活用しています。

• 文献レビュー
• 非形式的な証明スケッチ
• 定型的なLaTeX作成
• 探索的なコード作成

また、形式化証明支援系などのAIツールを使って、機械的な証明検証も行います。

ただし、それぞれのツールは全体のワークフローの特定部分では強力でも、結果をつなぎ合わせるのは数学者自身のアドホックな作業でした。これまで、数学者が用いる非線形プロセスを統合するインフラは存在していませんでした。

AI共同数学者の仕組み

このワークフローモデルは、Claude CodeやCodexといったAIコーディングツールから大まかに着想を得ています。しかし、ソフトウェアには仕様とテストスイートがありますが、数学研究は非線形です。最初は目標自体が曖昧だったり未定義だったりし、途中の発見が問いの枠組みを全く変えてしまうこともあります。

共同数学者のワークフローは、マルチエージェントシステムによって駆動され、次のように進みます。

1. 初期探索。完璧なワンショットのプロンプトを要求するのではなく、研究者はシステムと対話しながら高次の目標を洗練し、研究課題を形式化します。作業開始前に研究の意図を明確化します。
2. 文献レビュー。共同数学者は主要論文を特定し、関連する証明や数学的手法を抽出します。
3. 計算フレームワーク。共同数学者はPythonによる計算用ライブラリを作成し、デモケースと関連テストも用意します。
4. 探索の実行。計算フレームワークが整ったら、カスタムライブラリをインポートし、クラウドクラスター上で探索をスケールさせます。低レベルログで研究者を溺れさせることなく、高レベルの進捗を報告します。
5. 最終出力。最終出力はLaTeXでコンパイルされたレポートです。結果だけでなく発見のプロセスを説明し、余白注記で主張を特定の参考文献やコード出力に紐づけます。すべてのレビュ—エージェントが承認して初めてレポートは最終化されます。レビュー不合格のレポートも未解決として研究者に提示されます。これが、欠陥のある証明がLackenbyの目に留まった経緯です。

AI共同数学者のワークストリームアーキテクチャ

AI共同数学者のアーキテクチャは、マルチエージェントシステムであり、最上位にプロジェクトコーディネーターエージェントがいて、専門化されたサブエージェントが支えます。

ワークフローの調整

問題に取り組む前に、プロジェクトコーディネーターは研究者と対話を開始し、明確化のための質問を通じて目標を洗練します。たとえば計算幾何学の未解決問題「ソファ問題」の上界について尋ねる研究者に対し、どのバリアントに焦点を当てるか、あるいは両方か、といった問いを投げかけます。合意された明確な目標が、エージェントを動員する前に問題の範囲を定めます。

目標が固まると、プロジェクトコーディネーターはエージェントやサブエージェントに作業を委任します。依存関係がない限り並行して進みます。あるエージェントは文献レビュー、別のエージェントは計算フレームワークの構築、さらに別のエージェントは探索を担当します。ただし依存関係があります。計算フレームワークで作成したカスタムライブラリが存在しないと、探索は実行できません。

ハルシネーションの回避

標準的なエージェントは、無効な近道を見つけたり、存在しない補題をでっち上げたり、時期尚早に勝利宣言したりすることがあります。AI共同数学者は、レビュ—エージェントを含む仕組みによって、これらの欠点を回避します。

例えば、計算探索中に探索空間が爆発した場合、コーディングサブエージェントは、すべてのテストが合格し、レビュ—エージェントが結果を承認するまで、コードを完成としてマークできません。そのためワークフローが停止します。この失敗した探索はログに記録され、プロジェクトコーディネーターに送られ、コーディネーターはチャットで研究者に通知します。研究者は別のアプローチを提案できます。

こうした行き止まりは単に記録されるだけでなく、情報として扱われます。バージョン管理され、研究記録の一部として保存されます。数学では、失敗したアプローチが制約を明らかにしたり、別の道筋を示したりすることがよくあります。

プロセス全体を通じて、コーディネーターは通常は低レベルのノイズをフィルタしますが、研究者は必要に応じて任意のワークストリームを深掘りし、修正できます。

最初の事例研究とコラボレーション様式

初期の事例からは、異なる協働の様式が見て取れます。誤りと判定された証明の修復が人間の洞察を引き出したケース、余白のコメントが問いを再定義したケース、そして行き止まりを迅速に検出して一週間分の無駄を省いたケースです。

システムが誤りと指摘した証明の修復

オックスフォード大学の数学教授Marc Lackenbyは、（群論の未解決問題集である）Kourovkaノートブックの問題に本システムを適用しました。AIは証明を試み、レビュ—エージェントがその欠陥を見抜き、Lackenbyに報告しました。彼はその穴をどう埋めるか分かっていました。

この受け渡しこそが要点です。機械が見落とした点を人間が捉え、機械はその周辺の重作業を担いました。

余白コメントに導かれた新たな洞察

別の数学教授Gergely Bércziは、スターリング係数に関する予想の問題を調査しました。初期レビューとして、AI共同数学者にテーマ、その背景、既知の方法、AlphaEvolveの実験が示唆した潜在的方向性を提供しました。

AI共同数学者は、2つの予想について（現在人間の数学的レビュー中の）証明を作成し、主張を支える詳細な計算的根拠も示しました。Bércziは、完成文書の余白コメントが重要な洞察に気づかせ、その後チャットインターフェースで追究できたと報告しています。

一週間の損失になる前に行き止まりを検知

最後に、Semon Rezchikovはハミルトニアン微分同相写像に関する技術的な問題を提示しました。彼とプロジェクトコーディネーターは、タスクの正確な定義で合意できるまで議論を重ねました。AIが作成した書き起こしには、問題を本質的に解決する鍵となる補題とその証明（後に検証）が含まれていました。

その過程であるアプローチも試されましたが、行き止まりに達しました。AIは通常よりはるかに速く行き止まりに到達したため、彼は一週間を無駄にせずに済みました。システムは一週間分の徒労を数時間に圧縮しました。

FrontierMathベンチマークの結果

AI共同数学者は、厳密には数学問題を解くツールではなくワークフローのためのツールです。それでも著者らが高いベンチマークを示すことには、いくつかの理由があります。

• 基盤となる数学エンジンが、最前線の数学における有用な協働者たりうる実力を持つことを示すため。
• ベンチマークが、オーケストレーション層がどれほど寄与したかを測定する統制環境を提供するため。
• 標準化された指標が現状存在しないため、協働の有効性を代替的に示すため。

結果として、AI共同数学者は研究レベルのベンチマークであるFrontierMath Tier 4で48%を記録しました。これは、同じテスト・同じティアで19%だったGoogleのGemini 3.1 Proを含め、報告された中で最高のスコアです。Epoch AIは（Tier 1〜4にわたる）FrontierMathの問題の約3分の1に誤りを見つけ、人手によるレビューを進めています。

AI共同数学者は、プロの数学者から提供されたコードで検証可能な解をもつ未リークの研究レベル数学問題100問から成るGoogle社内ベンチマークで87%を記録しました。一方、Gemini 3.1 Proは57%、Gemini 3.1 Deep Thinkは70%でした。

AI共同数学者の既知の限界

論文では構造的な限界について率直に述べています。

• 主な品質管理はレビュ—エージェントと証明エージェントに依存。敵対的なレビューサイクルでは、正しさよりもレビュ—エージェントを満足させる議論に収束してしまうバイアスが生じうるという、構造的な脆弱性があります。
• 洗練されたLaTeX出力が、見かけ上の厳密さを生む恐れ。体裁の整った文書は、基礎となる数学が正しいかどうかに関わらず完成品に見えてしまいます。
• 研究者が真のドメイン専門家である場合にのみ、システムは十分に機能。非専門家が曖昧な問題をシステムに丸投げし、その出力を盲信してしまうリスクがあります。
• AIの証明には依然として人間の検証が必要。例えばBércziの証明は、公開時点で人手のレビュー中でした。

まとめ

AI共同数学者は、AIに「問題を解かせる」段階から、AIとともに反復的で混沌とした数学研究のプロセスに取り組む段階への転換を示しています。本当のボトルネックは、数学者の実務に即したワークフローのインフラです。

このようなエージェント型システムを自ら構築したい場合は、DataCampのAssociate AI Engineer for DevelopersおよびAssociate AI Engineer for Data Scientistsトラックから始めるのが有益です。