Масштаб прорыва: от тестов к математическим доказательствам
Команда Anthropic совместно с лабораторией Theorem провела беспрецедентный эксперимент по применению формальной верификации к реальным open-source проектам. Используя модель Claude, исследователи не просто нашли баги, а создали строгие математические доказательства корректности поведения программного обеспечения. Итоговый объем сгенерированных доказательств составил около 1 миллиарда строк, из которых 180 миллионов были интегрированы в рабочие процессы.
Ранее формальная верификация была уделом узких специалистов и требовала колоссальных ресурсов. Например, для ядра seL4 потребовалось 20 человеко-лет только на написание доказательств. Теперь же LLM способны автономно обрабатывать миллионы строк кода, превращая вероятностные тесты в детерминированные гарантии безопасности.
Методология: RISC-V, Linux и OSS-Fuzz
Исследование охватило 123 реальные open-source библиотеки, входящие в инициативу Google OSS-Fuzz. Ключевая особенность подхода — верификация на уровне ассемблерного кода (RISC-V) под управлением Linux. Claude доказывал, что программы никогда не аварийно завершат работу (не вызовут crash) при любых входах размером до 64 МБ, соблюдая условия однопоточного выполнения и фиксированного бюджета памяти.
Авторы перевели существующие fuzz-тесты в спецификации (specs). Если Claude доказывает, что тестовый кейс не может вызвать сбой ни при каком входе, это становится математическим подтверждением отсутствия уязвимостей в данной области кода, что надежнее любого количества прогнанных тестов.
Ключевые результаты и метрики
Эксперимент показал, что современные модели способны находить ошибки, которые годами оставались незамеченными даже после триллионов запусков тестов. Ниже приведена сводка параметров исследования:
| Параметр | Значение / Описание |
|---|---|
| Количество проверенных библиотек | 123 open-source проекта (из OSS-Fuzz) |
| Объем сгенерированных доказательств | ~1 миллиард строк кода |
| Уровень верификации | Ассемблер (RISC-V) + семантика Linux OS |
| Ограничения входа | Размер ввода < 64 МБ, однопоточное выполнение |
| Обнаруженные баги | Многочисленные уязвимости, игнорируемые годами |
Почему это важно для индустрии
Стандартные методы защиты от кибератак больше не справляются с растущей сложностью эксплойтов, которые LLM учатся комбинировать. Формальная верификация через AI позволяет перейти от реактивного поиска багов к проактивному доказательству их отсутствия. Anthropic публикует часть доказательств, семантику RISC-V и специальный «навык» (skill) для Claude, чтобы разработчики могли начать внедрять эти практики в свои проекты уже сейчас.
Источник: Anthropic ↗