В Anthropic утверждают, что Claude доказал, что 123 библиотеки с открытым исходным кодом не могут дать сбой
Компании Anthropic и Theorem использовали Claude для написания 180 миллионов строк машинно проверенных доказательств, демонстрирующих, что код, протестированный методом фаззинга в 123 библиотеках с открытым исходным кодом, не может дать сбой, и попутно обнаружили давно скрытые ошибки.
Компания Anthropic утверждает, что Claude математически доказал, что код, прошедший фаззинговое тестирование в 123 библиотеках с открытым исходным кодом, не может дать сбой при обработке входных данных размером менее 64 МБ, и при этом обнаружил ошибки, которые были пропущены в ходе многолетнего тестирования.
Работа, опубликовано Anthropic 22 октября Проект Theorem, разработанный совместно со стартапом Theorem, специализирующимся на формальной верификации, охватывает 239 точек входа из проекта Google OSS-Fuzz. Anthropic называет его первой крупномасштабной попыткой использовать ИИ для формальной верификации производственного программного обеспечения на уровне ассемблерного кода.
От тестов к доказательствам
Фаззинг запускает в программу огромное количество случайных входных данных, чтобы увидеть, что приводит к сбою, но он никогда не сможет проверить все входные данные. Anthropic превратил каждый существующий фаззинг-тест в формальное правило: “этот тест никогда не дает сбоя”, и попросил Claude доказать, что это правило выполняется для всех входных данных размером менее 64 МБ.
Доказательства работают с скомпилированным машинным кодом RISC-V, а не с исходным кодом. За несколько недель Claude написал около 180 миллионов строк доказательств в помощнике доказательств Rocq, что составляет примерно 600 000 строк для типичной программы. Человеку не нужно их читать; программа проверки Rocq подтверждает каждое доказательство механически.
Пропущены проверки на наличие ошибок
Всякий раз, когда доказательство не удавалось, Claude находил ошибку, исправлял её и пробовал снова. По словам Anthropic, в результате этой работы были обнаружены сотни ошибок, в том числе ошибка записи за пределы допустимого диапазона в декомпрессоре, которая возникала только при входных данных размером около 20 МБ с одним редким вариантом компоновки, а также повторное обнаружение известной уязвимости в XML-парсере libexpat.
В ходе отдельных тестов Claude доказал, что код zlib ядра Linux соответствует спецификации формата, а при попытке проверить широко используемый PDF-ридер обнаружил за одну неделю столько же уязвимостей, сколько обычно выявляется за год. Подробности в [ссылка на документацию]. техническое приложение.
Чего это не доказывает
В Anthropic четко указано, что “формально проверено” не означает отсутствие ошибок. Доказательства предполагают однопоточные, статически связанные RISC-V бинарные файлы на Linux, в то время как большинство реальных развертываний работают на x86 или ARM. Используемые проверки памяти не выявляют все ошибки безопасности памяти, и не каждая точка входа в каждой библиотеке была охвачена.
Ещё один нюанс — стоимость: для подтверждения могут потребоваться сотни миллионов токенов. Компания Anthropic утверждает, что Claude Opus 5.5 решил половину из 36 задач, использовав примерно на 40% меньше токенов, чем Opus 5, а агенты, которые делились доказательствами, использовали на 17% меньше токенов.
Почему это важно
Искусственный интеллект становится очень хорош в поиске ошибок, поскольку Уязвимости PHP2Shell Доказательства были продемонстрированы на этой неделе. Доказательства — это способ показать, что целых классов ошибок просто не существует. Компания Theorem выпустила... Claude навык для разработчиков открытого исходного кода, желающих зарегистрировать свои проекты, и это оценки что к концу 2027 года можно будет проверить 95% машинного кода в программной экосистеме Nix, что составит около $134 миллионов.
