複数のAIエージェントで未解決問題に取り組んだ成果を公表
米Googleは11月13日（日本時間14日）、開発ツール「Antigravity」の機能「/teamwork」などを使って、数学や化学、ソフトウエア開発の未解決の課題に取り組んだ成果を、Google Researchのブログで公表した。/teamworkは、役割を分けた複数のAIエージェント（AIが自分で作業を進める仕組み）を協力させる機能だ。公式ブログによると、Googleと提携先の大学の研究者がここ数週間、「Gemini 4 Argon」「Gemini 4 Carbon」「Gemini 4 Hydrogen」と/teamworkなどを使い、何年も解けていなかった問題に取り組んだ。どの成果も人間の専門家との協力によるもので、Googleはこれらの道具を外部にも提供するとしている。
公式ブログの筆者で、署名を「Google Fellow and VP, Google Research」とするバハブ・ミルロクニ氏は、日本時間14日早朝にXで成果を告知した。投稿では、/teamworkと、論文の原稿を点検する「DeepReview」を「powered by Gemini 4 models」と説明し、数学と計算機科学の理論で10件以上の未解決問題を解いたとしている。件数は公式ブログには書かれていない。
Check out our recent results solving open challenges across math/science and engineering with /teamwork and Gemini 4 models : https://t.co/in8niq88d4 Details: Following our recent updates on Antigravity’s /teamwork, we’ve been hard at work solving open challenges with our multiagent workflows (/teamwork and DeepReview powered by Gemini 4 models) and pushing these tools externally for everyone to use. Through close collaboration with academic partners, we are evolving these tools into true research and engineering partners designed to tackle open problems. We just posted on the Google Research blog providing a few recent examples : * Math Open Problems & Formal Verification: Reporting 10+ open math and CS theory problems solved including 50M-line Lean 4 proof of Courtade–Kumar conjecture plus open problems in quantum query complexity, Tarjan's Deque Conjecture. Also autonomous Lean formalizations of the Weil (1.8M lines), Birkhoff, and 3D Bochner–Riesz conjectures via Teamwork-LEAP, plus updates on Deep Review for STOC’27. * Chemistry & Discovery: 95% top-1 exact match on NMR molecular structure elucidation (nearly 2× single-agent). Also empowering Nuclear Fusion and Quantum algorithm results as well autonomously generating a CausalAnalyst Benchmark. * Systems, TPU Kernel, & Infra: * Clustering 1-Trillion-edge graphs on FarArray and RDMA (up to 180× faster), * 800K-line Zircon & 170K-line libgav1 safe Rust rewrites (20–30% faster than C++/ASM), * 4.09× JAXBench TPU kernel speedups with DuoDiscover, * surpassing 1 PiB fleet memory savings, and 24% fewer Borg TPU preemptions. Best of all, these tools are available externally in Antigravity. Previously, when we developed agents for coding and math competitions and later for science acceleration, we relied on internal models and agentic tools; now, I am happy we can share these tools with everyone—with Hydrogen models available to all, and Carbon and Argon models for Enterprise and Ultra/Paid users. We’re also opening applications for 10,000 academic researchers to get 6 months of free access to our highest usage tier for Antigravity. We also provide two free weekly DeepReview calls for all. This is a collaboration across many at Google (in Gemini, Antigravity, Research, Cloud); Congratulations to the whole team! We will post more details in Antigravity blog post. Apply for the academic researcher access program: https://t.co/BfuStASb4W, and Try DeepReview: https://t.co/r26ksY3COc Read the full blog here : https://t.co/in8niq88d4 #AntiGravity #Gemini4 #teamwork #AI4Math #AI4Systems #AI4Coding
Google DeepMindの共同創業者のデミス・ハサビス氏は、日本時間15日早朝にこの投稿をリポストした。独自のコメントは付けていない。
/teamworkは、モデルの答えが毎回同じにならない点と、何日も続く作業で細部を見失いやすい点を補う設計だという。複数のエージェントが並行して答えを探し、証明を検証するLean 4や既存のテストなどで、どの答えが正しいかを自動で確かめる。各エージェントには、その作業に必要なファイルと道具だけを渡し、批評役や監査役のエージェントが、作った側の考えを見ない状態で結果を確かめる。
情報理論の予想を証明し、Lean 4の5000万行で検証
数学では、2013年に示された情報理論の「Courtade–Kumar予想」の証明を挙げた。雑音の入る通信路を通したランダムなビット列について、入力を1ビットに縮める方法の中で、入力の1ビットをそのまま写す方法より多くの情報を残すものはない、という予想だ。Googleと香港中文大学（CUHK）、南カリフォルニア大学（USC）、カーネギーメロン大学（CMU）の研究者が、/teamworkの長い証明向けの手順を使い、完全な一般性で証明した。
公式ブログによると、まずGeminiが、CUHKの研究者の以前の論文にある一般化した予想に反例を見つけた。これを受けてCUHKの研究者が新しい候補の関数を示し、問題を14変数の最適化問題に絞り込んだ。その後、Gemini 4 Argonと以前のGeminiのモデルが、調べる範囲を分割し、新しい解析的な評価の大半と、区間演算による証明書を作った。研究チームは証明全体をLean 4で形式化し、5000万行のコードになった。
ほかにも、2014年から残っていた適応的なデータ分析の問題では、Gemini 4 Argonで動く複数のエージェントが、ほぼ最適な標本数の限界を独自に証明し、Leanで検証した。量子計算では、2014年の未解決の問いに答える新しい構成を見つけた。1985年に示された「TarjanのDeque予想」では、予想の解決まではいかないものの、大きく前進させる新しい上界を示し、Lean 4で検証した。Googleは、研究者が問題文をGemini 4や複数エージェントの仕組みに渡し、得られた証明を著者が検証し、簡潔にし、手を入れて発表したと説明している。
Weil予想を約180万行で自律的に形式化、STOCの投稿578本を点検
形式化（数学の証明を、計算機が1行ずつ確かめられるコードに書き直すこと）でも成果を挙げた。Google Cloud AIと開発した複数エージェントの仕組み「LEAP」を/teamworkと組み合わせ、Argonと使ったという。有限体上の多項式の解の数に関する「Weil予想」（1974年にドリーニュが証明を完成）を、完全に自律して形式化した。約180万行のLeanのコードで、下位のエージェントを2万8800回呼び出した。
1927年から未解決とされてきた力学系の「Birkhoff予想」について初めての形式化を作り、50年以上未解決の調和解析の「3次元Bochner–Riesz予想」も初めて形式化した。Bochner–Riesz予想では、最近公開された証明の穴を見つけて直したという。
論文の原稿を点検するDeepReviewは、計算機科学の国際会議「STOC 2027」の投稿者に提供した。全投稿の3分の1を超える578本の著者が、原稿への指摘を受け取ることを選んだ。継続中の著者への調査（回答70人）では、90%が指摘はおおむね、またはほぼすべて事実に基づくと答え、90%がまた使いたいと答えた。30%超が証明の誤りや数学的に重要な誤記を指摘されたと答え、14%は直すのに1時間以上かかる技術的な穴を指摘されたと答えた。
化学では分子構造の決定で95%が正解と一致
化学では、核磁気共鳴（NMR）の実験データから分子の構造を決める問題に使った。30のエージェントを、物理に基づいてスペクトルを再現する模擬装置と組み合わせ、互いに誤りを直す仕組みにした。複雑な分子を集めたベンチマークで、1位の候補が正解と完全に一致した割合が95%、上位3つに正解が入った割合が100%になった。Googleは単独のエージェントのほぼ2倍の成績だとするが、単独の場合の数字は公式ブログに書かれていない。
公式ブログは、Gemini 4のブログで報告した核融合や量子アルゴリズムの成果にも、/teamworkとArgonが役立ったとしている。因果推論のベンチマーク作りでは、Argonで動く29のエージェントが11.5時間で、13の公開データの表から50問を作った。ミルロクニ氏の投稿は、これを「CausalAnalyst Benchmark」と呼んでいる。
ソフトウエアの書き換えでは、Rust版が元のC++より20〜30%速く
システム開発では、/teamworkに測定の道具やテストを組み合わせ、数日がかりの開発を任せた。Googleの動画の復号ソフト「libgav1」は、C++から約17万行のRustに書き直し、幅広い適合テストで出力が元とビット単位で一致した。書き直した直後は元のC++より約4倍遅かったが、性能を測る道具を渡して速さを最大にするよう指示すると、x86_64とARMの両方で、元のC++と手で最適化したアセンブリより20〜30%速くなった。
OSのカーネル「Zircon」では、先に25%を移していたのに続き、Argonを使った2週間の作業で残りのC++を書き直し、安全なRustのコードを約80万行加えた。カーネルの単体テストにすべて合格し、arm64の機器で起動したという。ただし、この書き換えの手順は「まもなくAntigravityで提供する」段階だ。
データ処理では、低遅延でメモリーを共有する仕組み「FarArray」を作った。これを使った計算は1兆本の辺を持つグラフにも対応し、TCPでつなぐキー・バリュー型の保存先と比べて、処理量は60〜90倍、速度は40〜180倍で、使うメモリーは6分の1になった。TPU（Googleの独自のAI半導体）向けのプログラムの最適化では、/teamworkの「DuoDiscover」という手順をArgonで使った。実機での評価に7〜32分かかるところを、23秒で済む代わりの評価方法を作って候補を絞り、JAXBenchの17のカーネルで参照実装の4.09倍、vLLMのTPU向けの7つのカーネルで2.99倍に速めた（いずれも幾何平均）。
Google社内の設備にも使った。サーバー群全体のメモリーでは、当初見込んでいた1PiB（ペビバイト）を上回る節約の余地を見つけた。計算資源を割り振る社内の仕組み「Borg」では、変更2件を実装し、一部の種類の機器でTPUの処理が中断される回数を24%減らした。
| 分野 | 対象 | Googleが示した数字 |
|---|---|---|
| 数学 | Courtade–Kumar予想の証明 | Lean 4で5000万行 |
| 形式化 | Weil予想 | Leanで約180万行、下位エージェントを2万8800回呼び出し |
| 論文の点検 | STOC 2027へのDeepReview | 578本が利用、調査の回答者の90%が事実に基づくと評価 |
| 化学 | NMRによる分子構造の決定 | 1位の完全一致95%、上位3つで100% |
| ソフトウエア | libgav1のRust化 | 約17万行、元のC++とアセンブリより20〜30%速い |
| ソフトウエア | ZirconのRust化 | 約80万行を追加、単体テストにすべて合格 |
| TPU | DuoDiscoverによるカーネルの最適化 | JAXBenchの17カーネルで4.09倍 |
| 社内設備 | Borgの割り振りの変更 | 一部の機器でTPUの中断を24%削減 |
研究者1万人に最上位の利用枠を6カ月無料、DeepReviewは週2回無料
公式ブログによると、外部の科学者や開発者は、Antigravityの/teamworkと、日常のプログラミング向けの「/boost」でGemini 4のモデルを使えるほか、DeepReviewも同日から使える。DeepReviewは、利用者に週2回まで無料で提供する。学術研究者1万人を対象に、Antigravityの最上位の利用枠を6カ月無料で使える申込も始めた。
ミルロクニ氏の投稿によると、Hydrogenのモデルは全員が、CarbonとArgonのモデルは「Enterprise」と「Ultra/Paid」の利用者が使える。このプラン別の対象は、公式ブログには書かれていない。申込の受付期間や選考の方法も、投稿と公式ブログには示されていない。
すべての手順が外部で使えるわけではない。公式ブログによると、形式証明の手順などはこれからAntigravityに加え、今後数週間でAntigravityのブログに詳しい使い方を載せる。ミルロクニ氏も、詳細をAntigravityのブログで出すとしている。
今回の成果はGoogleによる発表で、公式ブログは多くの成果について論文の公開先やコードの置き場所へのリンクを載せている。査読を経たかどうかは書かれていない。
