Verifier feedback helps repair but can worsen theorem proving attempts
Repair, Retry, and the Cost of Hindsight: Verifier Feedback in Formal Theorem Proving
Artificial Intelligence
Summary
When trying to prove math problems using computers, showing a model its past failed attempts usually makes it worse at fixing mistakes because the model tends to copy errors. However, if the model also sees the exact compiler error from the failure, it can recover and improve its fixing ability. The paper finds that just re-trying with instructions but without showing previous failures can be as effective as including verifier feedback. So, while feedback can help, it doesn't fully overcome issues caused by focusing on past failures.
What this means in practice
- •For software developers: Improve automated proof checking tools by understanding when verifier feedback helps or hurts fix attempts.
- •For ai system builders: Design AI models for formal reasoning that balance feedback use to avoid performance loss from failed proof conditioning.
Authors
Jack Li, Sophia Li
Abstract
Verifier-guided self-repair conditions a model on feedback from failed attempts before it tries again, without weight updates. Yet two findings in prior work are in tension: verifier feedback can improve repair of failures, but self-repair itself can provide little-to-no advantage over independent resampling. We reconcile these findings in Lean theorem proving through controlled one-step experiments that hold the preceding failure fixed while varying whether the failed proof is shown, whether the compiler error corresponds to that failure, and the retry instruction. We test frozen Qwen3.6-27B, a general-purpose model, and DeepSeek-Prover-V2-7B, a specialized prover, on difficult MiniF2F problems. We find two opposing effects. Showing the model its failed predecessor reduces success and sharply increases copying of it, while on Qwen adding that attempt's compiler error recovers the loss, to the level of the diagnostic alone. Replacing the predecessor with another theorem's failed proof largely removes the degradation on both models; on Qwen, replacing the diagnostic with another problem's error substantially reduces the recovery. Without the failed proof, correct diagnostics show no resolved advantage over wrong-diagnostic controls on either model. The failed-proof penalty persists with and without the retry instruction, whereas Qwen's diagnostic recovery is weaker without it. In 11-problem sequential experiments through 64 attempts, Qwen retains a correct-diagnostic benefit within failed-proof histories, while DeepSeek-Prover shows no resolved recovery. However, no tested one-step feedback condition establishes an advantage over instruction-only resampling, nor does 64-attempt sequential repair with failed proofs and correct diagnostics at equal token budgets. Verifier feedback can thus improve repair without overcoming the performance loss from conditioning on a failed attempt.