用自反馈蒸馏提升大模型推理多样性，助力形式化证明
Distilling LLM Feedback for Lean Theorem Proving
- 让模型模仿自身在优质反馈下的生成分布，实现逐词监督
- 在Lean4上使策略熵更高，pass@k表现更好，轨迹更丰富
- 适合需要高多样性推理的复杂任务，如数学证明与逻辑推导
推理模型的后训练通常结合监督微调与基于可验证奖励的强化学习，最常见的是GRPO算法。但该方法存在奖励稀疏、探索有限和模式崩溃等问题。受自蒸馏启发，我们提出反馈蒸馏（Feedback Distillation），让模型在逐词层面匹配其自身在特权反馈条件下的输出分布。该方法提供细粒度监督，并可注入外部知识。在Lean4形式化证明任务上的评估表明，反馈蒸馏生成的轨迹更具多样性，政策熵更高，且在pass@k指标上表现出更优的扩展性。两种方法互补：以反馈蒸馏初始化的GRPO性能优于单独使用任一方法。结果表明，该方向为复杂推理的后训练提供了有前景的改进路径。
原文摘要 · Abstract (English)
Post-training for reasoning models typically combines supervised fine-tuning with reinforcement learning from verifiable rewards, most commonly with GRPO. However, this algorithm suffers from sparse rewards, limited exploration, and mode collapse. Building upon recent works on self-distillation, we propose Feedback Distillation, a training method where the model is trained to match, at the token level, its own distribution conditioned on privileged feedback produced by a language model. Feedback Distillation offers token-level supervision and can inject external knowledge. Evaluating our method for Lean4 theorem-proving, we find that Feedback Distillation maintains greater diversity in generated trajectories than GRPO, yielding higher policy entropy and better pass@k scaling. The two methods are complementary: initializing GRPO from a Feedback Distillation checkpoint outperforms either method alone. All in all, our results suggest a promising avenue to improve post-training for complex reasoning.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。