RESEARCH · RESEARCH · #2701
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.
KEY POINTS
- 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.
- This matters because it exposes brittleness in verifiable code generation—proofs that validate one implementation often break under harmless refactorings, affecting reliability and deployment of automated proof-generation systems.
WHY IT MATTERS
This matters because it exposes brittleness in verifiable code generation—proofs that validate one implementation often break under harmless refactorings, affecting reliability and deployment of automated proof-generation systems.