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 中可用。这使得团队能够根据过往运行记录设计自定义规范，跨不同的 harness 模式进行路由，并动态改进智能体 harness。虽然其中许多功能已在 Antigravity 中可用，但我们将在未来几周提供更多更新，向 Antigravity 的外部用户开放全部功能。继我们之前关于 Antigravity /teamwork 的文章之后，我们借助 /teamwork 和 Gemini 4 模型的新变体，为开放性挑战带来了新的成果。

数学与理论计算机科学

在数学和理论计算机科学领域，研究人员与 Gemini 4 及 /teamwork 框架协作，共同攻克大规模证明，并直接根据公开问题陈述生成完整的算法与证明。我们在此展示几个例子。

证明并验证 Courtade–Kumar 猜想

来自 Google、香港中文大学、南加州大学和 卡内基梅隆大学的研究人员使用 /teamwork 的 Long Proof 模式（在 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 年以来悬而未决的空白。这些界限首次为同时支持插入和删除的数据流提供了 近乎空间最优的算法，并能抵御自适应对手的攻击。在量子计算领域，一种新构造 解决了 2014 年的一个开放问题，首次找到了在常数误差下需要严格多于 n/2 次量子查询的 n 比特布尔函数，同时精确确定了各类对称函数的查询开销。

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

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

扩展形式化验证与论文评审

人工检查计算机辅助撰写的稿件给同行评审人员带来了沉重负担，而细微的缺陷可能隐藏在冗长的计算之中。在 Lean 4 中将数学形式化，可以把证明转化为计算机内核逐行检查的代码。一旦人类数学家确认形式化定理陈述与原始问题相符，只有当每个逻辑步骤都成立时，证明才能编译通过。

数学中许多最深刻的未解问题支配着物理波的传播方式、动力系统的演化方式，以及多项式方程是否存在整数解。我们的多智能体框架 LEAP 直接基于非形式化证明开展工作，它由我们与 Google Cloud AI 的同事共同开发，并与 Argon 配对使用，已在这些核心领域取得了进展。

值得注意的是，/teamwork-LEAP 完全自主地完成了对 韦伊猜想 的端到端、机器校验的形式化，这是关于有限域上多项式方程解计数的里程碑式成果，最终由 Pierre Deligne 在 1974 年完成证明。这一形式化横跨约 180 万行 Lean 代码，通过 28,800 次子智能体调用完成。该系统还合成了超过 91.9 万行 Lean 代码，首次对一个近期发表的、关于一般整数环上 希尔伯特第十问题 的证明进行了形式化。它还独立复现了对具有光滑强迫项的 三维 Navier–Stokes 方程 有限时间爆破这一近期证明的端到端形式化，该证明是七大 千禧年大奖难题 之一的一部分，悬置约 90 年。

除此之外，它还生成了 Birkhoff 猜想 的首个形式化结果，这是一个自 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 模型。

生成因果推断基准

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

编程与系统工程

当与网络基准测试、游戏引擎、未修改的测试套件和硬件计时器等客观评估器配合时，/teamwork 战役可以执行为期数天的软件和硬件工程项目。

分布式系统

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

自主爬山法

为了测试长周期自主优化，Argon 上的爬山团队从一个基础的 AlphaZero 实现出发，从零训练了一个 9x9 围棋引擎。人类研究员设定芯片分配和评估设置，而框架自主运行更快的自我对弈（实现 2,300 倍加速）和更快 Elo 读数的活动，严格通过对锁定记录的统计检验来晋升冠军。在不到八天时间里，该引擎提升了约 2,600 Elo，达到 1,885 Elo，介于每步 16 次和 32 次访问的 KataGo 之间。

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

大规模代码迁移失败的原因往往是智能体用桩替代依赖项，或者修改测试让有问题的移植通过。一种即将在 Antigravity 中推出的新 /teamwork 重写模式解决了这个问题：只有在某个模块的依赖项编译通过后才调度该模块，并将每个叶子模块与原始、未修改的测试套件链接。在 Zircon 微内核 最初 25% 移植的基础上，为期两周的 Argon 活动重写了其余的 C++ 代码，新增约 800,000 行安全的 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 在编码任务上的表现。这是一个框架为另一个框架优化 token 效率的例子。

对于机器学习系统，自定义 JAX 和 Pallas TPU 内核的完整硬件评估需要 7 到 32 分钟，限制了以往优化智能体能够探索的候选数量。通过在 Argon 上使用 /teamwork 的 DuoDiscover 模式，四个并行智能体识别出性能瓶颈，并构建了名为 yardstick 的快速 23 秒代理评估器。这些 yardstick 产生的候选排序会使用 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）中使用搭载 /teamwork 和 /boost 的 Gemini 4 模型。我们还开放了申请通道，为 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（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（普林斯顿大学）、Xin Lyu（UCB/ByteDance）、Samson Zhou（Texas A&M）、Erik Waingarten（UPenn），以及 Sorrachai Yingchareonthawornchai（ETH-ITS）。