Бенчмарк Vero проверяет, умеет ли агент писать код вместе с доказательством

Обычные проверки кодовых агентов смотрят, проходят ли тесты. Формальная верификация требует большего: к программе нужно доказательство того, что она соответствует спецификации при любых входных данных.

Дон Сон и коллеги представили Vero — первый, по их словам, бенчмарк на совместный синтез реализации и доказательства на уровне целого репозитория, а не отдельной функции. Задача агента — не просто написать работающий код, а сдать его вместе с проверяемым доказательством корректности.

Мотив прикладной: чем больше кода пишут агенты, тем меньше пользы от того, что он «просто работает» на тестах.

Dawn Song@dawnsongtweets

1/ Can AI agents build formally verified software repositories? Introducing Vero: the first benchmark for joint implementation and proof synthesis at the repository level. As AI agents write a growing share of our software, we need more than just working code; we need https://t.co/M8E1i1kjXB

18322 августа 2026