Program refactorings reveal instability in AI created proofs
How Stable Are LLM-Generated Proofs Under Program Refactoring? A Stress Test for Verifiable Code Generation
Artificial IntelligenceLogic in Computer ScienceSoftware Engineering
Summary
Proofs generated by large language models (LLMs) for code can break when the code is changed but still works the same. The authors tested hundreds of small variants of verified code and found that many AI-generated proofs don’t remain exactly the same after such changes. However, some AI prover models showed better proof stability than human-supplied references for certain tasks. They also found that fixing broken proofs after changes is often possible with small edits, meaning proof breaks don’t necessarily imply high repair work.
What this means in practice
- •For software verification teams: Check how robust AI-generated formal proofs are to code changes in verified software projects before adopting them.
- •For automated theorem prover developers: Develop more stable proof generation techniques by understanding how current proofs break under behavior-preserving code refactorings.
Authors
Aravind Mandiga, Guoming Li
Abstract
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.