Доказательства Lean для кода на ИИ рассыпаются после рефакторинга в 13–27% случаев

Когда языковая модель пишет код и сразу прикладывает к нему формальное математическое доказательство его корректности на языке Lean, это выглядит надёжно: программа гарантированно делает то, что от неё требуется. Но все существующие тесты проверяют доказательство только на одной, зафиксированной версии кода. А в реальной разработке код постоянно переписывают — выносят повторяющуюся логику в отдельные функции, меняют порядок операций, инвертируют условия — при этом поведение программы не меняется. Вопрос в том, выдержит ли старое доказательство такую перестройку, даже если смысл кода остался прежним.

Авторы работы предложили методику RefactorProof, чтобы это измерить. Они взяли 185 задач из известного бенчмарка VERINA (который проверяет и код, и доказательства на Lean) и применили к каждой задаче пять видов механических, полностью автоматических переписываний кода: вынос куска логики в отдельную функцию, перестановку операндов в коммутативных операциях, инверсию условий и так далее. Для каждого такого переписывания отдельно доказывалось — через Lean — что поведение программы не изменилось. В итоге получилось 458 проверенных вариантов кода. Дальше к каждому варианту прикладывали исходное доказательство (байт в байт то же самое) и смотрели, продолжает ли Lean считать его верным.

Что оказалось хрупким, а что нет

Эталонные доказательства, которые авторы VERINA написали вручную для 46 задач, пережили рефакторинг почти без потерь — доля поломок всего 4,3%. Но это не значит, что ручные доказательства надёжнее по природе: все эти 46 задач — самые простые в бенчмарке, с медианной длиной кода в одну строку, и лишь 6,5% из них рекурсивные.

Доказательства, сгенерированные специализированными моделями для доказательств — DeepSeek-Prover-V2-7B и двумя версиями Goedel-Prover-V2 (8B и 32B) — ломались намного чаще: доля неудач составила 13,3–26,8%. Но если сравнивать модели и эталон на одинаковом, сопоставимом наборе задач, картина обратная: доказательства моделей переживают рефакторинг чаще эталонных — на 15,6 п.п. для DeepSeek-7B, на 18,8 п.п. для Goedel-32B и на 20,3 п.п. для Goedel-8B. Разница статистически значима во всех трёх случаях.

Почему одни доказательства рушатся, а другие держатся

Исследователи нашли конкретный механизм устойчивости. Эталонные доказательства обычно начинаются с команды unfold, которая разворачивает определение функции прямо в тексте. Доказательства моделей чаще сначала явно называют вызов функции и её тело равными через тактику rfl (так называемый «определительный мостик»), а потом доказывают остальное автоматикой.

Когда код переносят в отдельную функцию (вынос логики), такой «мостик» работает гораздо надёжнее: на уровне задач доказательства с мостиком выживают в 6 из 6 случаев, тогда как прочие стратегии — только в 6 из 31. Но у этого приёма есть обратная сторона: если переписывание меняет само тело функции по существу (а не просто его расположение), мостик, завязанный на конкретный текст тела, перестаёт типизироваться — такие доказательства выживают лишь в 0 из 3 случаев против 17 из 19 у более общих, не завязанных на конкретную формулировку, доказательств.

Поломка — не катастрофа

Главный практический вывод: то, что доказательство перестало проходить проверку после рефакторинга, далеко не всегда означает дорогостоящую переделку. Исследователи проверили это напрямую: взяли сломанные доказательства и попытались исправить их одной простой точечной правкой — переименованием одного идентификатора. Из 54 подходящих поломок эталонных доказательств так удалось починить 51, а из 85 поломок доказательств от моделей — 58.

Для команд, которые полагаются на верифицируемую генерацию кода ИИ-моделями, вывод простой: сам факт, что доказательство перестало проходить после рефакторинга, — не повод паниковать и не показатель того, что модель в принципе хуже справляется с доказательствами. Это скорее сигнал на то, что в пайплайн верификации стоит встроить автоматическую проверку и лёгкий авторемонт доказательств после любых изменений кода, а не считать поломку финальным приговором качеству модели.