Googleの研究チームが、数学と理論計算機科学の研究に推論資源を配分するマルチエージェント・ハーネス「Stellar Colosseum」を公開しました。FOCS・STOC・SODAの論文から採られた研究水準の定理証明タスク群のベンチマークで、正答率71.0%を記録したとしています。Honghao Lin氏、David P. Woodruff氏、Vahab Mirrokni氏らによるこの論文が説明するシステムは設計段階からモデル非依存で、すでにGoogle Antigravityへ組み込まれています。
出発点はおなじみの失敗パターンです。言語モデルは短い証明ならもっともらしく書けますが、不確かで相互依存する判断が連鎖する長期課題になると性能が崩れます。序盤で一度まずい確定をすると、その先すべてが汚染されるからです。Colosseumの答えは、証明を単一の軌跡として扱うのをやめることでした。
要点
- Stellar ColosseumはGemini 3.1 ProとGemini 3.7 Flashを組み合わせ、FOCS・STOC・SODAの論文から抽出した研究水準の定理証明タスク集「TCS-Bench」で71.0%を記録しました。
- Gemini 3.1 Proによる別のCodeforces評価では、実行フィードバックを組み込んだ証明志向のパイプラインが222問中218問を解いています。
- このワークフローは現在、Google AntigravityのTeamworkフレームワークにLong Proofパターンとして搭載され、有料プランのプレビューコマンドとして利用できます。
ハーネスは計算資源をどこに使うのか
Colosseumは証明の執筆に踏み切る前に、いくつもの段階を踏みます。まず有望に見えた最初の経路へ即座に降りていくのではなく、代替戦略を探索します。次に「準備度ゲート」を適用し、その経路が分解できるだけ成熟しているかを判定します。そこまで済んでから、証明計画を相互依存するセクション単位の部分問題の集合として表現するのです。
検証はこの構造へ折り返し接続されています。検証器が問題を指摘すると、最初からやり直させるのではなく、その指摘が影響する論証の該当箇所へ結果が配送されます。全段階を通じてハーネスは候補を並列生成し、標的を絞った反証で攻撃し、候補とその批判を一つの研究成果物へ統合します。著者らはこの手法を重複ランダムサンプル木集約と呼んでいます。
これは単一エージェントの文脈長を伸ばして長く考えさせる賭け方とは方向が異なります。むしろ小規模な敵対的研究チームを運営するのに近い発想です。ただしここでスケジューリングされる高価な資源は、研究者の時間ではなく推論のほうです。
ベンチマークの数字が語ること
TCS-Benchは、モデル発表の定番である競技数学のセットより手強い相手です。タスク自体が、この分野のトップ理論会議3つに採択された論文から採られているからです。71.0%という数値は混成構成から出ています。Gemini 3.1 Proに、より安価なGemini 3.7 Flashを組み合わせた形です。ハーネスがすべての呼び出しを最大モデルに寄せるのではなく、協調によって品質を回復していることを示唆します。
Codeforcesの結果は射程こそ狭いものの目を引きます。実行フィードバックをループに入れて222問中218問を解きました。いずれの数字も著者ら自身の評価によるもので、独立した再現は行われていません。あらゆるエージェント・スキャフォールド論文につきまとうベンチマークの但し書きは、ここにも当てはまります。ハーネスの成績は、再実装で残りにくいプロンプトやツール設定の細部に悪名高いほど敏感です。
論文から製品へ
大半の研究用スキャフォールドと違い、こちらはすでに製品としての接点を持っています。Googleによれば、ColosseumのワークフローはAntigravityのTeamworkフレームワークにLong Proofパターンとして統合されており、システムが選択する5つのパターンの一つです。同社はTeamworkが未解決問題で7件の結果を出したとし、そこにはJMLR論文のスパース凸最適化の問いや、Leanで検証されたクヌースの巡回予想が含まれると説明しています。
論文はFOCSとJMLRの論文に残る未解決問題へ新たな結果を出したと主張します。これはベンチマーク精度とは性質のまったく違う主張であり、この分野が最も厳しく検める部分でもあります。OpenAIが1万体のエージェントで挑んだナビエ・ストークス方程式の証明でも、見出しより注釈のほうが重要でした。もっともLeanによる形式検証がある分、Googleはその主張の少なくとも一部で確かな足場を得ています。
よくある質問
TCS-Benchとは何ですか?
TCS-Benchは、理論計算機科学の主要会議であるFOCS、STOC、SODAで発表された論文から採られた、研究水準の定理証明タスクのベンチマークです。競技会の練習問題ではなく、開かれた研究課題を対象にしています。Stellar ColosseumはGemini 3.1 ProとGemini 3.7 Flashの組み合わせで71.0%の正答率を報告しました。
Stellar ColosseumはGeminiに縛られていますか?
いいえ。著者らはこのハーネスをモデル非依存だと説明しています。どのモデルが呼び出しを処理しても、その上に載るスケジューリングと集約の層だという位置づけです。ただし公開された評価はGemini 3.1 ProとGemini 3.7 Flashで行われているため、報告された数字はアーキテクチャそのものではなく、それらのモデルに固有の結果ということになります。
開発者は今すぐ使えますか?
間接的には使えます。ColosseumのワークフローはGoogle AntigravityのTeamworkフレームワーク内でLong Proofパターンとして提供されており、有料プランのプレビューコマンドという形です。論文自体はarXivのプレプリントで、査読は経ていません。
