Anthropic и её партнёр Theorem использовали Claude для математической проверки существующих программ. По данным исследователей, за несколько недель модель создала около 180 млн строк доказательств для кода из 123 открытых библиотек и обнаружила сотни ошибок. Но это не гарантия безотказной работы: доказательства действуют только в заданных условиях.
Не новый код, а доказательства для существующего
Команда Frontier Red Team в Anthropic вместе с Theorem проверяла уже написанное программное обеспечение. В основу работы легли тестовые программы для 123 библиотек из проекта безопасности Google OSS-Fuzz. Здесь речь не о том, что любой пользователь Claude теперь получает гарантированно безопасную программу по запросу.
Claude переводил тесты на сбои в математические задачи, анализировал машинный код и составлял доказательства. Это называется формальной верификацией: вместо проверки отдельных примеров система математически обосновывает, что код соответствует заданным условиям.
Затем доказательства автоматически проверяла отдельная программа Rocq. По заявлению Anthropic, участие людей в проверке почти не требовалось. Исследователи называют генерацию доказательств полностью автономной, однако инструменты и математическую основу для неё создали специалисты Theorem.
Поиск доказательств помог найти ошибки
По словам исследователей, во время работы Claude обнаружил сотни ошибок; модели разрешили самостоятельно их исправлять. Некоторые проявлялись лишь при редких сочетаниях условий — например, на необычно больших входных файлах или при определённой последовательности обращений к данным.
В одном из приложений Claude нашёл логическую ошибку, которая оставалась незамеченной более десяти лет. Anthropic отмечает: даже если полное доказательство построить не удаётся, сама попытка может выявить реальные дефекты. Это полезный результат, но не равнозначный доказанной корректности всей программы.
Где заканчивается гарантия
Anthropic отдельно предупреждает: формальная проверка не означает отсутствия любых ошибок. В этом проекте доказательства действуют для конкретной архитектуры процессора, однопоточных программ и входных данных объёмом менее 64 МБ. Однопоточная программа здесь означает выполнение в одном потоке, а не в нескольких параллельных. На другом оборудовании или при иной конфигурации переносить вывод автоматически нельзя.
Для читателя главный вопрос поэтому не «проверял ли код ИИ», а «что именно доказано и при каких условиях». Для сравнения с другими подходами пригодится обзор инструментов автоматической проверки кода: наличие такой проверки само по себе не означает наличия математического доказательства.
Цена вычислений пока остаётся открытым вопросом
Отдельные доказательства требовали сотен миллионов токенов — единиц текста, которые обрабатывает модель. Общую стоимость проекта Anthropic не раскрыла. Поэтому по этим результатам нельзя посчитать экономию для разработчиков или заключить, что метод уже выгоднее обычного тестирования.
Anthropic рассчитывает сделать формальную проверку с помощью ИИ столь же практичной, как стандартные тесты. В планах Theorem — работа с glibc, OpenSSL и cURL, важными компонентами программной инфраструктуры. Пока это направление дальнейшей работы, а не сообщение о завершённой проверке этих проектов.
