Anthropic автоматизирует доказательство корректности кода — стоимость пока не…

Anthropic и партнёр Theorem использовали Claude для математической проверки существующего программного обеспечения. По данным исследователей, модель создала около 180 млн строк доказательств для кода из 123 открытых библиотек за несколько недель и обнаружила сотни ошибок. Доказательства автоматически проверяла программа Rocq.

Для оценки применимости важны ограничения: конкретная архитектура процессора, один поток выполнения и входные данные менее 64 МБ. Отдельные доказательства требовали сотен миллионов токенов — единиц текста, обрабатываемых моделью. Общая стоимость проекта не раскрыта, поэтому подтверждённой оценки экономии для бизнеса нет.

Разбираем результаты проекта и границы применения такой проверки: https://ai-digest.ru/go/finbazar/4386/