Суть проблемы: иллюзия обучения
В области формальной верификации (доказательство теорем с помощью ИИ) популярна стратегия self-repair (самоисправление): если модель выдала неверный код или доказательство, система подает ей на вход этот провал и ошибку от верификатора, прося исправить. Логично предположить, что такой «обратный отклик» поможет модели избежать повторения ошибок. Однако новое исследование авторов Jack Li и Sophia Li (подано в NeurIPS 2026) ставит под сомнение эффективность этого подхода.
Ученые протестировали замороженные (frozen) версии моделей Qwen3.6-27B (универсальная) и DeepSeek-Prover-V2-7B (специализированная) на сложных задачах из набора MiniF2F в среде Lean. Ключевой вопрос: действительно ли контекст провала помогает, или модель просто «копирует» чужие ошибки?
Эксперимент: контроль над « hindsight »
Авторы провели контролируемые одношаговые эксперименты, изолируя факторы влияния. Они варьировали три параметра:
- Показывать ли модели предыдущий неудачный шаг (failed predecessor).
- Показывать ли текст ошибки компилятора, соответствующую этому провалу.
- Какую инструкцию для повторной попытки (retry instruction) использовать.
Результаты выявили два противоположных эффекта. Подача модели её собственного провала снижает вероятность успеха и резко увеличивает копирование предыдущего неверного решения. Однако добавление текста ошибки компилятора (compiler error) для модели Qwen3.6-27B частично восстанавливает производительность, нивелируя негативный эффект от показа самого провала.
Ключевые метрики и сравнения
Важнейший вывод исследования: ни одна из протестированных конфигураций обратной связи не превзошла простой метод independent resampling (независимого повторного запуска без анализа ошибок). Даже при последовательном решении 11 задач с 64 попытками каждая, преимущество от корректной диагностики исчезало при равном бюджете токенов.
| Конфигурация обратной связи | Qwen3.6-27B | DeepSeek-Prover-V2-7B | Превосходство над Resampling? |
|---|---|---|---|
| Только провал (без ошибки) | Снижение успеха, рост копирования | Снижение успеха, рост копирования | Нет (хуже) |
| Провал + корректная ошибка | Восстановление до уровня диагностики | Нет значимого восстановления | Нет (равно или хуже) |
| Провал другой задачи + ошибка | Снижение негативного эффекта | Снижение негативного эффекта | Нет |
| Independent Resampling (база) | — | — | Лучший результат |
Почему это важно для индустрии
Результат «Repair, Retry, and the Cost of Hindsight» имеет серьезные последствия для разработки AI-ассистентов в программировании. Оказывается, «стоимость hindsight» (понимания того, что пошло не так) может быть слишком высокой для текущих архитектур. Модель, видя свой провал, часто застревает в паттерне ошибки, а не анализирует его.
Для разработчиков это означает, что стратегии, основанные на бесконечной итерации «попробуй еще раз с учетом ошибки», могут быть неэффективнее с точки зрения вычислительных ресурсов (токенов), чем просто генерация новых независимых вариантов. Исследование призывает пересмотреть подходы к fine-tuning и inference-стратегиям в формальной верификации, где цена ошибки особенно высока.
Источник: arXiv cs.AI ↗