Verifier‑guided self‑repair 是一种在模型再次尝试之前，利用上一次失败的验证器反馈进行条件化的技术，且不进行权重更新。\ \ 先前研究报告了两条看似冲突的结论：一方面，验证器反馈能够提升对失败的修复；另一方面，自我修复相较于独立的重新抽样几乎没有优势。\ \ 为了解决这一矛盾，我们在 Lean 定理证明环境中设计了受控的一步实验。实验固定前一次的失败结果，仅在以下维度上进行切换：是否向模型展示失败的证明文本、编译错误是否对应该失败、以及是否提供重试指令。\ \ 我们使用了冻结的 Qwen3.6‑27B（通用模型）和 DeepSeek‑Prover‑V2‑7B（专用证明模型），在 MiniF2F 难题集上进行测试。\ \ 实验揭示了两种相反的效应。展示模型其失败的前辈会显著降低成功率，并导致模型大量复制前辈的错误；但在 Qwen 上，若同时提供该尝试的编译错误，成功率可以恢复到仅使用诊断信息的水平。将前辈替换为另一定理的失败证明基本消除了成功率的下降；而在 Qwen 上，用另一问题的错误替代诊断信息会显著削弱恢复效果。若不提供失败证明，正确的诊断信息在两种模型上都未表现出相对于错误诊断的优势。失败证明的惩罚在有无重试指令的情况下均存在，而 Qwen 的诊断恢复在没有指令时更弱。\ \ 在 11 个问题、共 64 次尝试的顺序实验中，Qwen 在包含失败证明的历史中仍保留了正确诊断的收益，而 DeepSeek‑Prover 则没有出现可辨识的恢复。没有任何单步反馈条件能够超越仅指令的重新抽样，也没有在相同 token 预算下的 64 次顺序修复中出现优势。\ \ 因此，验证器反馈能够在一定程度上提升修复能力，但仍无法克服因条件化失败尝试而导致的性能损失。\ \ 点评