Stellar Colosseum：面向数学与理论计算机科学长程研究的多智能体框架

语言模型能够生成看似合理的简短证明，但在长程研究问题上可能仍不可靠，因为这类问题的进展取决于一系列不确定且相互依赖的决策。我们提出 Stellar Colosseum，这是一种与模型无关的框架，用于在数学和理论计算机科学研究中分配推理资源。Colosseum 在构建证明之前探索多种备选策略，使用就绪度门控来决定某条路径何时成熟到足以进行分解，将证明计划表示为相互依赖的章节级子问题，并将验证器的发现反馈至论证中受影响的部分。在这些阶段中，它并行生成候选方案，通过有针对性的证伪对候选方案发起攻击，并通过重叠式随机采样树聚合，将候选方案及其批评整合为单一的研究成果。Colosseum 工作流还已集成到 Google Antigravity 的 Teamwork 框架中，作为 Long Proof 模式。 我们通过开放式研究，以及在定理证明和竞赛编程基准上的评测，展示了 Colosseum 的能力。将 Colosseum 与 Gemini 3.1 Pro 结合使用后，我们取得了若干新成果，解决了源自发表于 FOCS 和 JMLR 等顶级会议或期刊论文中的开放问题。在 TCS-Bench 上——这是一个从发表于 FOCS、STOC 和 SODA 的论文中抽取的研究级定理证明任务基准——Colosseum 使用 Gemini 3.1 Pro 和 Gemini 3.7 Flash 达到了 71.0% 的准确率。在另一项使用 Gemini 3.1 Pro 进行的 Codeforces 评测中，带有执行反馈的面向证明的流水线解决了 222 道题目中的 218 道。