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 題。
- 這套工作流程如今以 Long Proof 模式內建於 Google Antigravity 的 Teamwork 框架，付費方案可透過預覽指令使用。
這套框架把算力花在哪裡
Colosseum 在真正動筆寫證明之前會先跑過好幾個階段。它不會一頭栽進第一條看起來有希望的路徑，而是先探索其他替代策略；接著套用一道「成熟度閘門」，判斷該路徑是否已經成熟到可以拆解。到這一步之後，它才把證明計畫表示成一組彼此相依、以章節為單位的子問題。
驗證機制也接回了這個結構。當驗證器標出問題，該發現會被送到它所影響的那一段論證，而不是逼整份證明從頭再來。在每個階段，框架都會並行產生候選解，以針對性的反證加以攻擊，再把候選解與對它們的批評合併成單一份研究產出，作者稱這套做法為重疊隨機抽樣樹狀聚合。
這和擴大單一代理的脈絡長度、讓它想得更久是兩種不同的賭注。它更接近經營一個小型的對抗式研究團隊，只不過這裡被排程的昂貴資源不是研究人員的時間，而是推論。
基準數字說了什麼
TCS-Bench 比模型發表會上常見的競賽數學題組難得多，因為它的題目直接取自該領域三大理論會議所接受的論文。71.0% 這個數字來自混合配置：Gemini 3.1 Pro 搭配更便宜的 Gemini 3.7 Flash，這顯示框架是靠協調而非把所有呼叫都丟給最大的模型來把品質補回來。
Codeforces 的結果範圍較窄，但同樣醒目——在迴圈中加入執行回饋後解出 222 題中的 218 題。這兩個數字都出自作者自行執行的評測，尚未有獨立重現。適用於每一篇代理鷹架論文的基準測試但書，在這裡同樣成立：框架類成果對提示詞與工具設定的細節敏感得出了名，而這些細節往往在重新實作時就活不下來。
從論文到產品
與多數研究鷹架不同，這一套已經有了產品接觸面。Google 表示，Colosseum 工作流程已整合進 Antigravity 的 Teamwork 框架，成為系統可選用的五種模式之一，名為 Long Proof；該公司並稱 Teamwork 已產出七項未解問題的成果，其中包括一篇 JMLR 論文中的稀疏凸最佳化問題，以及以 Lean 驗證過的高德納循環猜想。
論文主張自己針對 FOCS 與 JMLR 論文中的未解問題取得了新結果。這與基準正確率是性質截然不同的主張，也是整個領域最會嚴加檢視的一項。OpenAI 動用一萬個代理挑戰納維－斯托克斯方程的證明時就是如此，附註比標題更重要。不過 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 工作流程以 Long Proof 模式提供於 Google Antigravity 的 Teamwork 框架中，形式是付費方案的預覽指令。論文本身則是 arXiv 上的預印本，尚未經過同儕審查。
