Google 开放 Antigravity 的 /teamwork 多智能体科研与工程协作工具

过去几周里，Google 及其学术合作机构的多个团队针对数学、科学和复杂系统工程领域悬而未决多年的公开难题展开了攻关。借助 Gemini 4 Argon、Gemini 4 Carbon、Gemini 4 Hydrogen 以及 Antigravity 的 /teamwork（基于多种 Gemini 模型构建）等多智能体工作流，这些合作在信息论、形式化验证、分子结构发现和内核优化等领域取得了一系列新突破，同时也为 Google 的生产基础设施带来了多项性能提升。我们现已在 Antigravity 的 /teamwork 中开放这些智能体工具（同时包含 /boost 及其他智能体），方便研究人员和开发者将其应用到自己的工作中。

前沿科学研究与系统工程往往需要查阅海量文献、构建定制计算流程、对照物理测量数据进行测试，并对每一个步骤进行严密验证。真正的突破往往源于一种交互式探索闭环：由研究人员提出问题并划定理论或物理约束，再由擅长长程任务的智能体编写定制求解器、探索庞大的搜索空间、测试候选设计方案，并对冗长的逻辑链条进行逐一验证。

扩展长程推理能力

当前语言模型的两大局限，直接推动了 /teamwork 的设计。首先，模型生成的结果往往具有不可预测性，单次尝试很难直接得出正确答案。该系统将并行探索与专用的证伪机制（例如 Lean 4 证明检查器、原生软件测试套件、执行模拟器、网络搜索或硬件计数器）相结合，自动验证哪些候选方案确实可行，从而弥合了这一差距。

其次，在执行跨越数天的任务时，随着上下文窗口不断膨胀，AI 模型的注意力会被稀释，容易遗漏细节。为解决这一问题，/teamwork 从架构上对上下文进行了隔离设计：每个专用智能体只接收当前步骤所需的具体文件和工具。协调者会将任务交接给拥有全新上下文的后继智能体，而评审者和审计者则在完全不受原始生成者推理干扰的纯净上下文中，对结果提出质疑并加以验证。

Teamwork 将这些工作流表示为声明式的、可自我改进的自然语言模式，并能根据用户输入的提示词，动态路由至最适合该任务的模式。这些模式涵盖了分布式编码、迭代式问题求解（作为独立功能打包为 /boost，即从以往运行轨迹中提炼出的“求解-验证”串行循环），以及长证明和文档评审等专用科研工作流，目前均已在 Antigravity 中上线。这使得团队能够根据以往的运行记录定制规范，在不同的测试驱动模式间灵活路由，并动态优化智能体驱动架构。尽管其中许多功能已在 Antigravity 中推出，我们仍将在未来几周带来更多更新，向外部用户全面开放所有功能。继此前关于 Antigravity /teamwork 的发文之后，我们在此展示由 /teamwork 新变体及 Gemini 4 模型联袂攻克各项挑战的最新成果。

数学与理论计算机科学

在数学和理论计算机科学领域，研究人员借助 Gemini 4 与 /teamwork 框架开展大规模协作证明，甚至直接根据未解决公开问题的表述，端到端生成了完整的算法与证明。以下是几个典型案例。

证明并形式化验证 Courtade–Kumar 猜想

来自 Google、香港中文大学（CUHK）、南加州大学（USC）和卡内基梅隆大学（CMU）的研究人员利用 /teamwork 的长证明范式（Long Proof pattern）（该范式在 Antigravity 中实现了 Stellar Colosseum），在全般性条件下证明了信息论领域的 2013 年 Courtade–Kumar 猜想。这一结果证实：当随机比特串通过带噪信道时，将输入压缩为单个比特的任何方式，所保留的信息量都不会超过“独裁函数”（即直接复制输入的某一个比特）。Gemini 首先发现了中大团队此前论文中一个广义猜想的反例；随后中大团队提出新的候选函数，将该猜想简化为一个 14 变量的最优化问题，并给出了关键的解析下界。接着，Gemini 4 Argon 及更早的 Gemini 模型对参数空间进行划分，推导出了大部分新的解析边界与区间算术证明证书，并在无人工干预的情况下将证明从平衡函数推广至非平衡函数。最终，团队在 Lean 4 中形式化验证了完整证明，生成了多达 5000 万行代码。

攻克最优化、统计学、量子计算与算法领域的未解难题

研究人员还将若干公开难题直接交给 Gemini 4 以及 Stellar Colosseum、/teamwork 等多智能体框架，直接得到了端到端的算法和证明（多附带 Lean 4 形式化代码），随后由作者核验、化简并整理发表。在自适应数据分析领域，基于 Gemini 4 Argon 运行的多智能体框架针对根据历史回答自适应选取的统计查询，独立证明并用 Lean 验证了其近乎最优的样本界，解决了自 2014 年以来悬而未决的问题。这些界限催生了首个适用于兼有插入和删除操作的数据流、且面对自适应对抗样本仍能保持精度的近空间最优算法。在量子计算领域，一项新构造通过找出首批在恒定误差下量子查询次数严格大于 n/2 的 n 比特布尔函数，彻底解决了 2014 年的一道悬案，并同时精确锁定了对称函数上的查询开销。

多项研究成果打破了海量矩阵与图处理及压缩领域长期存在的瓶颈。在 STOC 2024 之前的 50 年间，针对布尔矩阵乘法与三角形检测的组合算法（避免了快速矩阵乘法中的代数相消）相比立方时间复杂度只能节省对数因数。而一项全新的确定性算法解决了 STOC 2024 提出的核心公开问题，成功实现了相比立方时间的预期加速。在高维几何领域，一个新下界攻克了稀疏网络方面的公开难题，证明了哪怕引入额外的施泰纳点且允许任意多跳跃，若要在任意常数因子内近似 n 个点之间的所有成对距离，所需边数仍可能在多项式级别上大幅超过 n 条。在随机线性代数中，堆叠稀疏草图解决了2025 年的一项未决问题：在不塌缩 r 维子空间任何方向的前提下，将矩阵压缩至线性维度时打破了传统的稀疏度屏障，每行仅需 √log r 个非零元（比保留所有长度所需的 log r 实现了平方级减少），且近乎逼近了全新的理论下界。针对边权重会动态增删的加权图，Stellar Colosseum 解决了 FOCS 2022 遗留的公开问题，开发出首个用于割稀疏化的单遍流式算法，同时实现了接近最优的内存占用、更新时间与重构时间。

我们的研究成果还涵盖了优化理论、算术、数据结构与统计学。在优化理论方面，该方法解决了在线逆线性优化（根据专家在一段时间内的决策推断其隐藏目标）的未决难题，提出了一种确定性算法，在实现最优遗憾界的同时，将运行时间从维度的指数级直接降至多项式时间。针对 n 位整数乘法，多智能体协同将图灵机模型下的理论界限简化至 n log n 以下；另一项独立研究则在单一二维网格上给出了全新的 O(n log n) 算法，其 C 语言实现在高达 10 亿位时仍能与 GNU 多精度算术库（GMP）逐位保持一致。在数据结构方面，另一项成果对 Tarjan 于 1985 年提出的双端队列猜想（即自调整伸展树能否在均摊常数时间内处理两端的插入与删除）取得了重大突破，证明了单次操作开销的新上界，该界限同时优于所有有限次迭代的反阿克曼函数，且这一结论已在 Lean 4 中得到形式化验证。最后，在高维统计学领域，该方法证明了无需从头重新拟合模型的近似留一法交叉验证，在面对弹性网络等非光滑稀疏惩罚项时依然保持准确。

拓展形式化验证与论文评审规模

人工审查借助计算机完成的数学论文不仅给同行评审员带来沉重负担，冗长的推导计算中还容易潜藏细微漏洞。如果用 Lean 4 实现数学形式化，就能把证明转化为代码，交由计算机内核逐行验证。只要人类数学家确认形式化的定理表述与原问题完全吻合，那么唯有当每个逻辑步骤都完全成立时，证明代码才能编译通过。

许多极其深奥的数学未解之谜，关乎物理波如何传播、动力系统如何演化，以及多项式方程是否存在整数解。我们与 Google Cloud AI 的同事合作开发了多智能体框架 LEAP，并将其与 Argon 搭配使用；该框架可以直接基于非形式化的自然语言证明开展工作，目前已在这些核心数学领域取得突破。

值得一提的是，/teamwork-LEAP 完全自主地生成了韦伊猜想（Weil conjectures）的端到端、经机器检验的形式化证明。这一里程碑式的成果涉及有限域上多项式方程解的计数，最终由 Pierre Deligne 于 1974 年完成证明。该形式化成果跨越约 180 万行 Lean 代码，历经 28800 次子智能体调用方才完成。此外，该系统还合成了超过 91.9 万行 Lean 代码，首次完成了对一般整数环上希尔伯特第十问题最新证明的形式化验证。它还独立复现了一项最新证明的端到端形式化，该证明确立了带光滑外力的三维纳维-斯托克斯方程存在有限时间爆破，属于七大千禧年大奖难题之一，已悬而未决约 90 年。

不仅如此，该系统还首次形式化了自 1927 年悬置至今的动力系统难题——伯克霍夫猜想（Birkhoff conjecture）。它还首次形式化了调和分析的核心难题——困扰学界 50 多年的三维博赫纳-里斯猜想（3D Bochner–Riesz conjecture），并在此过程中发现并修复了近期一份非形式化证明中的漏洞。其他经过机器检验的突破还包括：解决了三维及更高维度下无穷调和函数的 C¹ 正则性（该问题已悬置约 20 年）；形式化了 Killip 和 Vişan 关于 KdV 水波方程在 H⁻¹ 中适定的定理；并验证了 UCLA 团队对已有 40 年历史的杰米森毛毛虫猜想（Jamison Caterpillar Conjecture）、Ağırseven-Ollis 猜想，以及对埃尔德什第 1063 号问题（Erdős Problem #1063）改进上界的非形式化证明。

最后，我们还为另一场计算机科学顶会的论文作者提供了 Deep Review 服务：在 STOC 2027 投稿阶段，共有 578 篇投稿（超过总投稿量的三分之一）的作者主动选择利用 Deep Review 获取初稿反馈。在目前进行的一项作者调研（样本量 N = 70）中，90% 的受访者认为反馈意见绝大部分或几乎全部属实，90% 表示愿意再次使用该工具。超过 30% 的受访者表示 Deep Review 发现了实质性的证明漏洞或具有数学意义的重要笔误，14% 的受访者称它找出了需要耗费一小时以上才能修复的技术缺陷。受访作者评价道：“这类工具能帮我们更快产出更严谨、更精确的研究成果”，并认为“DeepReview 为科学探索带来了安心保障”。我们每周向用户提供两次免费使用 Deep Review 的额度。Deep Review 也已作为 /teamwork 的文档审查模式上线，可在 Antigravity 中使用。欲了解更多关于 DeepReview 的细节，欢迎阅读我们的最新博文。

分子化学发现

除了形式化证明，将专用生成智能体与独立验证智能体相结合，还能在实验室实验科学中实现探索工作流。

根据实验核磁共振数据测定分子结构，是化学领域最棘手的难题之一。以HIV 蛋白酶抑制剂为例，仅仅一处化学键错位，就会让真正的药物沦为毫无活性的分子“仿品”。我们利用 /teamwork 和融合物理规律的光谱模拟器，将 30 个专用智能体组成自校正闭环，在复杂基准分子测试中取得了 95% 的 Top-1 精确匹配率以及 100% 的 Top-3 准确率，表现几乎是单智能体的两倍。这不仅让 Gemini 学会了推导分子结构，也为目前正在推进的 3D 蛋白质与复杂结构动力学研究打下了坚实基础。

除此以外，Gemini 4 博客文章中报道的核聚变应用和量子算法等科学难题，同样受益于 /teamwork 与 Argon 模型。

生成因果推断基准测试

我们也利用类似的多轮审计工作流来构建经验基准测试。以数据匿名化等人类设定的 5 项验收标准为起点，基于 Argon 运行的 29 个智能体耗时 11.5 小时，将 13 张公开数据表转化为了包含 50 个任务的因果推断基准测试。在这些任务中，模型必须判断因果效应是否可被识别，并对照已知答案给出预估值。初检过后，独立的评审与审计智能体会筛查投机取巧的行为、标记措辞提示并否决包含幻觉的脚本，最终将每个用例固化为正式测试项。这种原本重度依赖人工的任务生成过程实现自动化后，为训练 Gemini 解答反事实“假设（what-if）”问题提供了急需的高难度题目。

编程与系统工程

在与网络基准测试、游戏引擎、未经修改的测试套件以及硬件计时器等客观评估工具配合时，/teamwork 任务可以执行跨度数日的软硬件工程项目。

分布式系统

借助 /teamwork 和 Argon，我们基于 SNAP 微内核构建了低延迟内核旁路分区全局地址空间——FarArray。基于 FarArray 构建的应用包括无锁连通分量算法，该算法可扩展至万亿条边的图，相较于 TCP 键值存储，其吞吐量提升了 60 到 90 倍，运行速度提升了 40 到 180 倍，同时内存占用降低了 6 倍。类似地，InstantEmbedding（个性化 PageRank）相比加速版 MapReduce 实现，将 DRAM 峰值占用最高降低了 14 倍，运行时间缩短了 11 到 27 倍。团队还利用 /teamwork 和 Argon 为图神经网络开发了专用 TPU 内核，不仅使高带宽内存占用最高降低 185 倍，在前向和反向传播中也带来了 8 到 15 倍的加速。更多细节可参阅我们最新的 Antigravity 博客文章。

自主爬山优化

为了测试长周期的自主优化能力，Argon 上的爬山算法团队从基础版 AlphaZero 实现出发，从零训练出了一个 9x9 围棋引擎。人类研究员负责设定芯片分配方案与评估流程，自动化测试框架则自主运行多轮优化实验，大幅提升自我对弈效率（提速 2300 倍）与 Elo 评分测量速度，并且严格根据锁定记录上的统计检验来决出优胜版本。不到 8 天时间，该引擎的 Elo 积分就提升了约 2600 分，达到 1885 Elo，棋力介于每步搜索 16 次至 32 次的 KataGo 之间。

内存安全的 Rust 重写、/boost 以及 TPU 内核优化

在进行大规模代码迁移时，智能体往往会用桩函数糊弄依赖项，甚至篡改测试用例来让有缺陷的移植版本强行通过，导致迁移失败。即将在 Antigravity 中上线的全新 /teamwork 重写模式解决了这一难题：只有当某个模块的所有依赖项都编译通过后，系统才会排期处理该模块，同时让每个叶子模块都必须通过原版、未做任何修改的测试套件。在前期已完成 25% 移植的基础上，Argon 开展了为期两周的实验，将 Zircon 微内核剩余的 C++ 代码全部重写，新增了约 80 万行安全的 Rust 代码；这些代码不仅通过了所有内核单元测试，还能在 arm64 硬件上成功启动。此外，/teamwork 还将 Google 的 AV1 视频解码器 libgav1 从 C++ 重写为约 17 万行 Rust 代码，在广泛的一致性测试套件中实现了 100% 的逐比特完全一致。起初，该移植版本的运行速度只有原版 C++ 代码的四分之一左右。但在为 /teamwork 配备性能分析工具并要求其针对样本视频片段最大化提升性能后，该 Rust 移植版在 x86_64 和 ARM 架构上的运行速度反而比原版 C++ 和手工优化的汇编代码快了 20% 到 30%。

针对日常编程任务，Antigravity 的 /boost 命令封装了 /teamwork 的迭代编程模式。一项长期运行的 /teamwork 实验在分析了以往的运行轨迹后发现，处理紧耦合代码时，采用“顺序实现再逐级修订”的效果远好于“并行拆分”，这一发现进一步提升了 /boost 解决编程任务的效率。这也是一个测试框架为优化另一个测试框架的 Token 使用效率的典型范例。

在机器学习系统方面，针对自定义 JAX 和 Pallas TPU 内核进行完整的硬件评测每次需要 7 到 32 分钟，这严重限制了以往优化智能体所能探索的候选方案数量。通过在 Argon 上应用 /teamwork 的 DuoDiscover 模式，4 个并行智能体成功找出了性能瓶颈，并构建了只需 23 秒的快速代理评测工具（称为“标尺”）。这些标尺生成的候选方案排序，会通过肯德尔等级相关系数（Kendall's rank correlation）定期与完整的硬件运行结果进行交叉比对验证。在 17 个 JAXBench 内核上，DuoDiscover 相比基准实现的几何平均加速比达 4.09 倍；在针对前沿开源模型的 7 个手工优化版 vLLM TPU 推理 Pallas 内核上，也取得了 2.99 倍的几何平均加速比。

在 Google 基础设施中的应用

我们还将 /teamwork 和 /boost 应用到了 Google 内部的诸多生产基础设施与硬件建模难题中，其中包括：

• 全集群内存优化：在早期 Argon 内存优化工作的基础上，我们分析了全集群的各项指标以及内部过往的内存优化成功经验，构建起可复用的 /teamwork 工作流。该工作流发现的内存优化空间已经超过了我们最初预估的 1 PiB 节约量。此外，我们还部署了引入人在回路的“内存效率监控智能体”，利用消除结构体填充、标量缩窄、崖跳、外提以及标记指针等技术，实现了进一步的内存节省。
• Borg 智能体调度：基于 /teamwork 和 /boost 构建的 Borg 调度优化智能体工作流已完成两项重大变更上线。在保障工作负载 SLO 和集群利用率的同时，使部分硬件类型上的 TPU 工作负载抢占减少了 24%。

面向科研与开发者社区开放工具

外部科学家和开发者即日起即可在 Antigravity 和 Deep Review 中，将 Gemini 4 模型与 /teamwork 和 /boost 搭配使用。我们还开放了申请通道，将为 10,000 名学术研究人员提供为期六个月的最高等级免费使用权益。在接下来的更新中，我们还会把形式化证明范式以及更多专业工作流引入 Antigravity。未来几周，Antigravity 博客还将同步上线深度教程，确保开发者和研究人员拥有充足的资源来构建、检查和持续优化定制化的多智能体协作团队。除了模型本身，我们非常高兴能把这些工具也开放给所有人使用。

致谢

Antigravity 的 /teamwork 功能是 Google 内部多方通力协作与持续探索的成果。贡献者包括：Yuan Deng[279eb3]、Honghao Lin[279eb3]、Jieming Mao[279eb3]、Vahab Mirrokni[279eb3]、Vishnu Veeramachaneni[279eb3]、David Woodruff[279eb3]、Song Zuo[279eb3]、Shubham Agarwal、Santiago Balseiro、MohammadHossein Bateni、Mohsen Bayati、Garrett Bingham、Guy Blelloch、Douglas Chen、Vincent Cohen-Addad、Piaoyang Cui、Tulsee Doshi、Eric First、Michael Galkin、Elena Gribelyuk、Anupam Gupta、Guru Guruganesh、Mike Heddes、Patrick Heisel、Iman Hosseini、Kevin Hou、Lalit Jain、Adel Javanmard、Rajesh Jayaram、Xiaoen Ju、Po-Nien Kung、Silvio Lattanzi、Samuel Lavoie、Chun-Liang Li、Matthew Li、Yinan Li、Yuchen Li、Yiming Liu、Thang Luong、Brandon Mayer、Simon Meierhans、Swaroop Mishra、Ashish Naik、Sebastian Nowozin、Renato Paes Leme、Nikos Parotsidis、Ali Parviz、Neel Patel、Violet Peng、Bryan Perozzi、Anshul Ramachandran、Shashir Reddy、Lijie Ren、Madhavi Sewak、D Shin、Reza Shokri、Sukhdeep Singh、Samuel Smith、Linfeng Song、Dilara Soylu、Zheng Tan、Sasan Tavakkol、Hadi Tavassol、Yifeng Teng、Tom Wollschläger、Haifeng Xu、Zicheng Xu、Yihao Xue、Amir Yazdanbakhsh 以及 Goran Žužić。感谢 Carla Bromberg 和 Lauren Fraser 负责项目管理，感谢 Francis Duan、Pan-Pan Jiang、Xiyan Shao、Jane Shapiro、Weilun Shi 和 Xinyu Ye 对该项目作出的贡献。我们还要感谢各位领导的支持：Sergey Brin、Demis Hassabis、Koray Kavukcuoglu、Pushmeet Kohli、James Manyika、Yossi Matias、Varun Mohan 以及 Amin Vahdat。

多位学术合作者为这些研究论文做出了贡献：Zijie Chen、Amin Gohari、Chandra Nair (CUHK)、Songbin Liu、Arian Maleki、Chen Shang、Hanbo Yang、Wenjin Zhang (Columbia University)、Zihan Hao、Qipeng Liu、Jianan Shao (UCSD)、Lorenzo Beretta (IBM Cambridge)、Simone Bombari (BYU & Flatiron Institute)、Mahbod Majid、Margalit Glasgow (MIT)、Raphael Arkady Meyer (UC Berkeley, ICSI, & LBNL)、Kijun Shin (CMU)、Huacheng Yu、Elena Gribelyuk (Princeton University)、Xin Lyu (UCB/ ByteDance)、Samson Zhou (Texas A&M)、Erik Waingarten (UPenn)，以及 Sorrachai Yingchareonthawornchai (ETH-ITS)。