IT之家 11 月 14 日消息，谷歌宣布进一步扩展旗下 Antigravity 多智能体系统，利用多个由 Gemini 模型驱动的专业智能体组成 Teamwork 系统，号称可解决“长期悬而未决的数学难题”、“验证复杂数学证明”，并优化各种软件系统性能。 例如，谷歌已成功对韦伊猜想（Weil conjectures）进行形式化证明。这是一组关于有限域上多项式方程解的数量的重要数学结论，最初由数学家皮埃尔 · 德利涅（Pierre Deligne）于 1974 年证明。谷歌 Teamwork-LEAP 系统通过约 2.88 万次子智能体调用，累计生成约 180 万行 Lean 代码，完成了相关数学成果的形式化工作。 谷歌还表示，相应系统近期还成功复现了一项关于三维纳维-斯托克斯方程（Navier–Stokes equations）有限时间爆破问题的形式化证明。并帮助研究人员解决了库尔塔德-库马尔猜想（Courtade–Kumar conjecture）。 从技术层面，谷歌 Teamwork 系统主要依靠多个智能体并行工作，并安排独立系统对提出的解答进行质疑和验证，以减少单个 AI 模型在生成长篇推理过程中可能出现的错误。每个专业智能体只能访问完成任务所需的文件和工具，随后由独立的质疑者和审查者检查结果，而不依赖原始智能体的推理过程。 除了数学研究，谷歌还将这套技术应用于分子化学领域。一支由 30 个专业智能体组成的团队，配合融入物理知识的模拟器，利用核磁共振（NMR）数据识别分子结构。在复杂分子基准测试中，该系统的 Top-1 准确率达到 95%，Top-3 准确率达到 100%。 在系统工程领域，谷歌也展示了多智能体协作的应用成果。该公司表示，其智能体团队将自家的 libgav1 AV1 视频解码器从 C++ 重写为 Rust，最终生成约 17 万行代码，并在一套覆盖范围广泛的测试中实现了与原始版本完全一致的输出结果。 目前，谷歌正通过 Antigravity 向用户开放 Teamwork 系统，以及名为 /boost 的迭代式编程工作流，计划向 1 万名学术研究人员提供为期 6 个月的最高使用额度免费访问权限。
谷歌利用多个专业 AI 智能体打造 Teamwork 系统，成功验证多项复杂数学证明
IT之家 11 月 14 日消息，谷歌宣布进一步扩展旗下 Antigravity 多智能体系统，利用多个由 Gemini 模型驱动的专业智能体组成 Teamwork 系统，号称可解决“长期悬而未决的数学难题”、“验证复杂数学证明”，并优化各种软件系统性能。 例如，谷歌已成功对韦伊猜想（Weil conjectures）进行形式化证明。这是一组关于有限域上多项式方程解的数量的重要数学结论，最初由数学家皮埃尔 · 德利涅（Pierre Deligne）于 1974 年证明。谷歌 Teamwork-LEAP 系统通过约 2.88 万次子智能体调用，累计生成约 180 万行 Lean 代码，完成了相关数学成果的形式化工作。 谷歌还表示，相应系统近期还成功复现了一项关于三维纳维-斯托克斯方程（Navier–Stokes equations）有限时间爆破问题的形式化证明。并帮助研究人员解决了库尔塔德-库马尔猜想（Courtade–Kumar conjecture）。 从技术层面，谷歌 Teamwork 系统主要依靠多个智能体并行工作，并安排独立系统对提出的解答进行质疑和验证，以减少单个 AI 模型在生成长篇推理过程中可能出现的错误。每个专业智能体只能访问完成任务所需的文件和工具，随后由独立的质疑者和审查者检查结果，而不依赖原始智能体的推理过程。 除了数学研究，谷歌还将这套技术应用于分子化学领域。一支由 30 个专业智能体组成的团队，配合融入物理知识的模拟器，利用核磁共振（NMR）数据识别分子结构。在复杂分子基准测试中，该系统的 Top-1 准确率达到 95%，Top-3 准确率达到 100%。 在系统工程领域，谷歌也展示了多智能体协作的应用成果。该公司表示，其智能体团队将自家的 libgav1 AV1 视频解码器从 C++ 重写为 Rust，最终生成约 17 万行代码，并在一套覆盖范围广泛的测试中实现了与原始版本完全一致的输出结果。 目前，谷歌正通过 Antigravity 向用户开放 Teamwork 系统，以及名为 /boost 的迭代式编程工作流，计划向 1 万名学术研究人员提供为期 6 个月的最高使用额度免费访问权限。