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

Anthropic использовала Claude, чтобы математически доказать корректность существующего кода. Этот подход решает одну из ключевых проблем программного обеспечения, создаваемого ИИ, но имеет строгие практические ограничения.

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

Frontier Red Team Anthropic совместно с партнёром Theorem поручила Claude выполнить эту работу по доказательству. Всего за несколько недель модель создала около 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.

Новости ИИ без шумихи — отобраны людьми

Подпишитесь на THE DECODER, чтобы читать материалы без рекламы, получать еженедельную рассылку об ИИ, эксклюзивный отраслевой отчёт «AI Radar» о передовых разработках шесть раз в год, полный доступ к архиву и доступ к разделу комментариев.