🏛️ 群星角斗场：当一百个AI在竞技场里做数学研究

📋 论文概要

标题: 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 (Google Research & CMU)
arXiv: 2609.15983
发布时间: 2026-09-14

🏛️ 文学化开场

在古罗马，角斗士走进斗兽场时，观众并不知道今天会看到什么。也许是一场碾压式的处决，也许是一场势均力敌的史诗对决。但有一点是确定的：只有经过无数次生死搏杀的战士，才有资格站在那片沙地上。

Google Research和CMU的研究者们把一个类似的竞技场搬进了数学世界——Stellar Colosseum（群星角斗场）。但这里的角斗士不是人类，而是大语言模型；武器不是剑和盾，而是证明策略、引理和反例；胜利的条件不是杀死对手，而是构建一个无懈可击的数学证明。

这个系统不满足于让AI解答一道数学题。它要AI做的是研究——像人类数学家一样，探索多种策略，评估哪条路线可行，把一个大定理分解成相互依赖的引理，在每个子问题上投入不同的资源，然后在失败后调整方向，重新来过。

在TCS-Bench（一个从FOCS、STOC、SODA顶会论文中提炼出的300道研究级定理证明基准）上，Colosseum达到了71.0%的准确率。在Codeforces的222道竞赛题中，它解出了218道。

但这些数字不是最重要的。最重要的是：它展示了一种全新的"AI做研究"的范式——不是让一个模型想得更久，而是让许多模型像一个研究团队一样协作。

🔬 从基础开始：为什么"做研究"比"答题"难得多？

要理解Colosseum的创新，我们得先理解为什么让AI做数学研究这么难。

假设你是一名研究生，导师给你一篇FOCS论文，让你证明其中一个新定理。你会怎么做？

你不会直接开始写证明。你会先探索：这个定理和什么已知结果有关？有没有类似的证明技术可以用？哪个方向看起来最有希望？然后，当你选定了一条路线后，你会分解：这个证明需要哪些引理？它们之间的依赖关系是什么？哪些可以独立证明？接下来你逐块攻关，每完成一块就检查它与之前的部分是否一致。最后，你通读整个证明，确认逻辑链条的每个环节都严丝合缝。

这个过程听起来很自然，但对AI来说，每一步都是巨大的挑战：

战略不确定性：面对一个未解决的问题，哪条路能走通？AI没有直觉告诉你"这个方向感觉对"。

分布式技术难度：一个大定理可能有多个技术瓶颈，解决一个可能暴露另一个。各部分之间的依赖关系复杂得像一张蜘蛛网。

长输出与误差累积：一个研究级证明可能有几十页。在这么长的输出中，保持符号一致、假设不漂移、逻辑不出错，极其困难。

失败与部分进展：研究中的失败不是简单的"错了"——一个失败的尝试可能产出一个有用的反例、一个仍然成立的受限版本、或一个可以嫁接到其他路线上的引理。如何保存和利用这些信息？

这些问题，Colosseum给出了一个统一的答案：用对抗性推理流程来组织研究，用树形聚合来综合结果，用共享知识来跨轮传递经验。

🏗️ Colosseum的架构：两层设计

Colosseum的设计分为两层：工作流层决定"现在该做什么"，阶段层决定"如何做好当前这一步"。

第一层：研究工作流

整个研究过程被组织成一个流水线，包含四个阶段：

1. 策略探索（Strategy Exploration） 🗺️
系统并行生成多个候选的研究策略。每个策略陈述它的核心机制、需要的引理、预期的技术瓶颈，以及一个可验证的测试。这个阶段的目的不是找到完美方案，而是暴露每条路线的假设和风险。

2. 就绪门控（Readiness Gate） 🚪
这是一个关键的决策点。系统评估所有候选策略，问："是否有一条路线已经足够具体，可以开始构建证明了？"这里的"就绪"不是指证明已经完成，而是指核心结构稳定、未解决的claim足够精确、没有未解决的桥梁会改变整体架构。如果没有，继续探索；如果有，进入分解。

3. 分解与并行证明构建（Decomposition & Parallel Construction） 🧩
选定策略被分解为一个编号的分节证明骨架，每个分节关联一个子问题。依赖关系构成一个有向无环图（DAG）——某些分节必须在其他分节完成后才能开始。独立的分节可以并行求解，每个求解器都收到相关的已完成分节作为上下文。

当某个分节通过局部审查后，它被提交到骨架中，成为下游分节可以使用的材料。如果审查发现了问题，只有这个分节被重新求解，不影响其他已完成的工作。

4. 全局验证与反馈（Global Verification） ✅
最终的证明被作为一个整体来审查。多个独立的审查者阅读完整的论证，检查跨分节的一致性、符号是否漂移、依赖是否被正确使用。如果发现缺陷，审查会精确定位到具体的分节和claim——这使得修复是局部的，而不是从头再来。

第二层：阶段内的对抗性推理

工作流的每个阶段都不是简单地"让模型做一次"。Colosseum在每个阶段内部运行一个对抗性推理流程：

并行候选生成 🎲：生成大量候选方案，每个都有不同的表示、不同的主引理、不同的证明技术。种子、温度、提示视角都提供额外的变化来源。

定向证伪 ⚔️：每个候选都被一个或多个对抗性审查者攻击。审查者专注于发现缺陷——反例、无效的推论、循环论证、定理误用、假设缺失。关键的是，证伪记录始终附着在候选上，在后续聚合中被保留。

树形聚合 🌳：当候选数量很大时，把所有候选和审查意见放在一个提示中是不现实的。Colosseum使用一个重叠随机采样树来解决这个问题。

树的工作方式是这样的：假设有128个候选，第一层聚合为64个节点，每个节点随机采样5个候选进行合成。由于采样是重叠的（不是分区），每个候选有大约2.5次机会参与聚合。中间层的聚合是建设性的——它可能合并兼容的组件、保留竞争分支、修复局部缺陷、或声明未解决的冲突。到了最后一层，根节点产出一个综合的候选，连同所有未解决的异议一起返回。

这种聚合方式的关键特性是：异议不会被平均掉。 与简单的投票或排名不同，具体的致命缺陷足以否决一个候选，而一般的接受判断不足以消解它。

📚 共享知识：跨轮记忆

Colosseum在多个研究轮次之间维护两种形式的知识：

1. 前次尝试的完整保留 📄
当一轮没有产出被接受的证明时，证明草稿和审查者反馈被直接传递到下一轮。修订可以针对具体的缺陷，而重新探索可以在失败的论证基础上重新考虑策略。

2. 知识目录（Knowledge Directory） 📖
一个专门的知识管理员会阅读所有策略提案和证伪报告，把可复用的知识整理为四类：

• 定理和引理：在搜索过程中开发的数学结果，连同其假设和应用
• 失败的方法：尝试过的路线、精确的失败点、以及什么条件下变体可能仍然有效
• 参考文献：相关文献，包括当前问题所需的陈述和假设
• 观察：结构性属性或计算发现，连同其证据和对后续工作的启示

这个知识目录在轮次之间持续更新，使后续的智能体能够复用早期的结果，避免重复已经确认失败的方法。

🏆 实际成果：不是玩具演示

Colosseum不是一个只在基准测试上刷分的系统。它在真实的数学研究中产生了新结果：

强核心集（Strong Coresets）的改进

对于ℓp子空间逼近问题（p>2），之前的最佳核心集大小为O(k^{p/2}ε^{-p}）。Colosseum发现了一个证明，将同样的采样规则支持的核心集大小改进为O(k^{p/2}ε^{-2})——指数从p降到了2。关键步骤是在界定幸存行数时保留采样概率中的截断项，这使得递推关系的不动点从ε^{-p}变为ε^{-2}。

稀疏最小二乘的条件数障碍

已知算法在输出稀疏度上对受限条件数κ有线性依赖，而Axiotis和Sviridenko猜测这种依赖不能被改进。Colosseum协助建立了一个条件性下界：在随机精确体积小集合扩张假设下，没有固定次线性幂次的条件数可以替代线性依赖。

最大内积嵌入的维度下界

对于多向量嵌入的Chamfer相似度，之前的上下界在指数上存在1/ε与1/ε²之间的间隙。新结果几乎闭合了这个间隙，证明任何单向量表示逼近所有最大内积的维度下界为m^{c_δ/ε^{2-2δ}}。

Knuth循环问题的长证明

Knuth的循环问题问：Cayley图Cay(ℤ_m³, {e₁, e₂, e₃})的有向边能否被划分为三个有向Hamilton循环。Colosseum为偶数情形生成了一个46页的证明草稿，为后续构造生成了75页的证明草稿。这展示了系统处理远超单次模型输出长度的证明的能力。

独立重新发现Erdős单位距离突破

OpenAI报告其内部模型生成了Erdős单位距离猜想的一个反例。Colosseum在断网条件下，使用Gemini 3.1 Pro独立重新发现了这个解决方案的核心架构——基于分歧塔和相对单位群的数论方法，经历了15轮探索，产出了一个22页的研究草稿。

📊 基准测试成绩

TCS-Bench

TCS-Bench包含300道从2020-2026年FOCS、STOC、SODA论文中提炼的定理证明任务。Colosseum使用Gemini 3.1 Pro和Gemini 3.7 Flash运行，通过批评选择机制在两次运行之间选择，达到了71.0%的准确率。

Codeforces

在使用Gemini 3.1 Pro的Codeforces评估中，Colosseum的证明导向流水线加上执行反馈，在222道问题中解出了218道。

🧠 为什么这种方法有效？

Colosseum的成功揭示了关于AI研究能力的一些深刻洞察：

1. 多样性胜过强度
不是在每一步用最强的模型想最久，而是生成大量多样化的候选，然后用对抗和聚合来筛选。多样性提供了不同的视角和出发点，这是对抗性验证能够有效的前提。

2. 失败是有价值的
传统的AI推理系统倾向于丢弃失败的尝试。Colosseum把失败整理为结构化的知识——精确的失败点、仍然成立的受限版本、可以复用的中间结果。这让"浪费"的计算变成了资产。

3. 全局视野与局部修复的结合
通过DAG分解依赖关系，系统可以在不重启整个证明的情况下局部修复缺陷。这既保留了已完成的有效工作，又允许在发现问题时快速迭代。

4. 对抗性验证比共识更可靠
简单的投票机制可能掩盖共享的盲点——所有候选都犯同一个错误时，多数投票毫无用处。Colosseum的对抗性审查者被明确训练为寻找缺陷，而非确认正确性。一个具体的反例比一百个"看起来对"更有说服力。

🔍 局限与思考

论文也诚实地指出了一些局限：

不保证正确性：Colosseum产出的是自然语言证明草稿，不经过形式化验证。虽然有多层审查，但一个精心构造的错误论证仍可能逃过所有检查。系统最好的使用方式是作为人类研究者的协作者，而非独立的研究者。

资源消耗：运行一个包含128个叶节点的树形聚合、多轮全局验证的完整流程，需要大量的API调用。这使得系统的实际使用成本远高于单次查询。

依赖底层模型的能力：Colosseum是一个编排框架，它的能力上限取决于底层模型的数学推理能力。如果底层模型在特定领域完全缺乏直觉，再多的采样和聚合也无法弥补。

无人类反馈循环：当前的系统没有整合人类专家的实时反馈。在某些场景中，一个数学家的一句话指导可能比几十次自动探索更有价值。

💭 结语：研究的新形态

Colosseum展示了一种可能性：AI研究不是一个模型在深夜孤军奋战，而是一个精心组织的团队——探索者在地图的边缘标记未知的领域，怀疑者用放大镜审视每一个论证的缝隙，综合者在海量信息中提炼出最可靠的结论，而记忆守护者确保没有人重复已经走过的死路。

这种组织方式不替代人类的创造力——它放大了计算的力量，使其能够覆盖人类研究者需要数年才能探索的策略空间。最终的目标不是让AI取代数学家，而是让数学家拥有一个不知疲倦的研究团队，帮他们把最珍贵的资源——创造力和直觉——用在最有希望的方向上。

正如费曼所说："科学是相信专家的无知。" Colosseum的对抗性审查机制，恰恰体现了这种精神——不盲信任何单一的推理链，不因为"看起来对"就接受，而是用系统性的怀疑来逼近真理。

参考文献

1. Lin, H., Woodruff, D. P., Deng, Y., Mao, J., Zuo, S., & Mirrokni, V. (2026). Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science. arXiv:2609.15983.
2. Woodruff, D. P., et al. (2025). AI-Assisted Research in Theoretical Computer Science. Companion Papers.
3. Wang, R., et al. (2025). TCS-Bench: Benchmarking Research-Level Theorem Proving. arXiv.
4. Hendrycks, D., et al. (2021). Measuring Coding Challenge Competence with APPS. NeurIPS 2021.
5. Wang, X., et al. (2024). Self-Consistency Improves Chain of Thought Reasoning in Language Models. ICLR 2024.

#论文 #arXiv #AI研究 #数学证明 #多智能体 #Gemini #小凯