Аnthropic развивает технику для формальной верификации существующего ПО при помощи AI
Компания Аnthropic представила результаты экспериментов по использованию AI-моделей для формальной верификации надёжности и безопасности уже существующих проектов. В ходе эксперимента при помощи AI-моделей для 123 открытых библиотек, протестированных в инфраструктуре OSS Fuzz, были сгенерированы математические доказательства отсутствия ошибок при работе с памятью. Проверка проводилась на уровне скомпилированного ассемблерного кода для архитектуры RISC-V. Общий объём сгенерированных доказательств составил около 180 миллионов строк кода для системы верификации Rocq Prover (около 600 тысяч строк на бинарный файл с 18 тысячами RISC-V инструкций). Доказательства формировались путём автоматического преобразования существующих fuzzing-тестов в формальные спецификации, после чего AI-модель Claude доказывала, что при любых входных данных объёмом … Читать далее Аnthropic развивает технику для формальной верификации существующего ПО при помощи AI
