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» шесть раз в год, а также иметь доступ ко всему архиву и разделу комментариев.

Подписаться