Anthropic: Claude завершил масштабную формальную верификацию открытой библиотеки

Компания искусственного интеллекта Anthropic выпустила исследование Frontier Red Team 22 октября, в котором утверждается, что большие языковые модели теперь могут автоматически составлять формальные доказательства в более широком масштабе. Команда сотрудничала с Theorem, используя Claude на уровне ассемблера RISC-V для доказательства безопасных свойств более чем 100 реальных открытых библиотек, и заявила, что это первый известный случай использования ИИ для масштабной формальной верификации производственного программного обеспечения на уровне ассемблера. В процессе написания доказательства были обнаружены уязвимости, которые не были замечены в течение многих лет.

Эксперимент преобразовал существующие компилируемые тесты fuzz из 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. В 36 небольших задачах верификации Opus 5.5 доказал, что для половины из них требуется на 40% меньше токенов, чем для Opus 5. Команда также отметила, что доказательства касаются однопоточных, статически связанных двоичных файлов RISC-V, и проверяющий не может определить, соответствует ли спецификация реальности.