Парадокс обратной связи в Verus
В верифицируемом программировании на Rust (с использованием фреймворка Verus) существует скрытая проблема: попытка исправить ошибки модели (LLM) через корректность (correctness feedback) приводит к потере критически важных доказательств. Исследование, представленное на NeurIPS 2026 Workshop on AI for Verifiable Coding, демонстрирует, что программы, которые формально удовлетворяют написанному контракту, но нарушают намеренное поведение, «стираются» алгоритмами исправления.
Автор работы, независимый исследователь Adarsh Agrawal, выявил, что аудит полноты спецификаций (specification-completeness auditing) и исправление корректности имеют противоположные немедленные цели. Сохранение «свидетелей» (witnesses) до их исправления дает значительно лучшие результаты.
Эмпирические данные: Verus против IntentShield
Эксперимент проводился на 12 задачах Verus/Rust с использованием четырех семейств моделей. Ключевое сравнение было проведено между методом без обратной связи (no-feedback) и итеративным циклом с коррекцией от IntentShield. Результаты показали двукратное превосходство метода без обратной связи:
| Метод | Доля найденных свидетельств (Yield) | Успешность реализации (Post-repair) |
|---|---|---|
| IntentShield (с коррекцией) | 27.1% | 62.5% (IS-Revised) |
| Без обратной связи (No-feedback) | 59.0% | 81.3% (Phase-Revised) |
Важно отметить, что преимущество сохраняется во всех семействах моделей и устойчиво к ошибкам парсера. Отдельный эксперимент с разделением фаз (phase-separated execution), где ответы не переиспользовались, подтвердил агрегированную эффективность метода без обратной связи.
Почему это важно для AI-разработки
Результаты устанавливают четкую эмпирическую границу: подход, при котором модель сначала генерирует код, затем проверяется на полноту спецификации, и только потом исправляется, работает лучше, чем классический цикл «генерация-проверка-исправление». Большинство «свидетелей», найденных без обратной связи, проваливали тесты на отложенных данных, что указывает на то, что они выявляли реальные пробелы в спецификации, а не просто ошибки синтаксиса.
Интересно, что этот эффект не воспроизвелся в доступных оценках для Dafny и Lean, что подчеркивает специфику рабочего процесса Verus/Rust. Для разработчиков AI-ассистентов это означает необходимость пересмотра стратегий валидации: нужно сохранять и сертифицировать «провальные» случаи до их исправления, чтобы улучшить качество итоговых контрактов.
Источник: arXiv cs.AI ↗