Привычная цепочка проверки AI-сгенерированного кода выглядит так: агент написал код, тесты прошли, код пошёл в работу. Эта схема работает, пока баг не обнаруживается в сценарии, который тесты не покрывали. Vero — первый бенчмарк, где агент должен не просто написать многофайловый проект, но и формально доказать его корректность. Лучший протестированный агент полностью решил 27 из 43 задач.

Почему тестов больше недостаточно

Тесты проверяют конкретные случаи. Формальное доказательство покрывает всё пространство входных данных. Разница существенная: тест, проверяющий createAccount с одним ID, не гарантирует, что функция сработает с любым другим.

Vero содержит 43 задачи, собранные из реальных открытых репозиториев. Исходные языки — Python, Dafny, Verus и Coq, но все задачи переведены на Lean 4 — язык программирования, который одновременно является системой доказательства теорем. Каждая задача — это многомодульный проект с заранее определёнными интерфейсами API и формальными спецификациями.

Спецификация в этом контексте — точное математическое описание свойств, которые программа обязана иметь. Например, для банковского счёта: если создать новый аккаунт и сразу проверить баланс, он должен быть нулём. Не «обычно ноль» и не «в тестах ноль», а математически доказанное «всегда ноль, при любых входных данных».

Два режима и обман не засчитывается

Два режима оценки. В режиме proof агент получает готовую реализацию и должен доказать, что она соответствует спецификации. В режиме codeproof агент пишет и код, и доказательство одновременно. Полное покрытие обязательно: любая недоказанная спецификация означает дыру, в которой может скрываться баг.

Система проверки не доверяет агенту. Она пересобирает чистый Lean-проект, подставляет только тела функций, которые написал агент, и компилирует с проверкой аксиом. Доказательство, использующее sorry — заглушку Lean для пропуска доказательства — или внедрённую аксиому, не засчитывается.

Отдельный механизм — аудит. Агент может доказать, что предоставленная спецификация невыполнима или что эталонный код неверен. Это превращает ошибки в самих задачах из тихих провалов агента в формальные, проверяемые находки.

Результат: 27 из 43

В бенчмарке 43 задачи — каждая это многомодульный проект с API и формальными спецификациями. Задача считается решённой, только если агент написал весь код и доказал все спецификации без единого пропуска. Частичное решение не засчитывается.

Лучший протестированный агент полностью решил 27 проектов из 43. В 16 оставшихся остались недоказанные свойства — то есть агент написал код, но не смог математически подтвердить, что он соответствует спецификации. На самых сложных репозиториях — например, формальная арифметика и криптографические протоколы — агент не закрыл ни одной спецификации.

Важно: 27 из 43 — это не «агент почти справился». Каждая недоказанная спецификация — потенциальная ошибка, которую тесты не поймали бы. Тесты проверяют конкретные случаи, а формальное доказательство покрывает всё пространство входных данных.

Что это значит для практики

Для команд, использующих AI-агентов в реальных проектах, Vero намечает направление, в котором будет развиваться доверие к сгенерированному коду.

Внимание: Vero — исследовательский бенчмарк, а не готовый инструмент для продакшена. Lean 4 требует специализированной экспертизы, а формальная верификация применима только к задачам, где спецификацию можно записать математически. Большинство бизнес-задач пока не подходят под это определение.

Но тренд стоит отслеживать. Если AI-агенты научатся не только писать код, но и доказывать его корректность, граница ответственности между человеком и системой сдвинется. Сейчас она проходит на ревью кода. Через несколько лет может переместиться на проверку спецификаций — формулировок того, что код должен делать, а не того, что он делает.

Ссылки

Ссылки

По теме

По теме