形式化定理证明中的验证器反馈：修复、重试与后见之明的代价

研究人员在 Lean 定理证明中测试了 Qwen3.6-27B 与 DeepSeek-Prover-V2-7B，发现让模型看到上一轮失败证明会降低成功率并加剧抄袭，而编译器错误诊断仅能部分弥补该损失。在 MiniF2F 困难问题及多达 64 次尝试的序列实验中，任何单步反馈条件在相同 token 预算下均未超越仅靠指令的独立重采样。验证器反馈虽能改善修复，但无法克服因参考失败尝试带来的性能损耗。