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

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

Почему математика вдруг подешевела

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

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

Сунь в августе перешла в &Truth, который публично запустился в четверг. Стартап привлёк $70 млн и хочет со временем проверять код на любом языке. Научный директор &Truth Илья Сергей сравнивает это со строительством: мосты и здания не рушатся потому, что их заранее считают, а технологии для такого рассуждения в коде были, но плохо масштабировались.

Кто ещё занимается рынком

Конкурент Harmonic, сооснователем которого стал глава Robinhood Влад Тенев, получил $295 млн. На этой неделе компания объявила, что её ИИ-агент для математики Aristotle умеет проверять ПО на C и аппаратные описания на Verilog. Технологию оценивают потенциальные клиенты, среди которых производитель чипов Tensordyne и Nvidia, чей венчурный фонд входит в число инвесторов Harmonic.

Неделей раньше Anthropic и стартап Theorem сообщили, что с помощью ИИ нашли в открытом ПО ошибки, пропущенные триллионами тестов. Они также выпустили дополнение к Claude для помощи разработчикам с верификацией. Стоимость первого проекта не раскрыли. Мадан Мусувати, ушедший из Microsoft Research после более чем 20 лет, основал Truidic: по его словам, в руках атакующих ИИ очень силён, а верификация может сделать ИИ-системы безопасными.

Фонд Beneficial AI Foundation на грант Anthropic в этом году проверил тот же криптографический код, что и Сунь. Майнтейнер библиотеки curve25519-dalek Майкл Розенберг надеется на устойчивое финансирование, но не знает, откуда оно возьмётся, и считает неправильным полагаться на добрую волю ИИ-компаний.

Где скепсис и ограничения

Верификация уже есть в самолётах Boeing, серверах Amazon и более чем 2,5 млрд активных устройств Apple, но обычно это код, связанный с безопасностью. Байрон Кук из AWS говорит, что метод снял часть опасений клиентов облака и ускорил внутренние команды. Зато несколько компаний среднего размера рассказали WIRED, что проверяли максимум одну ключевую функцию. Причины: нехватка специалистов, стоимость выше возможных рисков и опасение, что недели ожидания замедлят выпуск продукта. Двое руководителей по кибербезопасности крупных компаний, не проверявших код формально, не уверены, что автоматизация изменит расчёт, но готовы платить крупным ИИ-лабораториям за «верифицированный» сгенерированный код.

Технология пока на стадии прототипов. Неясно, сколько клиенты готовы платить и как хотят её внедрять: напрямую или через посредников вроде Anthropic. Метод опирается на допущения о том, как компьютеры и люди взаимодействуют с ПО, поэтому часть экспертов сомневается, что он поймает ошибки пользователей и аппаратные отказы.

Уилл Уилсон, глава стартапа Antithesis, который ищет баги с помощью ИИ, называет формальную верификацию «ловушкой» для математиков вроде него. Компания потратила миллионы долларов на проверку части своей защиты, назвав процесс болезненным, и всё равно нашла дополнительные ошибки собственным инструментом. Antithesis обнаруживал баги и в ПО клиентов, которое те уже верифицировали. По его словам, формальная проверка даёт некоторую уверенность, но подтвердить её может только исчерпывающее тестирование. Виталик Бутерин в блоге также писал, что она не панацея.

Ещё одна оговорка касается самих спецификаций. Основатели Proofcraft Джун Андроник и Гервин Кляйн говорят, что интерес превышает их возможности и возможности конкурентов, но опасаются «неоправданного доверия» к результатам с ИИ-спецификациями. Для команд практический вывод таков: ИИ делает верификацию достаточно дешёвой, чтобы пробовать её на критичных модулях вроде криптографии, но заменить тесты она не обещает.