形式化定理证明中展示失败证明会降低成功率且诊断反馈难以完全抵消该损失

这篇来自 arXiv 的论文通过受控实验发现，在 Lean 定理证明任务中，向模型展示其失败的先前尝试（failed predecessor）会显著降低成功率并大幅增加对错误步骤的复制，而仅仅提供编译器错误诊断则能恢复部分性能。研究测试了冻结权重的通用模型 Qwen3.6-27B 和专用证明器 DeepSeek-Prover-V2-7B，在 MiniF2F 难题上进行了一步实验和 11 题序列实验（共 64 次尝试）。结果显示，虽然加入正确的诊断信息能让 Qwen 的性能回升至接近仅使用诊断的水平，但 DeepSeek-Prover 未能展现出类似的恢复优势。

关键证据在于，无论是否提供重试指令，展示失败证明带来的性能惩罚始终存在；即便在 64 次尝试的序列实验中保持相同的 token 预算，没有任何一种包含失败证明和正确诊断的反馈条件能建立优于单纯指令重采样的优势。这意味着验证器反馈虽然能改善特定失败点的修复质量，但无法克服因 conditioning on a failed attempt（基于失败尝试进行条件生成）而产生的整体性能损耗。对于依赖自我修复机制的 Agent 系统而言，直接丢弃失败历史可能比保留它更有效。

事实层面，实验证实了展示失败证明与成功率下降之间的强相关性，且这种效应在不同模型间表现一致。推断层面，当前的 verifier-guided self-repair 范式可能存在根本性局限，即反馈机制本身不足以弥补上下文污染带来的负面影响。猜测层面，若要在实际工程中应用此类机制，可能需要引入更复杂的去偏策略或改变训练数据分布，而非仅仅依赖推理时的提示词工程。