RefactorProof 基准：检验 LLM 生成证明在代码重构下的稳定性
How Stable Are LLM-Generated Proofs Under Program Refactoring? A Stress Test for Verifiable Code Generation
Lean 形式化证明重构后还成立吗？这篇用 458 个变体实测了 DeepSeek-Prover 和 Goedel-Prover 的证明有多脆，结果挺反直觉。
论文提出 RefactorProof 基准，从 185 个 VERINA 任务中派生出 458 个经 Lean 认证的行为保持重构变体，检验证明在重构后是否仍然有效。结果显示结构化重构会暴露证明的脆弱性：任务归一化结构 PSR 在参考证明上为 4.3%，在专用证明模型上达 13.3-26.8%。但在匹配任务上，专用证明器的未变证明存活率高于参考证明，DeepSeek-Prover-V2-7B 高出 15.6 个百分点，Goedel-Prover-V2-32B 和 8B 分别高出 18.8 和 20.3 个百分点。修复成本方面，预定义的单标识符编辑可修复 51/54 个合格参考证明结构失败和 58/85 个合格证明器失败。
How Stable Are LLM-Generated Proofs Under Program Refactoring? A Stress Test for Verifiable Code Generation
Benchmarks for verifiable code generation usually test a proof against one fixed implementation. We ask whether the same proof remains valid after a program refactoring that preserves behavior. We introduce RefactorProof, which derives 458 Lean-certified variants from the 185 VERINA tasks that compile in our pinned environment while holding the specification and evaluated proof fixed byte-for-byte. VERINA supplies reference proofs for 46 tasks, all from its basic split; the primary model-versus-reference comparisons further match on 21-25 short, non-recursive tasks. Structural refactorings expose substantial brittleness across proof sources: task-normalized structural PSR is 4.3% for the supplied references and 13.3-26.8% for the specialized provers. On the matched tasks, specialized prover proofs nevertheless have higher overall unchanged-proof survival than the supplied reference artifacts: +15.6 points for DeepSeek-Prover-V2-7B, +18.8 for Goedel-Prover-V2-32B, and +20.3 for Goedel-Prover-V2-8B; all three 95% CIs exclude zero. The ordering persists after excluding universally survived T1 variants, under family-balanced aggregation, and under alternative deployable valid-proof selection rules. However, unchanged-proof failure is not the same as high repair cost: predefined one-identifier edits repair 51/54 eligible reference structural failures and 58/85 eligible prover failures. RefactorProof therefore measures unchanged-proof stability under program refactoring, not the cost of maintaining a proof after it breaks.
