面向Lean定理证明的LLM反馈蒸馏

推理模型的后训练通常将监督微调与基于可验证奖励的强化学习相结合，其中最常用的是GRPO。然而，该算法存在奖励稀疏、探索受限和模式坍缩的问题。在近期自蒸馏工作的基础上，我们提出反馈蒸馏（Feedback Distillation），一种训练方法：让模型在词元层面去匹配其自身在某个语言模型所产生的特权反馈条件下的分布。反馈蒸馏提供词元级监督，并能注入外部知识。在Lean4定理证明任务上评估我们的方法，我们发现反馈蒸馏比GRPO保持更高的生成轨迹多样性，带来更高的策略熵和更好的pass@k扩展性。两种方法互补：从反馈蒸馏检查点初始化GRPO，其表现优于单独使用任一方法。总而言之，我们的结果为改进复杂推理的后训练指出了一条有前景的路径。