Claude от Anthropic теперь пишет код и автоматически доказывает его корректность

Доказывать, что программа работает без ошибок при любых обстоятельствах, всегда было слишком дорого. Команде специалистов понадобилось 20 человеко-лет, чтобы формально проверить небольшое ядро операционной системы seL4. Поэтому такой подход применяли лишь в особо ответственных случаях, например для программного обеспечения авионики Airbus.

Вместо специалистов доказательства строила модель Claude, которую задействовала Frontier Red Team Anthropic совместно с Theorem. За несколько недель модель создала около 180 миллионов строк математического кода доказательств, опираясь на тестовые программы из 123 библиотек с открытым исходным кодом проекта Google OSS-Fuzz, посвящённого безопасности.

Claude не писала новый код, а проверяла существующий: переводила тесты на аварийное завершение в математические задачи, анализировала скомпилированный машинный код и создавала развёрнутые доказательства. Независимая программа Rocq автоматически проверяла результат. По данным Anthropic, участие проверяющих почти не требовалось. Исследователи называют генерацию доказательств «полностью автономной», хотя инструменты и формальные основы для неё создали специалисты Theorem.

Claude находит ошибки, пропущенные годами тестирования

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

Так, при проверке популярной программы для чтения PDF команда за одну неделю нашла столько же ошибок безопасности, сколько обычно сообщали для этой программы за целый год. В другом приложении Claude заметила логическую ошибку, остававшуюся незамеченной больше десяти лет. Anthropic отмечает, что попытка построить доказательство выявляет настоящие ошибки, даже если завершить проверку не удаётся.

Возможности и ограничения формальной проверки

Anthropic подчёркивает: «формально проверенный» код не означает «код без ошибок». Доказательства действуют только при строгих условиях: для конкретной архитектуры процессора, однопоточных программ и входных данных размером менее 64 МБ. На практике эти библиотеки запускают на разном оборудовании и в разных конфигурациях.

Вычисления обходятся дорого: на отдельные доказательства уходят сотни миллионов токенов. Общую стоимость проекта Anthropic не раскрывает. Однако если ИИ может проверять собственный код, разработчики смогут больше доверять программам, созданным ИИ, и тратить меньше времени на их проверку. Экономия затронет не только формальную верификацию, но и весь процесс программирования.

Небольшой дополнительный тест показал, что доказательства можно использовать повторно, а новые модели работают эффективнее: Opus 5.5 решает половину задач на доказательство, расходуя примерно на 40 процентов меньше токенов, чем Opus 5.

Проект подкрепляет аргументы в пользу автоматизации разработки. Если ИИ способен писать код и доказывать его корректность при заданных условиях, вопрос меняется: теперь важно не только, может ли ИИ программировать, но и способен ли он подтвердить безопасность написанного кода. Если способен, последствия могут выйти далеко за пределы сегодняшних инструментов для разработки.

Anthropic ожидает, что формальная проверка с помощью ИИ вскоре станет такой же практичной, как стандартное тестирование. В дорожной карте Theorem уже указана критически важная инфраструктура: glibc, OpenSSL и cURL.