RefactorProof 测试显示 LLM 生成的证明在代码重构下存在显著不稳定性

该研究引入 RefactorProof 基准，通过 458 个 Lean 认证变体测试 185 个 VERINA 任务，发现程序重构会暴露生成证明的结构性脆弱：参考实现的归一化结构 PSR 为 4.3%，而专用证明器（specialized provers）的范围在 13.3% 至 26.8% 之间。尽管 DeepSeek-Prover-V2-7B、Goedel-Prover-V2-32B 和 Goedel-Prover-V2-8B 在匹配任务上的未改变证明存活率比参考实现高出 15.6 至 20.3 个百分点，但这仅衡量了证明在重构后的静态稳定性，而非动态维护成本。

关键证据在于，虽然证明失效频繁发生，但修复成本极低：预定义的单一标识符编辑即可修复 51/54 个参考实现的结构失效案例和 58/85 个证明器的失效案例。这表明模型生成的证明虽然在语义上保持有效，但在代码结构变化时极易断裂，需要极小的修改即可恢复，这种“高存活率”可能掩盖了实际工程中的维护负担。

事实层面，该研究证实了当前可验证代码生成模型在代码重构场景下的脆弱性；推断层面，现有的基准测试若仅基于固定实现，可能高估了模型在实际开发环境中的可用性；猜测层面，未来的评估体系需将“修复成本”纳入核心指标，否则无法真实反映 AI 辅助编程工具在生产代码库中的长期价值。