Anthropic: Claude провёл масштабную формальную верификацию библиотек с открытым исходным кодом

22 октября команда Frontier Red Team компании Anthropic, работающей в сфере искусственного интеллекта, опубликовала исследование, согласно которому большие языковые модели способны автоматически писать формальные доказательства в более широком масштабе. Команда совместно с Theorem использовала Claude для доказательства свойств безопасности более чем в 100 реальных библиотеках с открытым исходным кодом на уровне ассемблера RISC-V, заявив, что это первый известный случай применения ИИ для масштабной формальной верификации production-программ на уровне ассемблера. В процессе написания доказательств были также обнаружены уязвимости, которые оставались незамеченными на протяжении многих лет.В ходе эксперимента существующие компилируемые фазз-тесты из Google OSS-Fuzz были преобразованы в спецификации: при допущениях об однопоточных статических бинарниках, фиксированном бюджете памяти, процессорах RISC-V и Linux для любого ввода размером менее 64 МБ программа должна завершаться нормально, не вызывая ошибок безопасности памяти или сбоев утверждений. В течение нескольких недель Claude доказал вышеуказанные свойства для 239 точек входа в 123 библиотеках OSS-Fuzz после исправления выявленных проблем. Доказательства были нацелены на скомпилированные инструкции RISC-V, примерно 180 миллионов строк Rocq, и были проверены ядром Rocq. На странице отмечается, что это не означает отсутствия уязвимостей в этих библиотеках, поскольку оставшиеся проблемы могут находиться за пределами доверенных компонентов или области действия доказательств.На странице также упоминается, что команда заставила Claude формализовать RFC 1950 и доказала, что реализация zlib в ядре Linux соответствует этой спецификации на уровне бинарного кода x86; интерпретатор, написанный на Rust и охватывающий большое подмножество Python, показал 99,95% соответствия поведению CPython на более чем 1,7 миллиона случайно сгенерированных программ. В 36 небольших задачах верификации Opus 5.5 доказал, что примерно для половины из них потребовалось примерно на 40% меньше токенов, чем для Opus 5. Команда также указала, что доказательства были нацелены на однопоточные статически слинкованные бинарники RISC-V, а средство проверки доказательств не может определить, соответствуют ли спецификации реальности.