RefactorProof: бенчмарк стабильности доказательств LLM при рефакторинге кода
Статья (arXiv:2610.36328v1) представляет RefactorProof — набор из 458 Lean-проверенных вариантов, полученных из 185 задач VERINA, для проверки, остаются ли доказательства действительными после сохраняющего поведение рефакторинга. Авторы обнаруживают низкую выживаемость неизменённых доказательств (PSR 4,3% для эталонов VERINA; 13,3–26,8% для специализированных проверов), но специализированные проверы (DeepSeek-Prover-V2-7B, Goedel-Prover-V2-32B, Goedel-Prover-V2-8B) показывают более высокую выживаемость на сопоставимых задачах (+15,6; +18,8; +20,3 пункта соответственно, 95% ДИ не включают ноль), и многие ошибки удаётся исправить простыми изменением идентификатора.