ИИ проверил математикой часть кода Signal за полдня и $500 вместо 5 месяцев

Исследовательница Стэнфорда Chuyue Sun с коллегами создала ИИ-инструмент, который меньше чем за полдня и меньше чем за $500 выполнил инженерный проект: проверил часть кода, шифрующего переписку в мессенджере Signal. Трое высококвалифицированных специалистов на такую же работу вручную потратили пять месяцев. Проверка была не обычной, а формальной: программу не прогоняют через тысячи тестов, а математически доказывают, что она ведёт себя так, как задумано. Идея старая, но до сих пор она была слишком дорогой и медленной. Теперь на неё ставят стартапы с сотнями миллионов долларов и крупные ИИ-лаборатории.

Почему математика вместо тестов

Обычное тестирование показывает, что программа не сломалась в тех случаях, которые ей подсунули. Формальная верификация доказывает, что она не сломается ни в каком случае из описанного класса. Инженеры пишут точные утверждения о цели программы, затем переводят код в формулы, которые проверяют специальные системы. Среди таких систем Lean, Rocq и Isabelle.

Но работа тяжёлая. Спецификации нужно формулировать очень аккуратно. Простой пример: функция сортировки таблицы должна возвращать те же элементы, что получила, только в другом порядке. Для человека это очевидно, для математической системы это нужно записать строго.

Поэтому метод применяют там, где цена ошибки высока. По раскрытиям компаний, формально проверенный код есть в самолётах Boeing, на серверах Amazon и в более чем 2,5 млрд активных устройств Apple. Обычно это код, связанный с безопасностью. Byron Cook из Amazon Web Services говорит, что верификация снимала вопросы клиентов о защите облака и ускоряла внутренние команды: крупные ошибки отлавливались рано.

Кто и что ставит на ИИ

Стартапы хотят автоматизировать самую муторную часть: составление описания того, как программа должна себя вести. Дальше остальные шаги, возможно и без ИИ, переводят код в формат для математических систем.

• &Truth. Привлёк $70 млн, Sun присоединилась к нему в августе, публичный запуск состоялся в четверг. Цель — со временем проверять код на любом языке программирования.

Научный директор Ilya Sergey сравнивает подход со строительством: мосты и здания не рушатся, потому что до постройки их считали, так почему бы не делать то же с кодом. • Harmonic. Сооснователь — глава Robinhood Влад Тенев, привлечено $295 млн.

На этой неделе компания объявила, что её математический ИИ-агент Aristotle умеет проверять программы на C и описания микросхем на Verilog. Технологию оценивают потенциальные клиенты, включая производителей чипов Tensordyne и Nvidia; венчурное подразделение Nvidia — один из инвесторов. • **Anthropic и Theorem.

** Неделю назад они сообщили, что с помощью ИИ нашли ошибки в открытом ПО, которые не поймали триллионы тестов. Выпущено и дополнение для Claude, помогающее разработчикам с верификацией. Стоимость первого проекта не раскрыли.

• Truidic. Основал Madan Musuvathi, ушедший из Microsoft Research после более чем 20 лет работы. По его мнению, ИИ в руках атакующих очень силён, а верификация может сделать ИИ безопасным.

• Proofcraft. Давно занимается классической верификацией. Её руководители June Andronick и Gerwin Klein говорят, что поток запросов превышает возможности и их самих, и конкурентов.

Открытые проекты тоже пробуют метод. Некоммерческий фонд Beneficial AI Foundation на грант Anthropic проверил в этом году тот же шифровальный код, что и Sun. Michael Rosenberg, один из мейнтейнеров библиотеки curve25519-dalek, надеется на постоянное финансирование таких работ, но не знает, откуда оно возьмётся, и не хочет полагаться на добрую волю ИИ-компаний.

Где метод упирается в потолок

Пока технология на стадии прототипов. Неясно, сколько клиенты готовы платить и в каком виде получать продукт: напрямую или через посредников вроде Anthropic. Несколько средних технологических компаний рассказали Wired, что проверяли максимум одну ключевую функцию продукта, а то и ни одной. Причины: нехватка инженеров-верификаторов, цена выше потенциального риска и страх, что недели ожидания проверки замедлят выпуск обновлений. Даже Apple в своей библиотеке шифрования corecrypto вынуждена осторожно добавлять новый код, чтобы успевать его проверять.

Есть и принципиальные возражения. Доказательство опирается на допущения о том, как компьютеры и люди взаимодействуют с программой. Ошибки пользователя и поломки железа оно может не поймать. Will Wilson, глава стартапа Antithesis (ИИ-поиск багов), называет формальную верификацию «ловушкой» для любителей математики вроде него. Его компания потратила миллионы на проверку части своей защиты, назвав процесс «болью в заднице». Но собственный инструмент всё равно нашёл у неё дополнительные ошибки, а ещё баги в ПО клиентов, которое те уже формально проверили. Вывод Wilson: верификация даёт некоторую уверенность, но подтвердить её может только исчерпывающее тестирование. Виталик Бутерин в блоге тоже написал, что формальная верификация не панацея, хотя считает её важной защитой от кибератак с помощью ИИ.

Отдельный риск видят Andronick и Klein: если описание задачи писал ИИ, возникает «неоправданное доверие» к результату. Доказательство верно лишь настолько, насколько верно описано, что считать правильным.

Практический вывод для инженеров: ИИ резко снижает цену самого дорогого этапа, но проверять придётся и сами спецификации, и работу тестами. Две компании, где код формально не проверяют, готовы были бы платить ИИ-лабораториям за «проверенный» код, который сгенерировал ИИ. Если это сработает, формальная проверка выйдет за пределы NASA и Apple.