Науковий прорив Google Antigravity: формалізація теореми 1974 року в Lean і оптимізація ядра на Rust
Мультиагентна система допомогла формалізувати гіпотези Вейля та прискорити декодер відео на 20-30%
Google розширила мультиагентну систему Antigravity, яка тепер формалізує складні математичні теореми й переписує програмний код для прискорення роботи сервісів. Команда спеціалізованих агентів на базі моделей Gemini вже допомогла довести машинним способом знакову математичну теорему 1974 року, ідентифікувати молекулярні структури та прискорити роботу декодера відео, повідомляє Interesting Engineering. Технологія працює за принципом розподілу завдань між десятками окремих агентів, кожен з яких відповідає лише за свою частину роботи.
Найзначнішим досягненням виявилась повна машинна формалізація гіпотез Вейля - важливого набору результатів щодо кількості розв'язків поліноміальних рівнянь над скінченними полями. Оригінальний доказ французький математик П'єр Делінь опублікував у 1974 році, і тепер Google повідомляє про його повну машинну формалізацію. Для виконання цього завдання система Teamwork-LEAP створила близько 1,8 мільйона рядків коду мовою Lean, поділивши роботу на 28 800 звернень до субагентів.
Команда також відтворила формалізацію нещодавнього доказу про тривимірні рівняння Нав'є-Стокса, пов'язаного з однією із задач тисячоліття, а також допомогла довести гіпотезу Куртейда-Кумара з теорії інформації, сформульовану у 2013 році. Застосовуючи цей фреймворк, науковці з Google і партнерських університетів досягли доказу в повній загальності: моделі Gemini допомагали будувати аналітичні межі й формувати сертифікати, придатні для подальшої комп'ютерної перевірки.
В основі підходу - паралельна робота багатьох агентів замість одного великого модуля. Частина агентів формулює варіанти розв'язання, а інші налаштовані спеціально для того, щоб їх оскаржувати й перевіряти, - це покликано зменшити кількість помилок, які можуть з'являтися, коли один масивний ШІ- "ланцюжок міркувань" будує довгі й складні докази без незалежного контролю.
Систему застосували й поза математикою. Команда з 30 спеціалізованих агентів, поєднаних із фізично обґрунтованим симулятором, розв'язувала задачу ідентифікації молекулярних структур за даними ядерного магнітного резонансу. На складних тестових молекулах агенти досягли 95% точності у випадку найкращого варіанта та 100%, якщо враховувати три найімовірніші запропоновані структури.
Окремий напрям - перепис програмного забезпечення для приросту швидкодії. Агенти перетворили внутрішній відеодекодер AV1 libgav1, перенісши приблизно 170 000 рядків коду з C++ на Rust, і при цьому вихідні дані повністю збіглися на великому наборі тестів. Перша версія на Rust виявилася значно повільнішою за оригінал, проте після того, як агентам дали профайлінгові інструменти й окреме завдання підвищити продуктивність, Rust-реалізація стала на 20-30% швидшою за C++ як на x86_64, так і на ARM.
У іншому проєкті агенти переписали решту C++-коду мікроядра Zircon у приблизно 800 000 рядків Rust із безпечним керуванням пам'яттю, і ядро успішно пройшло модульні тести та завантажилося на апаратурі ARM64. За даними Google, агентний робочий процес планування дозволив скоротити примусове припинення завдань на TPU на 24% для деяких типів обладнання, не порушуючи при цьому встановлені рівні сервісу.
Google відкрила доступ до фреймворку науковцям
Компанія відкриває доступ до фреймворку Teamwork та ітераційного процесу написання коду /boost через платформу Antigravity. Google оголосила відбір 10 000 науковців, яким надасть шість місяців безкоштовного доступу до найвищого тарифного рівня використання системи. У майбутньому компанія планує додати до Antigravity більше спеціалізованих агентів для інших наукових і інженерних задач.
Раніше Інформатор повідомляв, що компанія запустила Gemini Decisions API - інструмент на базі моделі Gemini Decision 1, який одночасно оцінює до тисячі незалежних запитів за частки секунди й уже впроваджений у кілька сервісів компанії, зокрема Gemini Notebook і Google Search. Також ми писали, що співробітники лондонського офісу Google DeepMind виступили проти пункту в трудових угодах, який забороняє критику компанії довічно, вважаючи, що це змушує їх мовчати про ризики військового застосування штучного інтелекту.
Слідкуйте за нами у Telegram
Зараз читають на Інформаторі
