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

# 将LLM反馈提炼用于Lean定理证明 来源：https://arxiv.org/html/2605.30861 Gaëtan Narozniak FAIR at Meta, Inria gaetan@meta\.com &Gérard Biau Sorbonne Université, Institut universitaire de France &Rémi Munos FAIR at Meta Ahmad Rammal FAIR at Meta, CERMICS École des Ponts ParisTech &Pierre Marion Inria, ENS, PSL Research University pierre\.marion@inria\.fr ###### 摘要 推理模型的后训练通常将监督微调与基于可验证奖励的强化学习（最常用的是GRPO）相结合。然而，该算法存在奖励稀疏、探索受限和模式崩溃的问题。基于近期关于自蒸馏的研究，我们提出了**反馈蒸馏**，这是一种训练方法，其中模型在token级别被训练去匹配其自身在带有由语言模型产生的特权反馈条件下的分布。反馈蒸馏提供了token级别的监督，并且可以注入外部知识。在评估我们的方法用于Lean 4定理证明时，我们发现反馈蒸馏比GRPO在生成的轨迹中保持了更大的多样性，带来了更高的策略熵和更好的pass@k缩放。这两种方法是互补的：从反馈蒸馏检查点初始化GRPO优于单独使用任何一种方法。总体而言，我们的结果提示了一种改进复杂推理后训练的有前景的途径。 ## 1 引言 近来AI的进展在复杂推理任务中展示了显著的进步（Liet al\.,2022（https://arxiv.org/html/2605.30861#bib.bib40）；Rozièreet al\.,2023（https://arxiv.org/html/2605.30861#bib.bib41）；Yaoet al\.,2023（https://arxiv.org/html/2605.30861#bib.bib43）；Bestaet al\.,2024（https://arxiv.org/html/2605.30861#bib.bib44）；Reinet al\.,2024（https://arxiv.org/html/2605.30861#bib.bib42））。数学推理因其具有挑战性的搜索空间、明确的正确性标准以及从形式定理证明到非形式问题解决的丰富问题结构，已成为这些方法特别有价值的测试平台（Lightmanet al\.,2023（https://arxiv.org/html/2605.30861#bib.bib38）；Trinhet al\.,2024（https://arxiv.org/html/2605.30861#bib.bib39）；Hubertet al\.,2025（https://arxiv.org/html/2605.30861#bib.bib31）；Peyronnetet al\.,2026（https://arxiv.org/html/2605.30861#bib.bib34））。一种富有成效的策略使用可验证奖励，其中确定性验证器（例如，Lean证明检查器）评估模型输出。在这种设置下，最先进的后训练流程将基于专家解决方案（来自人类专家或更强的LLM）的监督微调（SFT）与最大化验证器提供奖励的强化学习（RL）相结合（Kumaret al\.,2025（https://arxiv.org/html/2605.30861#bib.bib32））。RL算法通常是GRPO（Shaoet al\.,2024（https://arxiv.org/html/2605.30861#bib.bib33）），该算法对每个提示采样多个输出并通过对比它们的奖励来优化策略。 然而，这种SFT+GRPO范式有显著的局限性。首先，SFT阶段受限于生成微调数据集的难度和成本。此外，由于它在离策略的示范上进行训练，可能导致在狭窄的微调分布之外出现灾难性遗忘（例如，参见Ross and Bagnell，2010（https://arxiv.org/html/2605.30861#bib.bib20）；Agarwalet al\.,2024（https://arxiv.org/html/2605.30861#bib.bib21）；Shenfeldet al\.,2026（https://arxiv.org/html/2605.30861#bib.bib2））。而且，与流行的观点（即RL训练会带来新的推理能力）相反，最近的证据表明GRPO不会放大模型答案的多样性，也不会在训练中促进探索，而是会坍缩到RL训练前已经存在的高奖励模式上（Yueet al\.,2025（https://arxiv.org/html/2605.30861#bib.bib1））。这在形式数学中尤其成问题，因为探索大型引理库（例如，Lean的Mathlib，The mathlib Community，2020（https://arxiv.org/html/2605.30861#bib.bib7））对于成功至关重要。最后，GRPO仅提供轨迹级别的奖励，当所有样本都失败时，这无法提供学习信号。这些相互关联的挑战促使我们探索替代的训练机制。 一个有前景的方法是最近提出的自蒸馏算法（Hübotteret al\.,2026（https://arxiv.org/html/2605.30861#bib.bib3）；Shenfeldet al\.,2026（https://arxiv.org/html/2605.30861#bib.bib2）；Zhaoet al\.,2026（https://arxiv.org/html/2605.30861#bib.bib11）），它训练模型在条件于特权信息时模仿其自身输出，有效地将提示策略直接蒸馏到模型权重中。这种在策略的方法很有吸引力，因为它提供了细粒度的token级别信用分配，而不是在整个轨迹上均匀分配奖励（参见图1（https://arxiv.org/html/2605.30861#S1.F1）中的示例）。此外，它可以应用于可验证奖励设置之外，因为它不直接依赖于验证器信号，尽管在我们的设置中我们也利用了验证器输出。 参见说明图1：MiniF2F数据集（Zhenget al\.,2022（https://arxiv.org/html/2605.30861#bib.bib9））中一个Lean语句上的反馈蒸馏示例，使用Qwen3-8B作为学生。Claude对学生的尝试提供反馈。然后，学生的回答按token进行着色，颜色由log⁡pteacher−log⁡pstudent\\log p\_\{\\text\{teacher\}\}\-\\log p\_\{\\text\{student\}\}决定：绿色token是教师偏好的，红色token是学生偏好的，白色token被分配大致相等的概率。学生写下“π\\pi”，而教师有98%的概率会写下“Real”，这反映了Claude的反馈。通过KL损失，学生被训练去增加在该位置“Real”的概率，从而学习编写更好的Lean代码。 #### 贡献。 在这项工作中，我们研究了自蒸馏在训练LLM用于数学方面的性能。更准确地说， - •我们提出了**反馈蒸馏**，这是自蒸馏的一个变体，其中特权信息是由模型的一个冻结副本或第三方LLM根据模型的尝试和验证器的输出产生的反馈，而不是原始的环境信号或真实解决方案（第3节（https://arxiv.org/html/2605.30861#S3））。 - •我们在Lean 4形式数学环境中评估了反馈蒸馏（第4节（https://arxiv.org/html/2605.30861#S4））。我们展示了它比GRPO保持了更高的策略熵，并实现了更好的pass@k缩放，表明更大的输出多样性。此外，我们表明这两种方法是互补的：从反馈蒸馏检查点初始化GRPO优于单独使用GRPO。在LeanWorkbook上训练后，Qwen3.5-9B在LeanWorkbook的测试集上单独使用GRPO达到了59%的pass@1测试准确率，而使用反馈蒸馏+GRPO则达到了75%。 - •我们提供了对反馈蒸馏的详细分析：我们与其他反馈来源进行了比较，并讨论了训练不稳定性以及我们训练方法的定性后果，这可以看作是一种在策略的知识迁移（第5节（https://arxiv.org/html/2605.30861#S5））。 ## 2 相关工作 #### LLM的自蒸馏。 最近的一系列工作通过最小化学生和教师（共享相同架构但条件于特权信息）之间的散度来训练LLM。Hübotteret al\.（2026（https://arxiv.org/html/2605.30861#bib.bib3））使用环境输出作为特权信号，而Shenfeldet al\.（2026（https://arxiv.org/html/2605.30861#bib.bib2））；Zhaoet al\.（2026（https://arxiv.org/html/2605.30861#bib.bib11））使用真实解决方案作为特权信息。我们的工作通过使用来自模型冻结副本或第三方LLM的反馈扩展了这一研究方向。此外，我们对自蒸馏的性质进行了仔细分析，特别证明了它比GRPO保持了更大的轨迹多样性，当从一个弱学生开始在困难的RL环境（形式数学）中进行训练时，这转化为更好的测试时缩放。 #### 形式数学的RL。 形式数学中最先进的证明器通常遵循两阶段流程（Linet al\.,2025（https://arxiv.org/html/2605.30861#bib.bib13）；Renet al\.,2025（https://arxiv.org/html/2605.30861#bib.bib14））：先对来自自然语言证明形式化的合成证明数据进行监督微调，然后进行基于GRPO的RL，通常称为基于可验证奖励的强化学习（RLVR）。在MiniF2F（Zhenget al\.,2022（https://arxiv.org/html/2605.30861#bib.bib9））和PutnamBench（Tsoukalaset al\.,2024（https://arxiv.org/html/2605.30861#bib.bib22））等基准测试上的最新进展越来越多地来自测试时缩放，而不是改进的训练（例如，Varamballyet al\.,2026（https://arxiv.org/html/2605.30861#bib.bib15））。这种缩放是通过结合了经过训练的证明器、推理模型以及与Lean环境迭代交互的智能体流程来实现的。虽然这些脚手架策略与我们的工作是正交的，但它们强调了强大基础证明器的持续重要性，我们的目标正是改进这些证明器的训练。 ## 3 反馈蒸馏 遵循自蒸馏方法（Hübotteret al\.,2026（https://arxiv.org/html/2605.30861#bib.bib3）；Shenfeldet al\.,2026（https://arxiv.org/html/2605.30861#bib.bib2）；Zhaoet al\.,2026（https://arxiv.org/html/2605.30861#bib.bib11）），我们的训练损失衡量同一个模型的两个独立权重实例（*学生*和*教师*，后者在其提示中接收特权信息）之间的散度。两个实例都从同一个预训练的LLMπ\\pi初始化。我们试图在一个拥有无解问题数据集DD（例如，无证明的Lean语句）的任务上进行后训练。具体来说，给定对于问题x∼Dx\\sim D的尝试证明y∼πθ\(⋅∣x\)y\\sim\\pi\_\{\\theta\}\(\\cdot\\mid x\)，我们将教师定义为 πμ,y′\(⋅∣x\)=πμ\(⋅∣x,F\(y\)\)，\\pi^\{\\prime\}\_\{\\mu,y\}\(\\cdot\\mid x\)\\;=\\;\\pi\_\{\\mu\}\(\\cdot\\mid x,\\,F\(y\)\)，其中FF是一个函数，它接收尝试回答yy并返回一个文本反馈信号（特权信息）。为了与先前工作一致，我们将πμ,y′\\pi^\{\\prime\}\_\{\\mu,y\}称为教师模型，尽管更准确的描述是增强的学生。在我们的设置中，反馈FF是一个分析尝试yy的LLM。由于反馈可能来自更强的模型，我们使用术语**反馈蒸馏**。反馈模型也可能是π\\pi的冻结副本，我们有时称之为自反馈蒸馏。关于其他反馈来源的讨论请参考第2节（https://arxiv.org/html/2605.30861#S2）和5.1节（https://arxiv.org/html/2605.30861#S5.SS1）。我们在图1（https://arxiv.org/html/2605.30861#S1.F1）和附录D（https://arxiv.org/html/2605.30861#A4）中给出了反馈示例。 遵循Hübotteret al\.（2026（https://arxiv.org/html/2605.30861#bib.bib3）），我们通过指数移动平均（EMA）更新教师的权重：每五个梯度步骤，设置μ←αμ\+\(1−α\)θ\\mu\\leftarrow\\alpha\\,\\mu\+\(1\-\\alpha\)\\,\\theta，其中α∈\[0,1\]\\alpha\\in\[0,1\]是一个超参数。这个超参数对稳定性和性能有至关重要的影响（参见第5.2节（https://arxiv.org/html/2605.30861#S5.SS2））。 我们的损失是沿着从学生采样的轨迹上教师和学生分布之间的逐token Kullback-Leibler散度，即： Lθ=Ex∼D,y∼πθ\(⋅∣x\)\∑t=1\|y\|KL\(πμ,y′\(⋅∣x,y 你是一位专家级反馈导师。给定一个问题和一个学生的尝试，写出简洁、可操作的、能够从学生经验中提供通用反馈的建议。写出1到3条编号的关于错误、有用之处或无用的反馈。反馈必须自成一体，并对那些无法看到学生回答的人有用。反馈必须以命令的形式表达，例如“做X”或“不要做X”，不要提及学生。每条反馈必须在10到50个单词之间。目的不是评论学生的表现，而是为将来可能尝试同一问题的人提供有用的反馈。一般情况下不要使用“你”、“你的”或第二人称。它必须对不知道有学生存在的人有用。它必须鼓励使用工具。除了反馈本身，不要输出任何其他内容——不要介绍，直接给出第一条建议的“1\.”。如果回答在结尾处似乎被截断，可能是因为学生达到了token限制；在这种情况下，命令要更简洁。 ## 附录B 损失推导 由于梯度不通过yy的采样进行传播（停止梯度），Lθ\\mathcal\{L\}\_\{\\theta\}关于θ\\theta的梯度简化为仅对KL内部的πθ\\pi\_\{\\theta\}进行微分： ∇θLθ=−Ex∼D,y∼πθ\(⋅∣x\)\[∑t=1\|y\|∑a∈Vπμ,y′\(a∣x,y 你是一位专家级反馈导师。给定一个问题和一个学生的尝试，根据学生所做的写出简洁、可操作的建议。 - •提示（2）：\+ 格式约束 > 你是一位专家级反馈导师。给定一个问题和一个学生的尝试，根据学生所做的写出简洁、可操作的建议。写出1到3条编号的关于错误、有用之处或无用的反馈。每条不能太长——10到50个单词。除了反馈本身，不要输出任何其他内容，不要介绍，直接给出第一条建议的“1\.”。 - •提示（3）：\+ 自成一体反馈要求 > 你是一位专家级反馈导师。给定一个问题和一个学生的尝试，根据学生所做的写出简洁、可操作的建议。写出1到3条编号的关于错误、有用之处或无用的反馈。每条不能太长——10到50个单词。除了反馈本身，不要输出任何其他内容，不要介绍，直接给出第一条建议的“1\.”。反馈必须自成一体，并对那些无法看到学生回答的人有用。一般情况下不要使用“你”、“你的”或第二人称——它必须对不知道有学生存在的人有用。反馈必须以命令的形式表达，例如“做x”或“不要做x”，不要提及学生。目的不是评论学生的表现，而是为将来可能尝试同一问题的人提供有用的指导。 - •提示（4）：\+ 工具使用与截断指导 > 你是一位专家级反馈导师。给定一个问题和一个学生的尝试，写出简洁、可操作的、能够从学生经验中提供通用反馈的建议。写出1到3条编号的关于错误、有用之处或无用的反馈。反馈必须自成一体，并对那些无法看到学生回答的人有用。反馈必须以命令的形式表达，例如“做X”或“不要做X”，不要提及学生。每条反馈必须在10到50个单词之间。目的不是评论学生的表现，而是为将来可能尝试同一问题的人提供有用的反馈。一般情况下不要使用“你”、“你的”或第二人称。它必须对不知道有学生存在的人有用。它必须鼓励使用工具。除了反馈本身，不要输出任何其他内容。