Нейросеть Claude нашла сотни уязвимостей в открытом ПО за пару недель

В рамках повышения безопасности открытого программного обеспечения нейросеть Claude написала 180 миллионов строк математических доказательств и обнаружила сотни скрытых уязвимостей. Проект компании Anthropic охватил 123 публичные библиотеки кода. ИИ-модель проводила формальную проверку, которая на языке высшей математики гарантирует отсутствие дефектов при заданных параметрах. Обычное тестирование проверяет программу точечно, тогда как математическое доказательство полностью исключает саму возможность сбоя.

Анализ машинного кода проводился совместно с компанией Theorem, обеспечившей техническую базу проекта. Искусственный интеллект переформатировал отчеты об ошибках в сложные математические задачи, а написанные им решения проверялись независимой платформой Rocq. Нейросеть самостоятельно корректировала найденные баги. Большинство уязвимостей активировались только при обработке массивных файлов или нестандартных запросах. За одну неделю анализа программы для открытия PDF-документов алгоритм нашел столько же слабых мест, сколько техническая поддержка фиксирует за год. В другом приложении была исправлена логическая ошибка, существовавшая более десяти лет.

Ранее формальная проверка кода была слишком дорогостоящей и применялась в узких сегментах, например, при разработке программ для самолетов Airbus, где процесс занимал до 20 лет работы программистов. Сейчас алгоритм справляется с задачей за несколько недель, но действует в строгих границах. Вычисления актуальны для одного потока, конкретного процессора и данных до 64 мегабайт. Финансовые затраты на проект в рублях не публикуются, однако разработчики отмечают рост энергоэффективности искусственного интеллекта. Версия Claude Opus 5.5 решает подобные задачи на 40% экономнее предшественника. В ближайшее время математические доказательства от нейросети Claude будут применены для аудита таких систем, как OpenSSL и cURL.

Источник: mltimes.ai