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