Distilling LLM Feedback for Lean Theorem Proving

📄 arXiv: 2605.30861v1 📥 PDF

作者: Gaetan Narozniak, Gérard Biau, Rémi Munos, Ahmad Rammal, Pierre Marion

分类: cs.AI

发布日期: 2026-05-29

💡 一句话要点

提出Feedback Distillation，利用LLM反馈提升Lean定理证明性能

🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture)

关键词: 定理证明 强化学习 语言模型 蒸馏学习 反馈机制

📋 核心要点

  1. 现有定理证明模型后训练方法（如GRPO）面临奖励稀疏、探索不足和模式崩溃等挑战。
  2. Feedback Distillation通过让模型学习匹配自身在LLM反馈下的token分布，实现token级监督和知识注入。
  3. 实验表明，Feedback Distillation能提升轨迹多样性，改善策略熵和pass@k指标，且与GRPO互补。

📝 摘要（中文）

推理模型的后训练通常结合监督微调和来自可验证奖励的强化学习，最常见的是GRPO。然而，该算法存在奖励稀疏、探索有限和模式崩溃的问题。受自蒸馏研究的启发，我们提出了一种名为Feedback Distillation的训练方法，该方法训练模型在token级别上匹配其自身的分布，该分布以语言模型产生的特权反馈为条件。Feedback Distillation提供token级别的监督，并可以注入外部知识。在Lean4定理证明的评估中，我们发现Feedback Distillation比GRPO在生成的轨迹中保持更大的多样性，从而产生更高的策略熵和更好的pass@k缩放。这两种方法是互补的：从Feedback Distillation检查点初始化GRPO优于单独使用任何一种方法。总而言之，我们的结果表明，这是一种有希望的途径来改进复杂推理的后训练。

🔬 方法详解

问题定义：论文旨在解决定理证明任务中，现有强化学习方法（如GRPO）在后训练阶段遇到的问题，包括奖励信号稀疏、探索能力不足以及容易陷入模式崩溃等。这些问题限制了模型在复杂推理任务中的性能提升。

核心思路：论文的核心思路是利用大型语言模型（LLM）提供的反馈作为特权信息，通过蒸馏的方式引导模型学习。具体来说，模型被训练成模仿自身在接收到LLM反馈后生成的token分布。这种方法提供了token级别的监督信号，克服了奖励稀疏的问题，并允许模型从LLM中学习外部知识。

技术框架：Feedback Distillation的整体框架包含以下几个主要步骤：1) 使用一个预训练的定理证明模型作为初始模型。2) 使用该模型生成定理证明的轨迹。3) 使用一个大型语言模型（LLM）对生成的轨迹进行评估，并提供反馈。4) 使用Feedback Distillation算法，训练模型匹配自身在LLM反馈下的token分布。训练目标是最小化模型预测的token分布与目标分布之间的差异，目标分布由模型自身在接收到LLM反馈后生成。

关键创新：该方法最重要的创新点在于利用LLM的反馈作为一种特权信息，通过蒸馏的方式来指导模型的训练。与传统的强化学习方法相比，Feedback Distillation提供了更密集的监督信号，避免了奖励稀疏的问题。此外，该方法还可以将LLM的知识迁移到定理证明模型中，从而提高模型的推理能力。

关键设计：在具体实现上，Feedback Distillation的关键设计包括：1) 使用交叉熵损失函数来衡量模型预测的token分布与目标分布之间的差异。2) 使用Adam优化器来训练模型。3) 可以通过调整LLM反馈的强度来控制知识迁移的程度。4) 可以将Feedback Distillation与GRPO等强化学习方法结合使用，以进一步提高模型的性能。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，Feedback Distillation在Lean4定理证明任务上优于传统的GRPO方法。具体来说，Feedback Distillation能够生成更多样化的轨迹，提高策略熵，并改善pass@k指标。此外，将Feedback Distillation与GRPO结合使用可以进一步提高模型的性能，表明这两种方法具有互补性。

🎯 应用场景

该研究成果可应用于定理证明、代码生成、数学问题求解等需要复杂推理能力的领域。通过利用大型语言模型的知识，可以提升模型在这些任务上的性能和泛化能力。此外，该方法还可以推广到其他需要密集监督信号的强化学习任务中，具有广泛的应用前景。

📄 摘要（原文）

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.