Проблема «пустой» верификации
Новое исследование авторов Aditya Vempaty, Himaneesh Sompalle и коллег ставит под сомнение метрику «процент верифицированного кода» (verification acceptance). Авторы доказывают, что стандартные пайплайны смешивают три разных свойства, и высокая оценка по одному из них не гарантирует качества. Они выделяют три «поверхности» (surfaces) сбоев:
- Поверхность A (Verifier Acceptance): Проходит ли код проверку статическим анализатором (верификатором)?
- Поверхность B (Syntactic Binding): Привязана ли доказательная обязанность (proof obligation) к реальной спецификации функции?
- Поверхность C (Semantic Fidelity): Отражает ли спецификация фактическое поведение кода и изначальное требование?
Эксперимент 1: 99.1% успеха, но 0% смысла
Для демонстрации разрыва между Поверхностью A и B исследователи использовали модель Claude Opus 4.7 (в репродукции пайплайна Li@Opus с использованием Dafny как промежуточного представления) на бенчмарке HumanEval. Результаты оказались шокирующими:
- 99.1% сгенерированного кода успешно прошли верификацию (Поверхность A).
- Однако лишь 1.9% этих образцов имели корректную привязку к спецификации (Поверхность B).
Это означает, что верификатор «видел» код, но не мог доказать его соответствие логике, так как связь с требованиями была нарушена на синтаксическом уровне.
Эксперимент 2: Верифицированный, но неработающий код
Чтобы проверить разрыв между Поверхностью B и C (когда спецификация привязана, но неверна), команда использовала внутренний пайплайн VCG (Dafny-as-intermediate) на двух Rust-бенчмарках: MBPP-Rust и VeriContest LC. В этом сценарии система принудительно обеспечивала полную верификацию.
Даже при наличии сертификата Dafny, значительная часть кода проваливала скрытые тесты:
| Бенчмарк | Доля верифицированных образцов, проваливших тесты | End2End успешность (VCG) |
|---|---|---|
| MBPP-Rust | 11.48% | — |
| VeriContest LC | 14.82% | 7.79% (535/6870) |
Сравнение с лидерами рынка
Исследователи также привели данные по конкурентам на срезе VeriContest LC, чтобы показать относительную эффективность их подхода VCG. Важно отметить, что прямое сравнение затруднено из-за различий в бюджете задач и хуках (harness), но дескриптивные различия существенны:
| Модель / Пайплайн | End2End Rate (VeriContest LC) | Примечание |
|---|---|---|
| VCG (внутренний пайплайн) | 7.79% | Полная верификация через Dafny |
| GPT-5.5 | 5.51% | Разница +2.3 п.п. |
| Opus 4.7 (single-shot) | 1.88% | Разница 4.14x |
Вывод исследования: высокая доля верифицированного кода — это «пустая» метрика, если не проверять привязку к спецификации (B) и семантическую точность (C). Разработчикам стоит смотреть не только на «зеленые галочки» верификаторов, но и на качество самих спецификаций.
Источник: arXiv cs.AI ↗