Google расширяет возможности науки и инженерии с командной работой /teamwork в Antigravity

Источник: research.google

Google описывает работу системы как сотрудничество людей и ИИ: специалисты формулируют задачу и задают теоретические или физические ограничения, а ИИ-агенты пишут решатели, исследуют варианты, проверяют решения и связывают длинные цепочки рассуждений. В проектах участвовали команды Google и академические партнёры. За последние недели они взялись за задачи, которые оставались нерешёнными годами, и получили результаты в теории информации, формальной верификации, поиске молекулярных структур и оптимизации ядер операционных систем.

Для проверки кандидатов система использует независимые инструменты: проверяющую доказательства систему Lean 4, неизменённые наборы программных тестов, симуляторы выполнения, поиск в интернете и аппаратные счётчики. Агентам также ограничивают контекст: каждый получает только нужные для своего шага файлы и инструменты. Координаторы передают работу новым агентам, а критики и аудиторы проверяют результаты в отдельных контекстах, не опираясь на ход рассуждений автора решения.

Как устроена /teamwork

Система направляет запрос пользователя в подходящий рабочий шаблон. Среди них — параллельная разработка кода, последовательное решение с проверкой, длинные доказательства и анализ документов. Команда /boost отдельно упаковывает последовательный цикл решения и проверки для повседневных задач по программированию.

Google говорит, что многие из этих возможностей уже доступны в Antigravity, а новые функции для внешних пользователей компания будет добавлять в ближайшие недели. Среди новых результатов, представленных в публикации, — задачи, решённые с помощью вариантов /teamwork и моделей Gemini 4.

Математика и информатика

Исследователи из Google, CUHK, USC и CMU с помощью шаблона Long Proof в /teamwork доказали в полной общности гипотезу Кортаде—Кумара, сформулированную в 2013 году. Она касается передачи случайной битовой строки через шумный канал: согласно гипотезе, никакое сжатие входа до одного бита не сохраняет больше информации, чем диктаторская функция, которая копирует один из входных битов.

Сначала Gemini нашла контрпримеры к обобщённой гипотезе из более ранней работы команды CUHK. Затем исследователи предложили новую функцию-кандидат, сведя задачу к оптимизации по 14 переменным и получив важную аналитическую нижнюю оценку. Gemini 4 Argon и более ранние модели разделили пространство параметров и вывели большую часть новых аналитических оценок и сертификатов интервальной арифметики. Без участия людей они также распространили доказательство со сбалансированных функций на несбалансированные. Полное доказательство команда формализовала в Lean 4: оно заняло 50 миллионов строк кода.

В других задачах по математике, статистике и информатике исследователи задавали открытые вопросы Gemini 4 и системам Stellar Colosseum и /teamwork. Полученные алгоритмы и доказательства, в том числе формализованные в Lean 4, авторы проверяли, упрощали и редактировали перед публикацией.

Формальная проверка доказательств

Ручная проверка рукописи с компьютерными вычислениями усложняет работу рецензентов, а ошибки могут скрываться в длинных выкладках. Формализация в Lean 4 превращает доказательство в код, который проверяет компьютерное ядро. После того как математики подтверждают соответствие формального утверждения исходной задаче, доказательство компилируется только при корректности каждого логического шага.

Разработанный вместе с коллегами из Google Cloud AI мультиагентный фреймворк LEAP, работающий с Gemini 4 Argon, применили к задачам о распространении физических волн, динамических системах и целочисленных решениях полиномиальных уравнений.

Система /teamwork-LEAP полностью автономно подготовила сквозную формализацию гипотез Вейля — результатов о подсчёте решений полиномиальных уравнений над конечными полями, кульминацией которых стало доказательство Пьера Делиня в 1974 году. Формализация заняла около 1,8 миллиона строк Lean и потребовала 28 800 запусков подчинённых агентов. Система также синтезировала более 919 000 строк Lean, чтобы впервые формализовать недавнее доказательство десятой проблемы Гильберта над общими кольцами целых чисел.

Кроме того, система независимо воспроизвела полную формализацию недавнего доказательства существования решения уравнений Навье—Стокса в трёх измерениях, которое за конечное время становится неограниченным при гладком внешнем воздействии. Эта задача входит в семь проблем тысячелетия и оставалась открытой около 90 лет.

Среди других результатов — первая формализация гипотезы Биркгофа о динамических системах, открытой с 1927 года, и гипотезы Бохнера—Рисса для трёхмерного пространства, одной из центральных задач гармонического анализа, остававшейся открытой более 50 лет. При работе над второй системой обнаружила и исправила пробел в недавно опубликованном неформальном доказательстве. Она также разрешила вопрос о регулярности класса C¹ для бесконечно-гармонических функций в трёх и более измерениях — он был открыт около 20 лет, — формализовала теорему Киллипа и Вишана о корректности уравнения Кортевега—де Фриза в H⁻¹ и проверила неформальные доказательства группы UCLA для гипотезы «Гусеницы» Джеймисона, которой 40 лет, гипотезы Агырсевена—Оллиса и улучшенной верхней оценки для задачи Эрдёша № 1063.

Перед конференцией STOC 2027 авторы 578 статей, то есть более трети всех заявок, согласились получить отзывы Deep Review на свои черновики. В продолжающемся опросе авторов (N = 70) 90% респондентов оценили отзывы как в основном или почти полностью фактические, а 90% заявили, что воспользовались бы инструментом снова. Более 30% сообщили, что Deep Review обнаружила существенные ошибки в доказательствах или математически значимые опечатки; 14% — что система нашла технические пробелы, на исправление которых ушло больше часа. Авторы также отмечали, что подобные инструменты могут помочь быстрее готовить более точные исследования и дают уверенность в научных результатах. Пользователям предоставляют два бесплатных обращения к Deep Review в неделю. Инструмент также доступен в Antigravity как шаблон анализа документов для /teamwork.

Поиск структуры молекул

Определение структуры молекулы по экспериментальным данным ядерного магнитного резонанса — одна из сложных задач химии. В случае ингибиторов протеазы ВИЧ одна неправильно расположенная связь может отличить лекарство от неактивной молекулы, похожей на него.

Google объединила 30 специализированных агентов в самокорректирующийся цикл /teamwork и подключила физически обоснованный симулятор спектров. На сложных молекулах из бенчмарка система достигла точности 95% при выборе одного лучшего варианта и 100% среди трёх лучших — почти вдвое выше результата одного агента. Работа закладывает основу для дальнейших исследований динамики белков и сложных структур в трёх измерениях. Google также сообщает, что /teamwork и модель Argon помогли в задачах ядерного синтеза и квантовых алгоритмов, о которых рассказано в публикации о Gemini 4.

Бенчмарк причинно-следственных выводов

Google использовала многоэтапную проверку и для подготовки эмпирического бенчмарка. На основе пяти заданных людьми критериев, включая анонимизацию данных, 29 агентов на Argon за 11,5 часа превратили 13 общедоступных таблиц в бенчмарк из 50 задач по причинно-следственным выводам.

В каждой задаче модели должны определить, можно ли установить причинный эффект, и оценить его, зная правильный ответ. После первичных проверок отдельные агенты-рецензенты и аудиторы обнаруживали упрощённые обходные пути, подсказки в формулировках и вымышленные сценарии. Найденные проблемы превращали в постоянные тесты. Автоматизация помогла подготовить сложные задачи, необходимые для ответов Gemini на контрфактические вопросы «что, если».

Разработка ПО и системная инженерия

В проектах по разработке ПО и оборудования /teamwork сочетает длительные автономные кампании с объективной проверкой: сетевыми бенчмарками, игровыми движками, неизменёнными наборами тестов и аппаратными таймерами.

Распределённые системы

С помощью /teamwork и Argon Google создала FarArray — низколатентную систему с обходом ядра, построенную на модели распределённого глобального адресного пространства и микроядре SNAP. На FarArray работают, среди прочего, алгоритмы поиска связных компонент без блокировок. Они масштабируются до графов с одним триллионом рёбер, обеспечивая пропускную способность в 60–90 раз выше и ускорение в 40–180 раз по сравнению с хранилищами ключей и значений на TCP при в шесть раз меньшем объёме оперативной памяти.

Система InstantEmbedding для персонализированного PageRank сократила пиковое использование динамической памяти до 14 раз, а время работы — в 11–27 раз относительно ускоренных реализаций MapReduce. Команда также разработала с помощью /teamwork и Argon пользовательские ядра TPU для графовых нейронных сетей. Они уменьшили расход памяти с высокой пропускной способностью до 185 раз и ускорили прямой и обратный проходы в 8–15 раз.

Автономная оптимизация игры в го

Для проверки длительной автономной оптимизации команда на Argon обучила с нуля движок го на доске 9×9, начав с базовой реализации AlphaZero. Люди задали распределение вычислительных ресурсов и схему оценки, после чего система самостоятельно ускоряла самообучение и вычисление рейтинга Эло. Победителей выбирали только статистическими тестами на закрытых записях партий.

Самообучение ускорилось в 2300 раз. Менее чем за восемь дней рейтинг движка вырос примерно на 2600 пунктов и достиг 1885 — между результатами KataGo при 16 и 32 посещениях на ход. Для публикации сыграли одну партию между итоговым чемпионом чёрными и сетью, с которой началась оптимизация рейтинга Эло, белыми. Чемпион выиграл 22,5 очка при подсчёте по территории и коми 7,5.

Перенос кода на Rust и оптимизация TPU

Перенос крупных кодовых баз может провалиться, если агенты заменяют зависимости заглушками или меняют тесты, чтобы скрыть ошибки. Новый шаблон /teamwork, который скоро появится в Antigravity, запускает работу над модулем только после сборки его зависимостей. Каждый конечный модуль проверяется с исходным, не изменённым набором тестов.

После первоначального переноса 25% микроядра Zircon двухнедельная кампания на Argon переписала оставшийся код на C++: добавила около 800 000 строк безопасного Rust, прошедших все модульные тесты ядра и загружающихся на оборудовании arm64. /teamwork также переписала декодер видео AV1 libgav1 от Google с C++ на примерно 170 000 строк Rust. Новая версия побитово совпала с исходной на всём широком наборе тестов соответствия. Сначала перенос работал примерно в четыре раза медленнее оригинала. После того как системе дали средства профилирования и задачу максимизировать скорость на коротких видеороликах, версия на Rust стала на 20–30% быстрее оригинального C++ и кода на ассемблере, оптимизированного вручную, на x86_64 и ARM.

Для повседневных задач команда /boost в Antigravity использует итеративный подход /teamwork к программированию. Анализ прошлых запусков показал, что тесно связанный код лучше писать и пересматривать последовательно, а не делить параллельно на части. На основе этого анализа Google улучшила /boost для задач по программированию. Это пример того, как один рабочий шаблон оптимизирует другой с точки зрения расхода токенов.

Полная оценка пользовательских ядер JAX и Pallas для TPU занимает от 7 до 32 минут, поэтому алгоритмы оптимизации успевают проверить ограниченное число вариантов. В шаблоне DuoDiscover на Argon четыре параллельных агента нашли узкие места и создали быстрые оценщики — «мерные линейки», — работающие за 23 секунды. Они ранжируют кандидатов, а результаты регулярно сверяют с полноценными запусками на оборудовании с помощью ранговой корреляции Кендалла.

DuoDiscover показала среднее геометрическое ускорение в 4,09 раза относительно эталонных реализаций на 17 ядрах JAXBench и в 2,99 раза на семи вручную оптимизированных ядрах Pallas для вывода на TPU с помощью vLLM для передовых моделей с открытыми весами.

Применение в инфраструктуре Google

Google применяла /teamwork и /boost и для производственных задач и моделирования оборудования. В оптимизации памяти для всего парка систем команда проанализировала внутренние показатели и прошлые успешные решения по снижению расхода памяти, а затем создала переиспользуемые рабочие процессы. Они нашли возможности для экономии, превысив первоначальную оценку в 1 PiB. Дополнительную экономию обеспечил агент мониторинга эффективности памяти, который работает с участием человека. Среди применённых методов — удаление выравнивания структур, сужение скалярных типов, использование скачков между уровнями выделения памяти, выделение фрагментов кода и тегированные указатели.

В Borg также запустили рабочий процесс оптимизации планирования на базе /teamwork и /boost. Он привёл к внедрению двух изменений: на некоторых типах оборудования вытеснение задач TPU снизилось на 24% при сохранении целевых показателей уровня обслуживания и загрузки кластера.

Доступ для исследователей и разработчиков

Внешние исследователи и разработчики уже могут использовать модели Gemini 4 вместе с /teamwork, /boost и Deep Review в Antigravity. Google также открыла приём заявок на шесть месяцев бесплатного доступа к своему старшему тарифу для 10 000 академических исследователей.

В следующих обновлениях в Antigravity добавят шаблон формального доказательства и другие специализированные рабочие процессы. В ближайшие недели Google обещает опубликовать подробные учебные материалы в блоге Antigravity, чтобы помочь разработчикам и исследователям создавать, проверять и постепенно улучшать собственные мультиагентные команды.

Участники

Работа над /teamwork объединила сотрудников Google и академических партнёров. Среди основных участников из Google названы Юань Дэн, Хунхао Линь, Цзимин Мао, Вахаб Миррокни, Вишну Вираманчанени, Дэвид Вудрафф, Сун Цзо, Шубхам Агарвал, Сантьяго Бальсейро, Мохаммадхоссейн Батени, Мохсен Баяти, Гарретт Бингем, Гай Блеллок, Дуглас Чен, Винсент Коэн-Аддад, Поян Цуй, Тулси Доши, Эрик Фёрст, Майк Галкин, Елена Грибылик, Анупам Гупта, Гуру Гуруганеш, Майк Хеддес, Патрик Хайзель, Иман Хоссейни, Кевин Хоу, Лалит Джейн, Адель Джаванмард, Раджеш Джаярам, Сяоэнь Цзюй, По-Ньен Кун, Сильвио Латтанци, Сэмюэл Лавуа, Чун-Лян Ли, Мэттью Ли, Инань Ли, Юйчэнь Ли, Имин Лю, Тханг Лыонг, Брэндон Майер, Симон Майерханс, Сваруп Мишра, Ашиш Наик, Себастьян Новозин, Ренато Паэс Леме, Никос Паротсидис, Али Парвиз, Нил Патель, Вайолет Пэн, Брайан Пероцци, Аншул Рамачандран, Шашир Редди, Лицзе Жэнь, Мадхави Севак, Ди Шин, Реза Шокри, Сукхдип Сингх, Сэмюэл Смит, Линьфэн Сун, Дилара Сойлу, Чжэн Тань, Сасан Таваккол, Хади Тавассол, Ифэн Тэн, Том Волльшлегер, Хайфэн Сюй, Чжичэн Сюй, Ихао Сюэ, Амир Язданбакш и Горан Жужич.

За управление программой отвечали Карла Бромберг и Лорен Фрейзер; вклад в проект также внесли Фрэнсис Дуан, Пань-Пань Цзян, Сиянь Шао, Джейн Шапиро, Вэйлунь Ши и Синьюй Е. Среди поддержавших проект руководителей Google названы Сергей Брин, Демис Хассабис, Корай Кавукчуоглу, Пушмит Коли, Джеймс Маньика, Йосси Матиас, Варун Мохан и Амин Вахдат.

В исследованиях участвовали академические партнёры Цзецзе Чен, Амин Гохари и Чандра Наир из CUHK; Сунбин Лю, Ариан Малекі, Чэнь Шан, Ханьбо Ян и Вэньцзинь Чжан из Columbia University; Цзыхань Хао, Ципэн Лю и Цзянань Шао из UCSD; Лоренцо Беретта из IBM Cambridge; Симоне Бомбари из BYU и Flatiron Institute; Махбод Маджид и Маргалит Глазго из MIT; Рафаэль Аркади Мейер из UC Berkeley, ICSI и LBNL; Ки Джун Шин из CMU; Хуачэн Юй и Елена Грибылик из Princeton University; Синь Лю из UCB и ByteDance; Сэмсон Чжоу из Texas A&M; Эрик Вайнгартен из UPenn; Соррачай Йингчарнтхаворнчай из ETH-ITS.

По оценке Dataist, Google показывает /teamwork как набор проверяемых рабочих процессов для исследований и инженерии: результаты опираются на внешние тесты, формальные доказательства и проверки людей. При этом доступность функций для внешних пользователей будет расширяться постепенно, а некоторые специализированные шаблоны пока только готовятся к запуску.