Claude от Anthropic теперь пишет код и автоматически доказывает его безопасность
decoder ·
Anthropic заключила партнерское соглашение с Theorem, чтобы продемонстрировать способность своей ИИ-модели Claude автоматически генерировать математические доказательства, подтверждающие корректность существующего программного кода. В ходе недавнего проекта Claude за несколько недель создала около 180 миллионов строк доказательного кода для 123 библиотек с открытым исходным кодом из проекта Google OSS-Fuzz. Этот автономный процесс включал преобразование тестов на сбои в математические задачи и анализ скомпилированного машинного кода, при этом независимый инструмент Rocq проверял результаты. На этапе верификации Claude обнаружила сотни ошибок, которые традиционные методы тестирования не выявляли годами, включая критические уязвимости безопасности в широко используемых PDF-ридерах. Однако эти формальные доказательства имеют строгие ограничения: они применимы только к определенным архитектурам процессоров, однопоточным программам и входным данным объемом менее 64 МБ. Хотя вычислительные затраты остаются высокими, Anthropic отмечает, что новые модели становятся более эффективными и требуют меньшего количества токенов для решения аналогичных задач. Компания стремится сделать ИИ-верификацию такой же рутинной процедурой, как стандартное тестирование ПО, что потенциально может трансформировать подход разработчиков к доверию и проверке кода, сгенерированного искусственным интеллектом.
decoder