RefactorProof: доказательства LLM ломаются после рефакторинга кода

Бенчмарки верифицируемой генерации кода обычно проверяют доказательство на одной фиксированной реализации. Авторы RefactorProof решили выяснить, что будет, если реализацию переписать, сохранив поведение. Из 185 задач VERINA, которые компилируются в их зафиксированном окружении, они построили 458 вариантов, сертифицированных Lean. Спецификация и проверяемое доказательство при этом не менялись ни на байт. Результат: на структурных рефакторингах доказательства массово перестают проходить проверку. Для эталонных доказательств из VERINA доля выживших (task-normalized structural PSR) составляет 4,3%, для специализированных LLM-провереров 13,3–26,8%.

Как устроен тест на хрупкость

Идея проста и жестока. Формальное доказательство привязано к конкретному тексту программы: имена, порядок определений, структура выражений. Если разработчик выносит функцию, меняет форму вычисления или переименовывает переменную, логически ничего не меняется, а доказательство в Lean может перестать собираться. В реальной разработке рефакторинг идёт постоянно, поэтому вопрос о том, переживёт ли доказательство правку, практический.

VERINA даёт эталонные доказательства только для 46 задач, и все они из базового сплита. Основные сравнения модель против эталона авторы поэтому строят на 21–25 коротких нерекурсивных задачах, подобранных так, чтобы у всех участников была одна почва под ногами. Это узкая выборка, и масштаб выводов нужно читать с оглядкой на неё.

Машины хрупки, но люди хрупче

Неожиданный поворот в том, что доказательства моделей оказались устойчивее эталонных. На сопоставимых задачах общая доля выживших неизменённых доказательств у моделей выше, чем у артефактов из VERINA. Доверительные интервалы 95% для всех трёх моделей не включают ноль.

• DeepSeek-Prover-V2-7B: +15,6 пункта к эталону
• Goedel-Prover-V2-32B: +18,8 пункта
• Goedel-Prover-V2-8B: +20,3 пункта

Порядок сохраняется при исключении вариантов T1, которые переживают вообще все, при агрегации с балансом по семействам рефакторингов и при альтернативных правилах отбора валидного доказательства, применимых на практике. Вероятная причина в том, что эталонные доказательства написаны под конкретную форму кода и тесно с ней связаны, а модели чаще выдают более прямолинейные и менее завязанные на детали конструкции. Это гипотеза, авторы работы такой механизм не доказывают.

Сломалось не значит дорого чинить

Главная оговорка статьи касается цены поломки. Предопределённые правки одного идентификатора чинят 51 из 54 подходящих структурных падений эталонов и 58 из 85 подходящих падений доказательств моделей. То есть большая часть «хрупкости» устраняется дешёвой правкой, а у эталонов чинится почти всё. Для моделей картина хуже: около 68% против 94%.

Поэтому RefactorProof измеряет именно стабильность неизменённого доказательства при рефакторинге. Стоимость сопровождения доказательства после поломки он не оценивает, и авторы подчёркивают это прямо.

Ключевые параметры исследования

• Бенчмарк: RefactorProof, производный от VERINA
• Исходных задач: 185 (компилируются в зафиксированном окружении Lean)
• Сертифицированных вариантов: 458
• Эталонные доказательства VERINA: 46 задач, только базовый сплит
• Сопоставимая выборка: 21–25 коротких нерекурсивных задач
• Структурный PSR эталонов: 4,3%
• Структурный PSR специализированных провереров: 13,3–26,8%
• Проверенные модели: DeepSeek-Prover-V2-7B, Goedel-Prover-V2-32B, Goedel-Prover-V2-8B
• Ремонт правкой одного идентификатора: 51/54 у эталонов, 58/85 у моделей
• Площадка: NeurIPS 2026 Workshop on AI for Verifiable Coding; рубрики cs.AI, cs.LO, cs.SE

Что менять в практике

Команды, которые строят пайплайны «LLM пишет код и доказательство, Lean проверяет», получают ясный сигнал: проверка на одной фиксированной реализации завышает надёжность. Добавьте в CI рефакторинговые варианты программы и прогоняйте доказательство против них. Если доказательство падает, сначала пробуйте дешёвые автоматические правки идентификаторов: по данным работы они закрывают значительную долю случаев. Оценивая prover-модели, смотрите не только на долю решённых задач, но и на выживание доказательств при изменении кода. Для авторов бенчмарков вывод тоже прямой: нужно измерять и стабильность, и стоимость ремонта. Второго показателя в RefactorProof пока нет.