反馈蒸馏：让大语言模型在Lean定理证明中实现更高效的推理训练

本文基于arXiv 2026年5月发布的论文《Distilling LLM Feedback for Lean Theorem Proving》（链接：http://arxiv.org/abs/2605.30861v1）。研究人员提出"反馈蒸馏"训练方法，解决GRPO算法在Lean4定理证明中的稀疏奖励、探索受限和模式崩溃问题，展现出更好的轨迹多样性和pass@k表现，且与GRPO形成互补协同效应。

主流定理证明模型后训练常结合监督微调和GRPO强化学习，但GRPO存在三个核心问题：1.稀疏奖励：仅完成完整证明获正向奖励，学习信号不足；2.探索受限：奖励稀疏导致难以探索广阔解空间，易陷局部最优；3.模式崩溃：重复少数成功模式，输出多样性下降。

反馈蒸馏的核心是让模型在token级别学习匹配自身以特权反馈为条件的分布：1.特权反馈生成：用更强模型或优化条件生成高质量反馈；2.条件分布学习：训练模型匹配反馈条件下的自身输出分布；3.Token级监督：提供细粒度学习信号，区别于GRPO的序列级奖励。

在Lean4定理证明任务中，反馈蒸馏表现出显著优势：1.轨迹多样性更高，避免固定解题模式；2.策略熵更高，保持丰富输出分布；3.pass@k扩展性更好，尤其大k值下优势明显，生成更多高质量候选解。

反馈蒸馏与GRPO可协同增强：用反馈蒸馏检查点初始化GRPO训练，性能超过单独使用任一方法。反馈蒸馏擅长广度探索建立多样化策略基础，GRPO擅长深度优化收敛到高质量解，形成"广度探索+深度优化"新范式。

-特权反馈设计：采用强模型生成参考解答、多采样聚合、验证器辅助三种方式提升反馈质量；-Token级监督优势：信用分配更精确（识别关键步骤）、学习更稳定（避免高方差）、收敛更快（细粒度信号加速学习）。

-自动定理证明意义：减少人工策略依赖，提升复杂多步骤证明能力；-一般推理任务启示：适用于代码生成、数学求解、科学验证等稀疏奖励任务；-开放问题：反馈质量与成本权衡、跨领域泛化能力、与思维链等技术结合。

反馈蒸馏通过外部知识注入和细粒度监督，克服传统强化学习局限，展示不同训练范式协同的可能性。它不仅提升当前模型性能，更为AI推理能力发展提供新视角和方向。