Как сообщает The Decoder, команда Frontier Red Team компании Anthropic совместно с партнером Theorem поручила модели Claude формальную верификацию существующего кода. Формальная верификация — это математическое доказательство корректности программы, а не просто проверка на тестовых примерах.
Раньше метод был непомерно дорогим: на формальную верификацию небольшого ядра операционной системы seL4 у команды специалистов ушло 20 человеко-лет. Поэтому его применяли лишь в исключительных случаях, например в авионике Airbus.
Claude сгенерировал около 180 млн строк математических доказательств за несколько недель, опираясь на тестовые программы из 123 открытых библиотек проекта безопасности OSS-Fuzz компании Google. Новый код модель не писала: она переводила тесты на сбои в математические задачи, анализировала скомпилированный машинный код и строила доказательства, которые автоматически проверяет независимая программа Rocq. По данным Anthropic, процесс почти не требует людей-рецензентов; исследователи называют его «fully autonomous» — полностью автономной — генерацией доказательств, хотя инструменты и формальные основы созданы людьми в Theorem.
По ходу работы Claude столкнулся с сотнями ошибок и получил право исправлять их сам; по словам Anthropic, даже неудачные попытки полного доказательства выявляют реальные ошибки. Многие из найденных проблем не ловило обычное тестирование: они проявляются только в особых условиях, например при нестандартно больших входных файлах или редкой последовательности обращений. При проверке широко используемого PDF-ридера за одну неделю обнаружили столько уязвимостей, сколько об этой программе обычно сообщают за год, а в другом приложении Claude нашел логическую ошибку, которую не замечали более десяти лет.
Anthropic признает, что «формально верифицированный» не означает «безошибочный»: доказательства действительны лишь при жестких условиях — конкретная архитектура процессора, однопоточные программы и входные данные меньше 64 МБ. На практике эти библиотеки работают на разном оборудовании и в разных конфигурациях. Дорог и сам процесс: отдельные доказательства расходуют до сотен миллионов токенов (единиц текста, которые обрабатывает модель), а общую стоимость проекта Anthropic не раскрывает.
При этом, по оценке Anthropic, если ИИ может проверять собственный код, разработчики смогут больше доверять сгенерированному ИИ ПО и тратить меньше времени на ревью — экономия возникает не только на верификации, но и на всем процессе разработки. Компания ожидает, что формальная верификация с помощью ИИ скоро станет такой же практичной, как стандартное тестирование, а дорожная карта Theorem уже нацелена на критическую инфраструктуру — библиотеки glibc, OpenSSL и cURL. По данным Anthropic, доказательства можно переиспользовать, а модель Opus 5.5 справляется с половиной доказательств, затрачивая примерно на 40% меньше токенов, чем Opus 5.
