Anthropic: Библиотека Claude для формальной верификации открыта в массовом порядке

22 октября команда Frontier Red Team компании Anthropic, специализирующейся на искусственном интеллекте, опубликовала исследование, в котором отмечается, что современные большие языковые модели обладают способностью автоматически генерировать формальные доказательства в значительно большем масштабе. Совместно с Theorem эта команда провела формальную верификацию свойств безопасности более чем 100 реальных открытых библиотек на уровне ассемблера RISC-V, используя модель Claude — это первая в истории попытка大规模 формальной верификации программного обеспечения производственного уровня системой искусственного интеллекта на уровне ассемблера. В процессе построения доказательств команда неожиданно выявила несколько давно существовавших, но до сих пор не обнаруженных уязвимостей. Метод эксперимента заключался в преобразовании уже существующих компилируемых тестовых примеров фаззинга из Google OSS-Fuzz в формальные спецификации и последующей верификации входных данных произвольного размера объёмом не более 64 МБ в условиях однопоточной статической двоичной среды, фиксированного бюджета оперативной памяти, архитектуры процессора RISC-V и среды выполнения Linux.