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 的外部用户提供全部功能。继此前关于 Antigravity /teamwork 的文章之后，我们在此公布由 /teamwork 新变体和 Gemini 4 模型赋能、针对开放挑战取得的新成果。

数学与理论计算机科学

在数学与理论计算机科学领域，研究人员借助 Gemini 4 和 /teamwork 工具链协作完成大规模证明，并能直接从开放问题陈述出发，生成完整的算法与证明。我们在此展示几个例子。

证明并验证 Courtade–Kumar 猜想

来自 Google、CUHK、USC 和 CMU 的研究人员使用 /teamwork 的长证明模式（在 Antigravity 中实现 Stellar Colosseum），在完全一般的情形下证明了信息论中的2013 年 Courtade–Kumar 猜想。该结果确认：当随机比特串通过有噪信道时，把输入压缩成单个比特的任何做法，所保留的信息都不如“独裁函数”——它只是复制单个输入比特。Gemini 首先找到了 CUHK 团队早先论文中一个推广猜想的反例。随后 CUHK 团队提出了一个新的候选函数，把该猜想归结为一个 14 变量优化问题，并给出了一个关键的分析下界。接着，Gemini 4 Argon 和更早的 Gemini 模型划分了参数空间，推导出大部分新的分析界和区间算术证书。它们还在没有人工输入的情况下，把证明从平衡函数推广到了非平衡函数。团队在 Lean 4 中形式化了整个证明，生成了 5000 万行代码。

解决优化、统计、量子计算和算法领域的开放问题

研究人员还直接把开放问题交给 Gemini 4 以及 Stellar Colosseum、/teamwork 等多智能体工具链，得到了端到端的算法与证明（通常附带 Lean 4 形式化），并由作者验证、简化和编辑后发表。在自适应数据分析中，运行于 Gemini 4 Argon 的多智能体工具链独立证明并经 Lean 验证了近最优样本界，适用于根据先前答案自适应选择的统计查询，填补了自 2014 年以来悬而未决的空白。这些界给出了首个近乎空间最优的算法，可用于同时包含插入和删除的数据流，并且面对自适应对手时仍保持准确。在量子计算中，一项新构造解决了一个 2014 年的开放问题：它找到了首批在常数误差下需要严格多于 n/2 次量子查询的 n 比特布尔函数，同时精确确定了对称函数上的查询开销。

多项成果打破了处理与压缩大型矩阵和图结构长期存在的壁垒。在 STOC 2024 之前的五十年里，针对布尔矩阵乘法与三角形检测的组合算法（避开快速矩阵乘法中的代数消去）相比立方时间只节省了对数因子。一项新的确定性算法解决了 STOC 2024 的主要未解问题，实现了其相对于立方时间的目标加速。在高维几何中，一项新的下界解决了一个关于稀疏网络的未解问题，证明在任意常数因子内近似 n 个点之间的所有两两距离，可能需要多项式级多于 n 条边，即使允许额外的 Steiner 点和任意多跳。在随机线性代数中，堆叠稀疏草图解决了一个 2025 年未解问题，打破了将矩阵压缩到线性维度而不使 r 维子空间任何方向坍缩的经典稀疏性壁垒，每行只需 √log r 个非零元（比保持所有长度所需的 log r 平方级更少），并几乎匹配一个新的下界。对于动态边权插入与删除下的加权图，Stellar Colosseum 解决了 FOCS 2022 留下的一个未解问题，开发出首个割稀疏化的单遍流式算法，同时实现近最优的内存、更新时间和重建时间。

我们的成果还涵盖优化、算术、数据结构和统计学。在优化方面，针对在线逆线性优化（从随时间做出的决策中推断专家的隐藏目标）的一个未解问题，该方法给出了一个确定性算法，在达到最优遗憾的同时将运行时间从随维度指数增长降至多项式时间。对于 n 位整数乘法，多智能体协作将理论图灵机界简化到 n log n 以下，而另一项工作则在单个二维网格上给出了新的 O(n log n) 算法，其 C 实现与 GNU 多精度算术库（GMP）在高达十亿位时逐位一致。在数据结构方面，另一项成果在 Tarjan 1985 年的双端队列猜想（自调整伸展树能否以常数摊还时间处理两端的插入和删除）上取得重大进展，证明了每次操作开销的一个新上界，同时优于所有有限次迭代的逆 Ackermann 函数，并在 Lean 4 中完成验证。最后，在高维统计中，该方法证明了近似留一交叉验证（避免从头重新拟合模型）对于像弹性网这样的非光滑稀疏惩罚仍然准确。

扩展形式化验证与稿件评审

人工检查计算机辅助的稿件会给同行评审带来沉重负担，而细微的缺陷又可能藏在冗长的计算之中。用 Lean 4 把数学形式化，就能将证明变成代码，由计算机内核逐行检查。一旦人类数学家确认形式化的定理陈述与原问题一致，那么只有每一步逻辑都成立，证明才能通过编译。

数学中许多最深刻的未解问题，关乎物理波如何传播、动力系统如何演化，以及多项式方程是否有整数解。我们的多智能体框架 LEAP 与 Google Cloud AI 的同事共同开发，并与 Argon 配合，直接从非形式化证明出发，在这些核心领域取得了进展。

值得一提的是，/teamwork-LEAP 完全自主地端到端产出了韦伊猜想的机器可检验形式化，这是关于有限域上多项式方程解计数的里程碑成果，最终由 Pierre Deligne 于 1974 年完成证明。这次形式化约含 180 万行 Lean 代码，由 28,800 次子智能体调用生成。系统还合成了超过 91.9 万行 Lean 代码，首次形式化了一般整数环上希尔伯特第十问题近期证明。它还独立复现了三维纳维–斯托克斯方程在光滑外力下有限时间爆破的近期证明的端到端形式化，该问题属于七大千禧年大奖难题之一，已悬置约 90 年。

除此之外，它还首次形式化了伯克霍夫猜想，这是一个自 1927 年起悬而未决的动力系统问题。它还首次形式化了三维 Bochner–Riesz 猜想，这是调和分析中悬置 50 多年的核心问题，过程中还发现并修复了近期一份非形式化证明中的一处漏洞。其他经机器检验的突破还包括：解决了三维及更高维无穷调和函数的 C¹ 正则性（悬置约 20 年），形式化了 Killip 与 Vişan 的定理——KdV 水波方程在 H⁻¹ 中适定，并验证了 UCLA 团队对已有 40 年历史的 Jamison 毛毛虫猜想、Ağırseven-Ollis 猜想以及 Erdős 第 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模型。

生成因果推断基准

我们还应用了类似的多轮审计工作流来构建实证基准。从数据匿名化等五项人工指定的验收标准出发，29个在Argon上运行的智能体历时11.5小时，将13张公开表格转化为一个包含50项任务的因果推断基准。在这些任务中，模型必须判断因果效应是否可识别，并对照已知答案进行估计。经过初步检查后，独立的评审员和审计员智能体捕获了捷径、标记了措辞提示，并否决了幻觉脚本，将每一项都转化为永久性测试。自动化这项高度人工化的任务生成工作，提供了帮助Gemini回答反事实“假设”问题所需的难题。

编码与系统工程

当与网络基准、游戏引擎、未经修改的测试套件和硬件计时器等客观评估器配对时，/teamwork活动可以执行持续多日的软件和硬件工程项目。

分布式系统

利用/teamwork和Argon，我们构建了FarArray，这是一个基于SNAP微内核的低延迟内核旁路分区全局地址空间。基于FarArray的应用包括无锁连通分量，可扩展到万亿条边的图，相比TCP键值存储，吞吐量提升60倍至90倍，速度提升40倍至180倍，内存占用降低6倍。同样，InstantEmbedding（个性化PageRank）相比加速的MapReduce实现，峰值DRAM降低最多14倍，运行时间缩短11倍至27倍。团队还使用/teamwork和Argon为图神经网络创建了自定义TPU内核，实现了最高185倍的高带宽内存减少，以及前向和后向传播8倍至15倍的速度提升。更多细节请参见我们近期的Antigravity博客文章。

自主爬山

为了测试长周期下的自主优化能力，Argon 上的爬山团队从零开始训练了一个 9x9 的围棋引擎，起点是一个基础的 AlphaZero 实现。人类研究员负责设定芯片分配和评估方案，而 harness 则自主运行多轮实验，加快自对弈速度（实现了 2,300 倍加速）并更快读取 Elo 分数，严格依据锁定记录上的统计检验来晋升优胜版本。不到八天，该引擎的 Elo 提升了约 2,600 分，达到 1,885 Elo，介于每步 16 次访问和 32 次访问的 KataGo 之间。

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

大规模代码迁移常常失败，因为智能体会把依赖项留成空壳，或者改动测试，让有问题的移植版本通过。一种新的 /teamwork 重写模式（即将在 Antigravity 中提供）解决了这个问题：每个模块只在其依赖项编译通过后才被调度，并且每个叶子模块都链接到原始、未经修改的测试套件。在 Zircon 微内核最初 25% 移植成果的基础上，一次为期两周的 Argon 实验重写了剩余的 C++ 代码，新增约 80 万行安全 Rust 代码，通过了全部内核单元测试，并能在 arm64 硬件上启动。/teamwork 还将 Google 的 AV1 视频解码器 libgav1 从 C++ 重写为约 17 万行 Rust，在广泛的一致性测试套件上实现了 100% 位精确一致。起初，移植版本比原始 C++ 代码慢约 4 倍。但在让 /teamwork 使用性能分析工具，并要求它在示例视频片段上尽可能提升速度之后，Rust 移植版在 x86_64 和 ARM 上都比原始 C++ 和手工优化的汇编代码快 20-30%。

对于日常编码任务，Antigravity 的 /boost 命令封装了 /teamwork 的迭代编码模式。一次长期运行的 /teamwork 实验分析了过往运行轨迹，发现紧耦合的代码最好通过顺序实现和修订阶段来处理，而不是并行拆分，这提升了 /boost 在编码任务上的表现。这是一个 harness 为节省 token 而优化另一个 harness 的例子。

对于机器学习系统，对自定义 JAX 和 Pallas TPU 内核进行完整的硬件评估需要 7 到 32 分钟，这限制了此前的优化智能体能够探索的候选方案数量。在 Argon 上使用 /teamwork 的DuoDiscover 模式，四个并行智能体识别出性能瓶颈，并构建了耗时仅 23 秒的快速代理评估器，称为 yardsticks。这些 yardsticks 生成候选方案的排序，并通过 Kendall 秩相关与定期进行的完整硬件运行结果持续校验。DuoDiscover 在 17 个 JAXBench 内核上相比参考实现取得了 4.09 倍的几何平均加速，在 7 个针对前沿开放权重模型手工优化的 vLLM TPU-Inference Pallas 内核上取得了 2.99 倍的几何平均加速。

Google 基础设施应用

我们还将 /teamwork 和 /boost 应用于 Google 内许多生产基础设施和硬件建模问题。例子包括：

• 全集群内存优化：在早期 Argon 内存工作的基础上，我们分析了全集群指标以及内部以往内存节省的成功经验，创建了可复用的 /teamwork 工作流，找出了多处内存节省机会，超出我们最初 1 PiB 的节省预估。我们还部署了带人工审核环节的内存效率监控智能体，通过消除结构体填充、标量收窄、cliff jumping、outlining、带标签指针等技术，进一步节省了内存。
• Borg 智能体调度：基于 /teamwork 和 /boost 构建的 Borg 调度优化智能体工作流已成功上线 2 项变更，使部分硬件类型上的 TPU 工作负载抢占率降低 24%，同时保持了工作负载 SLO 和集群利用率。

向研究者和开发者社区开放这些工具

外部科学家和开发者现在可以在 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（香港中文大学），Songbin Liu、Arian Maleki、Chen Shang、Hanbo Yang、Wenjin Zhang（哥伦比亚大学），Zihan Hao、Qipeng Liu、Jianan Shao（加州大学圣地亚哥分校），Lorenzo Beretta（IBM 剑桥），Simone Bombari（杨百翰大学 & 熨斗研究所），Mahbod Majid、Margalit Glasgow（麻省理工学院），Raphael Arkady Meyer（加州大学伯克利分校、ICSI & 劳伦斯伯克利国家实验室），Kijun Shin（卡内基梅隆大学），Huacheng Yu、Elena Gribelyuk（普林斯顿大学），Xin Lyu（加州大学伯克利分校/字节跳动），Samson Zhou（德州农工大学），Erik Waingarten（宾夕法尼亚大学），以及 Sorrachai Yingchareonthawornchai（ETH-ITS）。