Google рассказала о результатах развития платформы Teamwork для Antigravity, в которой над одной задачей одновременно работают несколько специализированных ИИ-агентов. Одни системы ищут решения, другие проверяют вычисления, а третьи независимо оценивают результаты, снижая вероятность ошибок.
Одним из главных достижений стала формализация гипотез Вейля — фундаментальных математических результатов, доказанных Пьером Делинем в 1974 году. Для их машинной проверки система Teamwork-LEAP сгенерировала около 1,8 миллиона строк кода на языке Lean, выполнив 28 800 обращений к вспомогательным агентам.
Кроме того, ИИ помог исследователям получить доказательство гипотезы Куртаде — Кумара из теории информации, предложенной в 2013 году. Результат был формализован в Lean 4, что позволило проверить математические рассуждения компьютерными средствами. Система также использовалась для формализации исследований, связанных с уравнениями Навье — Стокса, хотя знаменитая задача тысячелетия об их глобальной регулярности по-прежнему остаётся нерешённой.
В химии команда из 30 ИИ-агентов смогла определять молекулярные структуры по данным ядерного магнитного резонанса. По информации Google, точность первого предложенного варианта достигла 95%, а при рассмотрении трёх вариантов — 100% на использованном наборе сложных молекул.
Не менее интересные результаты получены в программировании. Агенты переписали видеодекодер libgav1 с C++ на Rust, создав около 170 тысяч строк кода. Первоначально новая версия работала в четыре раза медленнее оригинала, но после оптимизации оказалась на 20–30% быстрее на процессорах x86_64 и ARM.
В другом эксперименте ИИ за две недели переписал около 800 тысяч строк кода микроядра Zircon на Rust. Полученная версия прошла модульные тесты и успешно загрузилась на оборудовании ARM64.
Google уже открыла доступ к Teamwork через Antigravity и предложила 10 тысячам научных исследователей возможность получить шестимесячный бесплатный доступ к максимальному тарифному плану. В дальнейшем компания намерена расширять набор инструментов для научных вычислений, программирования и автоматической проверки результатов.
Читать TechDigest в Google
