arXiv cs.AI· Jack Li, Sophia Li·· 12 小时前AI 评分34
修复、重试与事后成本：形式定理证明中的验证器反馈
Repair, Retry, and the Cost of Hindsight: Verifier Feedback in Formal Theorem Proving
AI 导读
在 Lean 定理证明中，向模型展示失败证明会降低成功率并显著增加对失败证明的复制，而附加该次尝试的编译器错误可将损失恢复到仅给诊断的水平。研究测试了冻结的 Qwen3.6-27B 与 DeepSeek-Prover-V2-7B 在困难 MiniF2F 问题上的表现，发现将失败证明替换为其他定理的失败证明可基本消除性能退化。
正文 · 原文
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.
| Comments: | NeurIPS 2026 Workshop on AI for Verifiable Coding |
| Subjects: | Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2610.22698 [cs.AI] |
| (or arXiv:2610.22698v1 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2610.22698 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Sophia Li [view email]
[v1]
Thu, 15 Oct 2026 22:03:07 UTC (2,487 KB)
来源：arXiv cs.AI · arxiv.org