Metraipolis › archive › dc_e0872bcff5a2

Repair, Retry, and the Cost of Hindsight: Verifier Feedback in Formal Theorem Proving — arXiv:2610.22698

Source: arXiv (en)
Original: https://arxiv.org/abs/2610.22698
License (as archived): CC0-1.0
Archived: 2026-10-19T08:42:11.591Z
SHA-256 of the archived text: 860646a0c464e74b42f05c15eb413cccfc0b069f2af7bbe322192b50fe89247c
Stable URL of this page: https://metraipolis.com/documento/dc_e0872bcff5a2

How to cite

Repair, Retry, and the Cost of Hindsight: Verifier Feedback in Formal Theorem Proving — arXiv:2610.22698 — arXiv (en), https://arxiv.org/abs/2610.22698 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_e0872bcff5a2 (Metraipolis archive dc_e0872bcff5a2, sha256 860646a0c464e74b42f05c15eb413cccfc0b069f2af7bbe322192b50fe89247c)

BibTeX

@misc{dce0872bcff5a2,
  title = {Repair, Retry, and the Cost of Hindsight: Verifier Feedback in Formal Theorem Proving — arXiv:2610.22698},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2610.22698},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_e0872bcff5a2; sha256 860646a0c464e74b42f05c15eb413cccfc0b069f2af7bbe322192b50fe89247c},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2610.22698. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

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.

Tema degli esploratori: agenti e intelligenza artificiale (elenco arXiv cs.AI, nuovi lavori del giorno).
Categorie arXiv: Artificial Intelligence (cs.AI).
Pagina del lavoro: https://arxiv.org/abs/2610.22698 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-10-19T08:39:10.025Z dalla pagina https://arxiv.org/list/cs.AI/new (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).