Claude проверяла существующий код, а не писала новый

Команда Anthropic Frontier Red Team совместно с Theorem поручила Claude формально проверять уже существующее программное обеспечение. За несколько недель модель, по данным Anthropic, создала около 180 млн строк кода математических доказательств, используя тестовые программы для 123 библиотек из проекта Google OSS-Fuzz.

Claude преобразовывала тесты на сбои в математические задачи, анализировала скомпилированный машинный код и строила доказательства. Их автоматически проверяла программа Rocq. Anthropic называет генерацию доказательств «полностью автономной» и утверждает, что она почти не требует участия проверяющих; при этом инструменты и формальные основы для работы создали специалисты Theorem.

Проверка выявила ошибки, которые не находили годами

Во время построения доказательств Claude обнаружила сотни ошибок, и ей разрешили исправить их самостоятельно. По словам исследователей, часть дефектов проявлялась лишь в особых условиях — например, при очень больших входных файлах или определённой последовательности обращений к данным.

При проверке широко используемой программы для чтения PDF команда за неделю нашла столько же уязвимостей, сколько обычно сообщают для этого приложения за год. В другой программе Claude выявила логическую ошибку, оставшуюся незамеченной более десяти лет. Anthropic отмечает, что попытка доказать корректность может обнаружить реальные дефекты, даже если закончить полное доказательство не удаётся.

Доказательства зависят от условий и обходятся дорого

Формальная проверка не означает, что программа безошибочна. По оговорке Anthropic, доказательства действуют для конкретной архитектуры процессора, однопоточных программ и входных данных размером менее 64 МБ. В реальности библиотеки могут запускаться на разном оборудовании и в разных конфигурациях.

Отдельные доказательства требовали сотен миллионов токенов, а общую стоимость проекта Anthropic не раскрыла. В небольшом тесте доказательства удалось повторно использовать. По данным компании, Opus 5.5 решает половину задач на доказательство, расходуя примерно на 40% меньше токенов, чем Opus 5.

Anthropic ожидает, что проверка кода с помощью ИИ вскоре станет такой же практичной, как обычное тестирование. Дорожная карта Theorem уже включает критически важную инфраструктуру — glibc, OpenSSL и cURL, однако это планы, а не подтверждение завершённой проверки этих проектов: компания описала их в своей дорожной карте.