arXiv cs.AI· Jack Li, Sophia Li·· 11 小时前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 问题上的表现，发现将失败证明替换为其他定理的失败证明可基本消除性能退化。
正文 · AI 翻译
摘要：验证器引导的自我修复让模型以失败尝试的反馈为条件，然后再试一次，且不更新权重。然而，先前工作中的两项发现相互矛盾：验证器反馈可以改善对失败的修复，但自我修复本身相比独立重采样几乎没有优势。我们在 Lean 定理证明中通过受控的单步实验来调和这些发现，实验固定先前的失败，同时改变是否展示失败的证明、编译器错误是否对应该失败，以及重试指令。我们在困难的 MiniF2F 问题上测试了冻结的 Qwen3.6-27B（通用模型）和 DeepSeek-Prover-V2-7B（专用证明器）。我们发现两种相反的效果。向模型展示其失败的前驱会降低成功率，并急剧增加对其的复制；而在 Qwen 上，加入该尝试的编译器错误可以恢复损失，达到仅提供诊断信息的水平。用另一个定理的失败证明替换前驱，在很大程度上消除了两个模型上的性能下降；在 Qwen 上，用另一个问题的错误替换诊断信息会大幅降低恢复效果。在没有失败证明的情况下，正确的诊断信息在两个模型上都没有表现出相对于错误诊断对照组的已解决优势。失败证明惩罚在有无重试指令时都持续存在，而 Qwen 的诊断恢复在没有重试指令时较弱。在通过 64 次尝试进行的 11 问题顺序实验中，Qwen 在失败证明历史中保留了正确诊断的益处，而 DeepSeek-Prover 没有表现出已解决的恢复。然而，没有任何测试过的单步反馈条件能建立相对于仅指令重采样的优势，在相同 token 预算下，使用失败证明和正确诊断的 64 次尝试顺序修复也没有。因此，验证器反馈可以改善修复，但无法克服以失败尝试为条件所带来的性能损失。
| 评论： | NeurIPS 2026 可验证编码 AI 研讨会 |
| 主题： | 人工智能（cs.AI） |
| 引用为： | arXiv:2610.22698 [cs.AI] |
| （或 arXiv:2610.22698v1 [cs.AI] 为此版本） | |
| https://doi.org/10.48550/arXiv.2610.22698 arXiv 颁发的 DOI 通过 DataCite（待注册） |
提交历史
来自：Sophia Li [查看电子邮件]
[v1]
2026年10月15日星期四 22:03:07 UTC（2,487 KB）
来源：arXiv cs.AI · arxiv.org