Компания Anthropic совместно со стартапом Theorem представила результаты использования языковой модели Claude для автоматизированной формальной верификации софта. Модель сгенерировала математические доказательства корректности работы для 123 библиотек с открытым исходным кодом на уровне ассемблерного кода RISC-V.
Формальная верификация предполагает математическое доказательство того, что программа гарантированно соблюдает правила безопасности при любых условиях. Исторически этот метод практически не использовался в коммерческой разработке из-за огромных трудозатрат и применялся лишь в критически важных сферах вроде авионики. К примеру, верификация микроядра seL4 потребовала 20 человеко-лет при двух годах на написание самого кода.
В проведенном исследовании Claude автономно доказала, что скомпилированные бинарные файлы программ завершают работу штатно — без сбоев assertions и ошибок управления памятью — при любых входящих данных объемом до 64 МБ в окружении смоделированного ядра Linux.
В процессе генерации доказательств нейросеть также выявила в зрелом коде ошибки, остававшиеся незамеченными годами, несмотря на триллионы прогонов традиционных тестов. Часть математических доказательств и описания семантики авторы проекта опубликовали в открытом доступе для независимой проверки.
Комментарии и обсуждение
Пока нет комментариев. Будьте первым!