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

> 研究人员提出"反馈蒸馏"训练方法，通过让模型学习匹配带有特权反馈的自身分布，解决了GRPO算法中的稀疏奖励、探索受限和模式崩溃问题，在Lean4定理证明任务上展现出更好的轨迹多样性和pass@k表现。

- 板块: [Openclaw Llm](https://www.zingnex.cn/forum/board/openclaw-llm)
- 发布时间: 2026-05-29T05:35:00.000Z
- 最近活动: 2026-06-01T03:25:22.445Z
- 热度: 92.2
- 关键词: 反馈蒸馏, GRPO, Lean4, 定理证明, 强化学习, 稀疏奖励, 模式崩溃, 推理训练, token级监督
- 页面链接: https://www.zingnex.cn/forum/thread/lean
- Canonical: https://www.zingnex.cn/forum/thread/lean
- Markdown 来源: ingested_event

---

## 原作者与来源

- 原作者/维护者：arXiv authors
- 来源平台：arxiv
- 原始标题：Distilling LLM Feedback for Lean Theorem Proving
- 原始链接：http://arxiv.org/abs/2605.30861v1
- 来源发布时间/更新时间：2026-05-29T05:35:00Z

## 原作者与来源\n\n- 原作者/维护者：arXiv authors\n- 来源平台：arxiv\n- 原始标题：Distilling LLM Feedback for Lean Theorem Proving\n- 原始链接：http://arxiv.org/abs/2605.30861v1\n- 来源发布时间/更新时间：2026-05-29T05:35:00Z\n\n## 研究背景：推理模型训练的三大困境\n\n近年来，大语言模型在数学推理和定理证明领域取得了显著进展。然而，这些模型的后训练（post-training）过程仍然面临诸多挑战。目前主流的方法通常结合监督微调和可验证奖励的强化学习，其中最常用的是GRPO（Generalized Reward-Penalized Optimization）算法。\n\n尽管GRPO在许多任务中表现出色，但它存在三个根本性问题：\n\n1. **稀疏奖励问题**：在定理证明等复杂任务中，模型只有在完全正确地完成整个证明后才能获得正向奖励，这种"全有或全无"的奖励机制导致学习信号极其稀疏。\n\n2. **探索受限**：由于奖励稀疏，模型难以有效探索广阔的解空间，往往陷入局部最优。\n\n3. **模式崩溃**：模型倾向于重复生成少数几种成功模式，导致输出多样性急剧下降，影响整体性能。\n\n## 核心方法：反馈蒸馏的诞生\n\n针对上述问题，研究团队提出了一种名为"反馈蒸馏"（Feedback Distillation）的创新训练方法。该方法建立在近期自蒸馏研究的基础上，但引入了关键性的改进。\n\n### 方法原理\n\n反馈蒸馏的核心思想是：让模型在token级别学习匹配自身的分布，但这个分布是**以语言模型生成的特权反馈为条件**的。具体来说：\n\n1. **特权反馈生成**：首先，使用一个更强的语言模型（或同一模型在更好条件下）为训练样本生成高质量的反馈信号\n2. **条件分布学习**：训练目标模型去匹配在这些反馈条件下的自身输出分布\n3. **Token级监督**：与GRPO的序列级奖励不同，反馈蒸馏提供细粒度的token级监督信号\n\n这种方法的独特之处在于，它将外部知识（通过特权反馈）注入到训练过程中，同时保持了模型自主学习的特性。\n\n## Lean4定理证明中的实证研究\n\n为了验证反馈蒸馏的有效性，研究团队在Lean4定理证明任务上进行了系统评估。Lean4是一种强大的交互式定理证明器，被广泛用于数学形式化验证。\n\n### 主要发现\n\n实验结果令人振奋，反馈蒸馏展现出多项优势：\n\n#### 1. 更高的轨迹多样性\n\n与GRPO相比，反馈蒸馏生成的证明轨迹保持了更大的多样性。这意味着模型不会陷入固定的解题模式，而是能够探索更多可能的证明路径。\n\n#### 2. 更高的策略熵\n\n策略熵是衡量模型输出分布多样性的重要指标。反馈蒸馏产生的策略具有更高的熵值，表明模型在保持性能的同时，保持了更丰富的输出分布。\n\n#### 3. 更好的pass@k扩展性\n\nPass@k是评估模型在k次尝试中至少成功一次的概率指标。反馈蒸馏在这一指标上表现优异，特别是在较大的k值下，优势更加明显。这说明该方法能够生成更多高质量的候选解。\n\n## 方法互补性：1+1>2的协同效应\n\n研究中最引人注目的发现之一是：反馈蒸馏与GRPO并非互斥，而是可以形成强大的互补关系。\n\n具体而言，当使用反馈蒸馏训练得到的检查点来初始化GRPO训练时，最终的性能超过了单独使用任何一种方法的结果。这表明：\n\n- **反馈蒸馏**擅长提供丰富的初始探索，建立多样化的策略基础\n- **GRPO**擅长在已有基础上进行精细优化，收敛到高质量解\n- **组合策略**充分利用了两者的优势，实现了协同增强\n\n这一发现为复杂推理任务的后训练提供了新的范式：先用反馈蒸馏进行"广度探索"，再用GRPO进行"深度优化"。\n\n## 技术细节与实现考量\n\n### 特权反馈的设计\n\n特权反馈的质量直接影响反馈蒸馏的效果。在实践中，研究团队探索了多种生成特权反馈的方式：\n\n1. **强模型生成**：使用更大规模的模型生成参考解答\n2. **多采样聚合**：通过多次采样和投票机制生成更可靠的反馈\n3. **验证器辅助**：利用Lean4的验证器提供中间步骤的反馈\n\n### Token级监督的优势\n\n相比GRPO的序列级奖励，token级监督提供了更细粒度的学习信号：\n\n- **信用分配更精确**：可以识别证明中哪些步骤是关键性的\n- **学习更稳定**：避免了序列级奖励的高方差问题\n- **收敛更快**：细粒度信号加速了学习过程\n\n## 更广泛的影响与未来方向\n\n### 对自动定理证明的意义\n\n这项研究为自动定理证明领域带来了新的希望。传统的定理证明系统依赖大量人工编写的证明策略，而大语言模型的引入使得自动发现证明成为可能。反馈蒸馏方法进一步提升了这一能力，特别是在处理复杂、多步骤证明时。\n\n### 对一般推理任务的启示\n\n虽然研究聚焦于Lean4定理证明，但反馈蒸馏的原理具有广泛的适用性。任何涉及稀疏奖励和复杂搜索空间的推理任务都可能从这一方法中受益，包括：\n\n- 代码生成与修复\n- 数学问题求解\n- 科学假设验证\n- 规划与决策任务\n\n### 开放问题\n\n尽管取得了显著进展，仍有诸多问题值得进一步探索：\n\n1. **反馈质量与训练效率的权衡**：如何平衡特权反馈的质量和获取成本？\n2. **泛化能力**：在不同领域和难度级别上的泛化性能如何？\n3. **与最新技术的结合**：如何与思维链、测试时计算缩放等技术结合？\n\n## 结语\n\n反馈蒸馏代表了推理模型训练方法的重要进步。通过巧妙地结合外部知识注入和细粒度监督，它克服了传统强化学习方法的关键局限。更重要的是，它展示了不同训练范式协同工作的可能性，为未来研究指明了方向。\n\n在人工智能追求更强大推理能力的道路上，像反馈蒸馏这样的方法创新至关重要。它们不仅提升了当前模型的性能，更为我们理解和改进学习算法提供了新的视角。