Группа UC Berkeley во главе с Dawn Song выпустила Vero — первый открытый бенчмарк, который оценивает AI-агентов на уровне целых мультимодульных репозиториев с формальной верификацией в Lean 4. Лучшие протестированные конфигурации закрыли лишь часть проектов, а 10 инстансов не решила ни одна модель: по оценке авторов, верифицированный синтез на уровне репозитория пока остаётся нерешённой задачей.
Что произошло
Benchmarks состоят из 43 мультимодульных проектов на Lean 4, суммарно содержащих 743 публичных API и 2705 спецификаций; они переведены из реальных кодов на Python, Dafny, Verus и Coq. В режиме codeproof агент сам должен написать не только реализации, но и машинно-проверяемые доказательства для каждой спецификации. Каждый запуск ограничен 90 минутами wall-clock времени. Лучший результат показала GPT-5.5 (xhigh) в Codex: полностью решены 27 из 43 инстансов, что соответствует 87,3% всех спецификаций; Claude Opus 4.8 (xhigh) закрыл 8 из 43. Десять проектов не были решены ни в одной протестированной конфигурации, и авторы делают вывод, что текущие агенты пока не способны к верифицированному синтезу на уровне репозитория.
Контекст
Ключевая особенность Vero — критерий оценки: корректность каждой спецификации подтверждается не оценкой другой модели, а машинной проверкой в Lean 4, что устраняет типичную субъективность LLM-as-judge в оценке кода. Важна и масштабность: прежние оценки агентов в основном проводились на отдельных функциях, тогда как здесь единицей измерения становится целый мультимодульный репозиторий. В бенчмарк встроен audit-механизм: агенту формально разрешено доказать ошибочность самой спецификации бенчмарка и исправить её, что защищает результаты от тихих ошибок curation pipeline — стандартной проблемы ручных бенчмарков верифицированного кода. Vero не является продуктом, а представляет собой открытый оценочный стенд: curation pipeline и evaluation harness, опубликованные вместе со статьёй на arXiv (2608.13522).
Почему это важно для индустрии
Для отрасли Vero создаёт публично измеримую метрику: «верифицированное ПО, созданное агентом» впервые стало измеримой величиной на общем воспроизводимом эталоне, по которому вендоры coding-агентов смогут сравнивать свои модели друг с другом. Лидерборд с поминаутными кривыми прогресса даёт видимый индикатор того, закрывается ли capability gap, и можно ожидать, что вендоры моделей начнут оптимизироваться под Vero, публиковать результаты в анонсах моделей и строить гибридные пайплайны agent + automated theorem prover, нацеленные на остающиеся нерешённые инстансы. Одновременно бенчмарк даёт трезвый производственный сигнал: ни одна модель не даёт верифицированный репозиторий «из коробки», поэтому репозиторий-уровневая верифицированная генерация пока не является надёжно развёртываемой способностью.
Почему это важно для пользователей
Бенчмарк полностью открыт: код, curation pipeline и evaluation harness доступны в репозитории GitHub sunblaze-ucb/vero, методика описана в arXiv-бумаге 2608.13522, а публичный лидерборд с кривыми прогресса позволяет отслеживать динамику во времени. Любая команда может запустить собственного агента на 43 репозиториях и отследить результаты по публичным кривым. Отдельная ценность — список 10 репозиториев, которые ни одна frontier-модель пока не взяла: от формализаций floating-point до распределённой KV-хранилища ironkv. Это наглядная карта текущих пределов агентов в верифицируемом коде.
Что пока неизвестно / ограничения
Результаты получены для конкретных конфигураций моделей и scaffolding (GPT-5.5 и Claude Opus 4.8 в режиме xhigh) с бюджетом 90 минут wall-clock; другое время или другой scaffold могли бы дать иную картину. Вывод о неспособности текущих агентов основан только на протестированных конфигурациях, а не на всём классу возможных систем. Бенчмарк является research-инфраструктурой, а не продуктом для конечных пользователей, а прогнозы об оптимизации вендоров под Vero и о будущем классе «verified by default» программного обеспечения остаются сценариями, а не подтверждёнными фактами.
Источники
Автор
Look at AI, редакция