Проблема верификации: статика против динамики
Традиционные бенчмарки для верифицируемой генерации кода (например, VERINA) тестируют доказательство на одной фиксированной реализации. Однако в реальной разработке код постоянно рефакторится. Авторы работы Aravind Mandiga и Guoming Li задались вопросом: остается ли сгенерированное LLM доказательство валидным, если структура программы меняется, но ее поведение и спецификация сохраняются?
Для ответа они представили новый тест RefactorProof. На основе 185 задач из набора VERINA были выведены 458 вариантов Lean-кода с применением структурного рефакторинга. При этом спецификация и исходное доказательство оставались неизменными побайтово.
Ключевые метрики хрупкости
Результаты показали существенную хрупкость (brittleness) доказательств. Показатель структурной стабильности (PSR) для референсных доказательств составил всего 4.3%. Это означает, что в подавляющем большинстве случаев даже незначительное изменение структуры кода делает стандартное доказательство невалидным.
Сравнение специализированных провайдеров
Несмотря на общую хрупкость, специализированные модели-провейдеры (provers) демонстрируют значительно лучшую устойчивость, чем референсные артефакты. Ниже приведены данные по выживаемости доказательств (unchanged-proof survival) на совпадающих задачах:
| Модель / Источник | Улучшение стабильности (в пунктах) | Примечание |
|---|---|---|
| Референсные доказательства (VERINA) | База (0) | Структурный PSR: 4.3% |
| DeepSeek-Prover-V2-7B | +15.6 | 95% CI исключает ноль |
| Goedel-Prover-V2-32B | +18.8 | 95% CI исключает ноль |
| Goedel-Prover-V2-8B | +20.3 | 95% CI исключает ноль |
Все три специализированные модели показали статистически значимое преимущество. Порядок эффективности сохраняется даже при исключении универсально выживших вариантов и при агрегации по семействам моделей.
Цена восстановления: дешевый ремонт
Важное открытие исследования заключается в том, что «слом» доказательства не всегда означает высокую стоимость его восстановления. Авторы обнаружили, что для исправления большинства сбоев достаточно минимальных правок:
- 51 из 54 сбоев в референсных доказательствах исправляется редактированием всего одного идентификатора.
- 58 из 85 сбоев в доказательствах от провайдеров также исправляются одним редактированием.
Это указывает на то, что LLM-генерируемые доказательства, хотя и хрупки к структурным изменениям, легко адаптируются. RefactorProof измеряет именно стабильность «из коробки», а не стоимость поддержки доказательства после его поломки.
Значение для индустрии
Работа, принятая на NeurIPS 2026 Workshop on AI for Verifiable Coding, подчеркивает необходимость перехода от тестирования на статических примерах к тестированию на динамически изменяющемся коде. Для создания надежных систем верифицируемой генерации кода критически важно учитывать устойчивость доказательств к рефакторингу, а не только их способность доказать корректность фиксированного фрагмента.
Источник: arXiv cs.AI ↗