Claude помог доказать свойства безопасности кода в 123 библиотеках
Anthropic и Theorem 22 октября опубликовали исследование формальной проверки программ с помощью Claude. По данным авторов, за несколько недель удалось доказать свойства для 239 тестовых точек входа в 123 открытых библиотеках.
От перебора тестов к проверяемому доказательству
Обычный фаззинг подаёт программе множество специально подобранных входных данных и ищет сбой. В эксперименте существующие тесты превращали в математические требования к скомпилированной программе. Claude строил доказательства, а проверяющая система Rocq проверяла их соответствие этим требованиям.
Авторы сообщают примерно о 180 миллионах строк доказательств. Часть результатов и описание используемой модели исполнения опубликованы для внешней проверки.
Где заканчивается гарантия
Речь идёт об определённых свойствах статических однопоточных RISC-V-программ с заданными условиями исполнения и входами меньше 64 МБ. Это не утверждение, что все 123 библиотеки полностью безопасны на любом процессоре, в любой конфигурации и при любом использовании.
Доказательство зависит от корректности спецификации, модели процессора и операционной системы, а также самого проверяющего инструмента. Оставшиеся за пределами модели ошибки оно не исключает.
Почему это интересно: проверяемый результат можно оценивать отдельно от убедительности ответа языковой модели. Но перед переносом подобной гарантии в продукт нужно установить, совпадают ли доказанные условия с реальной системой.
Масштаб эксперимента указан по отчёту авторов; редакция не воспроизводила весь набор доказательств.