Anthropic поручила Claude формально проверить программы из 123 открытых библиотек. За несколько недель модель создала около 180 млн строк математических доказательств и обнаружила сотни ошибок.
Формальная проверка отличается от обычных тестов. Тест показывает, как программа работает на отдельных примерах. Математическое доказательство подтверждает, что при заданных условиях определённая ошибка не возникнет ни на одном допустимом входе.
Раньше такая работа требовала огромных ресурсов. Например, формальная проверка небольшого ядра операционной системы seL4 заняла у специалистов 20 человеко-лет. Поэтому этот подход применяли главным образом там, где сбой особенно опасен, включая авиационное ПО Airbus.
В проекте Anthropic участвовала компания Theorem, которая создала инструменты и формальную основу проверки. Claude преобразовывал тесты на сбои из проекта Google OSS-Fuzz в математические задачи, анализировал скомпилированный машинный код и писал доказательства. Затем их автоматически проверяла независимая система Rocq.
Когда Claude находил ошибки, ему разрешали исправлять их самостоятельно. Некоторые дефекты проявлялись только на очень больших файлах или при редкой последовательности обращений. При проверке популярной программы для чтения PDF за неделю нашли столько уязвимостей, сколько обычно сообщают за год. В другом проекте модель выявила логическую ошибку, которая оставалась незамеченной больше десяти лет.
Однако доказательство не означает, что программа свободна от любых ошибок. Результаты действуют только для конкретной архитектуры процессора, однопоточного выполнения и входных данных объёмом до 64 МБ. Отдельные проверки также требуют сотен миллионов токенов, а общую стоимость эксперимента Anthropic не раскрыла.
Новые модели уже расходуют меньше ресурсов. По данным небольшой дополнительной проверки, Claude Opus 5.5 решил половину задач примерно на 40% экономнее по токенам, чем Opus 5. Следующие цели Theorem — критические компоненты glibc, OpenSSL и cURL. Пока Claude доказывает корректность кода только в жёстко заданных границах.
