Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science
Honghao Lin, David P. Woodruff, Yuan Deng, Jieming Mao, Song Zuo, Vahab Mirrokni
cs.AI, cs.CL, cs.LG
2026-09-15
Colosseum 先探索策略再把证明拆成 DAG，候选经定向证伪后做重叠树聚合，Gemini 3.1 Pro 与 3.7 Flash 跨模型选择在 TCS-Bench 达 71.0%，加执行反馈后 Codeforces 222 题过 218 题。
语言模型已经能写出看起来像样的短证明。长程研究卡在另一处：先选哪条路、引理怎么切、某一步垮了要不要换方向，这些决策互相咬着，错一步后面整段都可能作废。对终稿做平坦投票帮不上忙，因为多条推理路径可以共享同一个错。
已有系统把探索、分解、验证拆成不同角色，或者在 Lean 里用形式化检查器盯每一步。Colosseum 面对的是策略本身还不稳、证明也还没形式化的理论计算机科学和数学问题。证明可能比单次模型输出长得多；失败尝试里仍可能留下反例、限制条件和中间结论。这些东西若不记下来，下一轮等于从头再猜。
Google Research 与 CMU 给出一套模型无关的多智能体编排，名叫 Stellar Colosseum。工作分两层。
外层是研究管线。并行探索不同改写、中间断言、以及和已知结果的连接。就绪门（readiness gate）不问证明是否已经写完，只问这条路的核心机制是否稳定、未决断言能否分到具体小节、会不会改掉整份论证的骨架。过关之后，分解器把路线变成带依赖边的 DAG：文档顺序管叙述，依赖图管谁能先算。独立小节并行写；局部审查不过关，只重跑受影响的那一节，别的已完成工作保留。全部填完后，全局验证器把整份证明当一个论证来读，核对依赖是否带错假设、记号有没有漂、有没有漏情形、最终命题是否对上原问题。致命缺陷一票否决，不是多数表决。策略还站得住就修订小节或大纲；骨架垮了，回到探索。
内层在每个难阶段复用同一套对抗推理。先并行生成一批候选，来源包括不同表示、主引理、证明技术和假定的攻击路线。再让对抗审查专门找错：反例与边界、偷加强的假设、循环论证、定理或外部引用误用、所证命题和目标对不上。证伪记录贴在对应候选上。最后用重叠随机抽样树聚合：每一层的聚合节点从当前种群里无放回抽 k 个，不同节点独立抽样，集合可以重叠。中间聚合是构造性的，可以合并兼容部分、保留竞争分支、修局部错，也可以把冲突原样带上去。批评不会被投票平均掉。
跨轮记忆有两份。上一轮完整草稿加验证意见直接喂给下一轮；知识目录另外收录定理与引理、失败路径及其失效点、文献陈述、以及带证据的观察。开放问题研究里，探索树可以超过 100 个叶节点，其余阶段固定 16 叶。TCS-Bench 和 Codeforces 的探索树宽度是 (32, 16, 8, 5, 1)，其余阶段是 (16, 8, 5, 1)，每节点抽样 k=5。
开放研究里，工作流贡献了五条后续论文中的结果。p>2 时 ℓp 子空间逼近的强 coreset 规模，从原先分析里的 ε^{-p} 改成 ε^{-2}，运行时间仍是 Õp(nnz(A)+d^ω)。稀疏最小二乘在随机精确体积 Small-Set Expansion 假设下，条件数的线性依赖不能换成任何固定的次线性幂。最大内积嵌入的维数下界把指数里 1/ε 和 1/ε² 的空隙几乎补上。单阶段 Hadamard 量化去掉残差级的 O(d) bit 载荷，把已证上界的领先常数大约缩小 5.93 倍。前缀矩阵分解的 γ{2,1}(Q) 下界达到 Ω(log^{3/2} n / (log log n)^{3/2})，与 dyadic 上界只差 (log log n)^{3/2}。
两个案例补了长度和隔离条件。Knuth cycles 的两条构造分别产出 46 页和 75 页证明草稿。Erdős 单位距离问题在禁用联网的条件下，用 Gemini 3.1 Pro 跑了 15 轮探索，写出 22 页草稿，独立摸到了与 OpenAI 方案相近的架构。
TCS-Bench 有 300 道题，来自 2020–2026 年 FOCS、STOC、SODA 论文。参考辅助自动打分器在另 100 份专家标注证明上超过 90% 准确率。
| 方法 | TCS-Bench 准确率 |
| Gemini 3.1 Pro 直接评 | 30.3% |
| Gemini 3.1 DeepThink | 52.0% |
| GPT-5.6 Pro (max) | 68.0% |
| Colosseum + Gemini 3.1 Pro | 54.0% |
| Colosseum + Gemini 3.7 Flash | 55.0% |
| 跨模型选择 | 71.0% |
| Oracle best-of-two | 77.3% |
选择规则：Gemini 3.7 Flash 对 Pro 的证明独立抽 8 次批评，至少 5 次判对就交 Pro，否则交 Flash。选出的证明解了 213 题，比单跑更强的那次多 48 题。批评信号相对打分器的 AUC 是 0.896；只用 Pro 内部验证器做路由，准确率 64.7%。
Codeforces 侧沿用 Gemini 3 Deep Think 的题单：222 道 clist.by 估计难度高于 1500 的题，来自 52 场、编号 2084–2162，中位难度 2381。隐藏测试全过才算接受，按提交原文评分。Gemini 3.1 Pro 加上 C++ 执行探针（公开样例和模型生成的压力输入）是 218/222，语料级表现分 4263；去掉探针是 213/222、3918。两端修订预算不同，论文写明这 5 题之差不能当成探针的因果效应。
这套工作流已被接进 Google Antigravity 的 Teamwork，称作 Long Proof pattern。
对做 agent 编排的人，这是一套把「先想清楚走哪条路」和「长证明怎么并行写、怎么局部修」接起来的具体设计。批评跟着候选走、失败路径写进知识目录，针对的就是长程研究里最容易丢掉的中间产物。竞赛题那边，分解的终点改成一段 C++ 实现，说明同一套 DAG 可以迁到可执行任务，不必另起一套写代码专用控制器。
数字上要分开看。单模型 Colosseum 54.0% 和 55.0%，只比 DeepThink 的 52.0% 高一点，低于 GPT-5.6 Pro (max) 的 68.0%。71.0% 来自两个模型证明互补，再加批评路由，不是单套编排单独打出来的。论文没有给出与 DeepThink 的算力对齐对照。
开放结果的措辞是 workflow contributed，完整定义和证明在 companion papers 里。把它读成全自动独立发现，论文自己也不支持。
正文没有单独的 Limitations 节。能核对到的缺口如下。
证明主产物是自然语言。形式检查和可执行测试有则当证据用，系统不以 Lean 证书为通过条件。TCS-Bench 的数字经过自动打分器，打分器在 100 份专家标注上超过 90% 准，剩下约一成噪声会进准确率。
单模型相对 DeepThink 的增益很小，又缺算力对齐，说不清多出来的那两个点是编排还是多花了推理。跨模型 71.0% 离 oracle 77.3% 还有 6.3 个点，路由会错杀。Codeforces 两臂修订预算不同，探针到修订的路径也没有单独验证。
五条研究贡献、Knuth 长稿、Erdős 重发现，都很难把人和编排的功劳切开。Erdős 那次是断网条件下摸到相近架构，22 页草稿，不是一篇已经人类核验并发表的完整证明。
未来工作自己点了几处：少数派策略容易在混合种群里被聚合吃掉；小节边界切错时只能整节重试；树宽和抽样数开跑前写死；轨迹若拿去训练，功劳归属仍不清楚。