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