RefactorProof: benchmark testing stability of LLM-generated proofs under program refactoring
The paper (arXiv:2610.36328v1) introduces RefactorProof, a benchmark that derives 458 Lean-certified variants from 185 VERINA tasks to test whether proofs remain valid after behavior-preserving program refactorings. It finds low unchanged-proof survival (task-normalized structural PSR 4.3% for VERINA references; 13.3–26.8% for specialized provers) but also that specialized provers (DeepSeek-Prover-V2-7B, Goedel-Prover-V2-32B, Goedel-Prover-V2-8B) show higher unchanged-proof survival on matched tasks (+15.6, +18.8, +20.3 points respectively, 95% CIs exclude zero), and many failures can be repaired with simple one-identifier edits.