Anthropic и Theorem: Claude доказал свойства безопасности в машинном коде 123 библиотек с открытым кодом и нашёл ошибки, не замеченные годами
Материал подготовлен Sintelligent с помощью ИИ. Опубликовано в SI: . Обновлено: .
ИИ научился не только искать ошибки в коде, но и доказывать их отсутствие, хотя доказательства пока работают лишь в узких условиях и обходятся дорого.
В совместной работе с компанией Theorem Anthropic с помощью Claude доказала свойства безопасности на уровне ассемблерного кода RISC-V в более чем 100 реальных библиотеках с открытым кодом; авторы называют это, насколько им известно, первой крупной попыткой применить ИИ для формальной верификации промышленного ПО на уровне ассемблера. Как пересказывает The Decoder, Claude переводил проверочные тесты на сбои в математические задачи и писал доказательства, которые проверяет независимая программа Rocq: речь о 123 библиотеках из проекта OSS-Fuzz и примерно 180 млн строк доказательного кода. В процессе нашлись сотни ошибок, пропущенных обычным тестированием, в том числе логическая ошибка, остававшаяся незамеченной более десяти лет; для одной программы просмотра PDF за неделю нашли столько проблем безопасности, сколько обычно сообщают за год. Оговорки: доказательства верны для конкретной архитектуры процессора, однопоточных программ и входных данных до 64 МБ, а одно доказательство может стоить сотни миллионов токенов.
Источники 2