Meta与Inria联手：AI数学证明训练迎来"教练式学习"新范式，探索突破强化学习瓶颈的可能路径

这项由Meta人工智能研究院（FAIR at Meta）、法国国家信息与自动化研究所（Inria）、索邦大学、法国大学研究院（Institut universitaire de France）以及巴黎桥梁工程学院（CERMICS Ecole des Ponts ParisTech）联合开展的研究，于2026年5月29日以预印本形式发布，编号为arXiv:2605.30861v1，感兴趣的读者可通过该编号查阅完整论文原文。研究的核心是提出一种名为"反馈蒸馏"（Feedback Distillation）的训练方法，专门用于提升大型语言模型在形式化数学证明领域的能力，尤其针对Lean 4这一数学证明辅助工具的应用场景。

在正式进入研究细节之前，有必要先建立一个贯穿全文的理解框架。将AI学习数学证明的过程比作培训一位棋手，是一个颇为贴切的类比。传统的训练方式（也就是本文要挑战的方法）就像是让棋手自己下棋，然后告诉他"你赢了"或"你输了"，却不告诉他到底是哪一步走错了。而本文提出的新方法，更像是为棋手配备了一位有经验的教练，这位教练会在棋手下完每一局棋后，仔细分析棋局，针对具体失误给出精准建议——"这里应该走马，不应该走炮"。整篇文章，都可以从这个"自我训练的棋手"与"配备了教练的棋手"之间的对比来理解。

一、当前主流训练方法的困境：为什么棋手光靠"赢了/输了"的反馈还不够

教AI学会数学证明，是一件比看起来难得多的事情。人类数学家在证明一个定理时，需要从浩如烟海的引理库中选取合适的工具，需要在多个可能的推理路径中做出判断，稍有偏差就会功亏一篑。对于AI来说，这种挑战更为严峻——以Lean 4为例，它的核心数学库Mathlib拥有超过30万条数学声明，相当于一个规模庞大的棋谱库，棋手每次落子都要从中选取恰当的走法。

目前最主流的AI后训练方法，是将监督微调（SFT）与强化学习中的GRPO算法结合使用。简单来说，监督微调的过程就像给棋手展示大量名家棋局，让他模仿学习；而GRPO则是让棋手同时尝试多种走法，根据最终胜负来判断哪种策略更好。这套"看名家棋局+自我对弈"的组合拳，在过去取得了不少成果，但研究团队发现它存在三个根本性的问题。

第一个问题是"稀疏反馈"。GRPO的工作原理是让AI对同一道题同时生成多个答案，然后对比这些答案的正确与否来决定如何调整。但当题目很难，所有答案都是错的时候——就像棋手每一局都输了——这套方法完全无法给出任何有效的学习信号。棋手不知道自己哪里出了问题，只能原地踏步。

第二个问题是"探索不足"。近期研究发现，GRPO并不像人们原来以为的那样能让AI探索新的解题路径。相反，它倾向于强化AI在训练开始前就已经掌握的少数几种策略，让AI的思维越来越收窄，越来越依赖那几招"熟练棋路"，而不是学会面对新局面时的灵活应变。这对于需要从Mathlib中调用大量不同引理的形式化数学来说，是一个严重缺陷。

第三个问题是"模式崩溃"。这是一个更为微妙的现象：随着GRPO训练的深入，AI生成答案的多样性会逐渐下降，就像一个棋手的棋风越来越单一，形成了固定的"套路"。这样的棋手在应付他熟悉类型的题目时表现不错，但一旦遇到需要新思路的局面，就会束手无策。

此外，监督微调阶段还有另一个隐患：用现成的"名家棋局"来训练AI，不但制作这些棋局的成本高昂，而且AI在学习这些棋局时，可能会"忘记"之前已经掌握的其他知识，就好比棋手专门练习了某一类开局，结果把其他开局的感觉给打乱了。这种现象在机器学习中被称为"灾难性遗忘"。

二、反馈蒸馏的核心思想：为棋手配备一位实时教练

研究团队提出的"反馈蒸馏"方法，建立在"自蒸馏"这一近期出现的技术思路之上。自蒸馏的基本想法是：让模型同时扮演"学生"和"老师"两个角色，老师能看到学生看不到的额外信息，然后学生通过学习模仿老师的行为来成长。

反馈蒸馏的具体工作流程是这样的：首先，作为"学生"的AI模型尝试证明一道数学题，生成一个证明过程；接下来，这个证明过程（包括对错情况）被交给一个"反馈模型"——在主要实验中，这个反馈模型是Claude Opus 4.6，一个由Anthropic公司开发的强大语言模型——后者对这次尝试进行分析，给出1到3条具体的、可操作的改进建议，例如"在Lean证明中使用Real.pi而不是unicode符号π"或者"遇到绝对值不等式时，先用rcases le_or_lt拆分情况"；然后，将这条具体建议附加在证明题目后面，形成"老师"看到的完整输入，让老师模型根据这份更丰富的信息生成它认为更好的答案；最后，学生被训练去模仿老师的这种"加了建议之后"的表现。

这里有一个非常精妙的设计：训练的损失函数不是简单地告诉学生"整个答案对了还是错了"，而是在每一个词、每一个符号的层面上，让学生学习老师的概率分布。论文中给出了一个直观的例子（图1）：学生在证明一道关于π的题目时，以56.1%的概率写出了unicode符号"π"；而老师在看到"不要用unicode符号π，应该用Real.pi"这条反馈之后，以98.1%的概率在相同位置写出了"Real"（即Real.pi的开头）。通过这种逐词比对和调整，学生被精确地引导向更好的写法，而不是笼统地被告知"这个证明错了"。

这种逐词的、细粒度的学习信号，正是反馈蒸馏相比GRPO的核心优势——就像教练不仅告诉棋手"你这局输了"，而是具体指出"你第17步那个炮的落点选错了，应该走到这里，因为可以牵制对方的车"。

在技术实现层面，训练损失函数使用的是KL散度（一种衡量两个概率分布差异的数学工具），逐词衡量老师分布与学生分布之间的差距，并驱动学生向老师靠拢。为了降低计算成本，实际操作中只关注老师认为概率最高的前25个词，而非全部词汇表（通常有数万词）。此外，为了让老师模型不至于在训练过程中越来越落后于学生（毕竟学生在不断进步，而一个固定不变的老师会越来越不适合当前的学生水平），研究团队采用了"指数移动平均"（EMA）的方式来更新老师的权重：每隔五次梯度更新，就将老师的参数向学生靠拢一小步，用公式表示就是 μ ← α·μ + (1-α)·θ，其中α是一个控制靠拢速度的超参数。

三、实验设计：在数学证明的"竞技场"里进行公平比试

为了验证反馈蒸馏的有效性，研究团队搭建了一套精心设计的实验环境。实验选择Lean 4形式化数学证明系统作为测试场，原因是多方面的：使用的基础模型（Qwen3-8B和Qwen3.5-9B）在训练开始时对Lean 4几乎一无所知（分别只有2%和11%的初始准确率），这意味着任何有意义的进步都来自真正学到了新东西，而非依赖已有知识；Lean 4的搜索空间极为庞大，需要从Mathlib的30万余条声明中选取合适工具；Lean编译器能给出确定性的正确/错误判断，提供了可靠的验证信号。

训练数据来自LeanWorkbook数据集，从中抽取了1万道有已知证明的数学陈述用于训练。评估则在两个独立测试集上进行：一个是LeanWorkbook的256道测试题，另一个是MiniF2F的244道竞赛级数学题（如数学奥林匹克题目的形式化版本）。

为了让模型能够更灵活地与Lean环境交互——就像棋手在练棋时能随时查阅棋谱、试走棋步一样——研究团队为模型配备了三个工具：lean_write_file用于将代码写入文件，lean_check_file用于编译文件并返回编译器的错误或成功信息，rg_in_mathlib用于用正则表达式在Mathlib库中搜索相关引理。实验验证了这些工具的使用能显著提升两种训练方法的表现。

反馈模型Claude Opus 4.6收到的信息包括：待证明的数学陈述、模型的完整尝试过程（包括所有工具调用记录和工具返回结果）、最终Lean编译器的输出。它被要求给出1到3条简洁、可操作的建议，以"请做X"或"不要做X"的命令式语气呈现，每条建议在10到50词之间，且要在不看学生答案的情况下也能独立理解。

实验的比较对象包括：纯GRPO训练、纯反馈蒸馏训练，以及在反馈蒸馏训练到一定阶段后切换为GRPO继续训练的"组合方法"。主要结果以Qwen3.5-9B为基础模型呈现，Qwen3-8B的结果作为补充验证。

四、实验结果：组合方法力压各方，多样性是关键优势

整体实验结果如图2所示，展示了各方法在训练准确率、LeanWorkbook测试准确率、MiniF2F测试准确率以及策略熵（一种衡量AI生成答案多样性的指标）四个维度上随训练步骤的变化曲线。核心结论可以从几个维度来理解。

关于"反馈蒸馏+GRPO"组合的优势，结果相当清晰：在反馈蒸馏训练200步、300步或400步后切换为GRPO，最终性能均明显超过从头用GRPO训练的结果。具体数字上，对Qwen3.5-9B而言，在LeanWorkbook测试集上，纯GRPO的pass@1（即每道题只给一次机会的准确率）约为59%，而反馈蒸馏+GRPO达到了75%。这意味着，反馈蒸馏阶段给了棋手一个更好的"基本功"，使得后续的自我对弈训练能够在更高的起点上发挥作用。

关于多样性和熵的差异，这一点是论文最有特色的发现之一。在整个训练过程中，反馈蒸馏始终保持比GRPO更高的策略熵。所谓策略熵，可以理解为棋手走法的丰富程度——熵高意味着棋手面对同一局面时有更多不同的应对策略，熵低意味着棋手越来越依赖固定套路。GRPO在训练过程中熵值持续下降，印证了前文提到的"模式崩溃"问题；而反馈蒸馏的熵值维持在较高水平，说明AI在学习的同时保留了更强的探索能力。

这种多样性的保持，在pass@k指标上有直接体现。pass@k是指给模型k次机会，只要有一次答对就算成功的准确率。如图3右侧所示，在两种方法pass@1相近的检查点上（即每次只给一次机会时表现差不多），反馈蒸馏在k=2、4、8、16时的表现都明显优于GRPO，而且差距随k的增大而扩大。这说明反馈蒸馏保持的更高熵不是"随机噪声"，而是真实的答案多样性——就像一个棋手真正掌握了多种下法，而不只是下法看起来多变但其实没什么章法。

关于新引理的发现速度，图3左侧展示了一个颇为直观的指标：在训练过程中，模型每步新用到的Mathlib引理数量。反馈蒸馏在这一指标上明显优于GRPO，新引理的发现速率更快也更持久。这就像是教练的建议让棋手开始尝试之前从未用过的开局套路，而纯靠自我对弈的棋手则越来越局限于已知的几种走法。

关于训练稳定性，研究团队也坦诚地指出了一个问题：GRPO以及反馈蒸馏+GRPO的组合，都存在训练不稳定的现象，在训练后期准确率会突然崩溃式下降（从图2的曲线中可以明显看到这种"过山车"形态）。研究团队专门做了学习率调整实验来排除这是单纯由学习率设置引起的可能性，确认这是GRPO本身的固有问题。值得一提的是，在Qwen3-8B模型上，训练稳定性明显好于Qwen3.5-9B，说明这一问题与模型本身有关。但无论如何，"反馈蒸馏+GRPO"的峰值性能始终高于纯GRPO，这一结论在两个模型上都成立。

关于样本效率，反馈蒸馏在训练早期明显比GRPO更高效——用同样数量的数据，反馈蒸馏能取得更快的进步。当然，需要注意的是GRPO每批次实际处理的数据量（有效批量大小640）是反馈蒸馏（128）的五倍，因为GRPO对每道题要同时生成5个答案进行比较。

五、不同反馈来源的对比：教练的质量很重要

反馈蒸馏中的"反馈"来源是一个关键设计选择。论文中对三种不同的反馈来源进行了系统比较，结果如图4所示。

第一种是Claude提供的自然语言建议（主要实验中使用的方式）。第二种是"地面真值反馈"，即直接把正确答案的证明以"Example of a correct solution:{solution}"的格式提供给老师——这相当于教练不给建议，直接把正确棋谱摆给棋手看。第三种是"Lean编译器输出"，即把Lean编译器返回的原始错误信息提供给老师，成功时则提供找到的答案——这相当于给棋手看裁判的判罚单。

实验结果显示，Claude建议和地面真值反馈都明显优于原始Lean编译器输出。这在直觉上是可以理解的：编译器的错误信息通常很底层，类似于"第42行语法错误"，而Claude的建议是高层的策略性指导，更容易被模型吸收；地面真值则直接提供了正确答案，信息量最为丰富。

一个有趣的观察是，Claude反馈相比地面真值反馈，能让模型保持更高的策略熵。研究团队认为这是因为：地面真值直接给出了正确答案，老师模型在看到答案后会以很高的确定性复现这个答案，学生也会被引导到这一种固定路径；而Claude的建议只是指出方向和问题，并不直接给出答案，老师在此基础上还需要自己探索，因此保留了更多的生成多样性，就像教练说"你应该控制中路"，棋手仍然有很多种具体走法来实现这一目标。

此外，论文还特别测试了一种"自反馈蒸馏"设置：反馈不来自更强大的Claude，而是来自被训练模型自身的一个冻结副本，即用相同的模型来评价自己的证明尝试。结果显示，自反馈蒸馏+GRPO的组合仍然比纯GRPO表现更好，说明即便没有外部更强模型的参与，这种"自我批评式学习"也能提取出GRPO找不到的有效学习信号。不过，自反馈蒸馏的峰值性能仍低于使用Claude反馈的版本，这表明更高质量的外部反馈确实能带来额外增益，同时也提示改进反馈内容的设计是进一步提升的方向。

六、EMA超参数的作用：教练要多快更新自己的认知

EMA超参数α的选择，是这套方法中一个微妙但至关重要的细节。α越接近0，表示老师的参数每次都会大幅向学生靠拢（更新激进）；α越接近1，表示老师几乎不更新（更新保守）；α=1时，老师完全冻结，不受学生的影响。

为什么老师需要随着训练动态更新，而不能保持固定呢？原因在于：随着训练进行，学生会逐渐掌握越来越多的新知识（比如正确使用Real.pi而非π）。如果老师是固定的，它不知道学生已经掌握了这些知识，当学生正确写出Real.pi时，固定的老师可能仍然会给出较低的概率，反而惩罚了正确的行为。就像一个教练如果不跟踪棋手的成长，还在批评棋手"你应该学会X战术"——而棋手其实早已掌握了X战术——这种批评就是错误的负反馈。EMA更新让老师能够逐步跟上学生的进步，保持"批评的准确性"。

论文中对α从0到1进行了全面的消融实验（图6）。结果显示，α=0（最激进的更新）能让训练在早期快速推进，但后期会陷入不稳定；α=1（完全冻结）则避免了不稳定，但学习速度很慢；综合考量，α=0.9提供了最佳的速度与稳定性平衡，成为所有主要实验的设置。然而，即便是α=0.9，长期训练仍然会出现不稳定现象，研究团队认为这是未来需要解决的重要问题。

七、定性分析：反馈真的被"内化"了吗？

一个合理的疑问是：经过这种训练，模型是真的学会了Claude建议的技巧，还是只是在推理时依赖Claude的帮助？研究团队设计了一个有趣的实验来验证"反馈被内化"这一核心声明。

在这个实验中，反馈不再是针对具体题目的具体建议，而是一个在整个训练过程中固定不变的字符串——要么是"请思考后再作答，验证答案的正确性"（Think），要么是"请简洁作答"（Be concise）。老师是完全冻结的（不更新权重）。结果如图7所示：接受"Think"反馈训练的学生，平均回复长度逐渐增加；接受"Be concise"反馈训练的学生，平均回复长度则逐渐减少。与此同时，学生与老师之间的KL散度（分布差异度量）收敛到接近零。这说明学生确实逐渐学会了模仿老师在有反馈时的行为方式，并且把这种行为"写入了自己的参数"——训练结束后，即使不再给模型看反馈，它也会表现得像是一直在接受这条反馈一样。

另一个定性发现涉及"认知不确定性的表达"。近期一些研究发现，当自蒸馏方法使用地面真值（完整正确答案）作为反馈时，模型会减少使用"wait（等一下）""hmm（嗯）""perhaps（也许）"等表达不确定性的词语，模型变得过于自信，在遇到新情况时表现变差，这种现象被称为"认知言语化的抑制"。研究团队在图13中追踪了不同反馈来源下这些不确定性词语的出现频率，发现地面真值反馈确实导致了这些词的显著减少；但Claude的批评式建议和自反馈蒸馏，都没有造成同样程度的减少——模型保留了更丰富的思考过程表达。这与前面提到的"更高策略熵"是一脉相承的：批评式建议让老师的生成更有探索性，学生模仿老师时也保留了这种探索性。

与此相对应，图14还显示，使用批评式反馈（Claude或自反馈）训练的模型，平均回复长度远长于使用地面真值反馈的模型，整个训练过程中保持在较高水平。这与"保持多样性、保持探索能力"的总体结论完全一致。

八、反馈提示词的设计：措辞影响着学习效果

研究团队还专门测试了四种不同结构化程度的反馈提示词（Prompt 1到Prompt 4），从最简单的"给一些建议"到包含详细格式要求、自包含性要求、工具使用鼓励以及截断处理指导的完整提示词。结果如图12所示，提示词的结构化程度对训练动态有显著影响：结构化程度越高的提示词，早期学习速度略慢，但训练更加稳定，最终性能也更高。特别是Prompt 3和Prompt 4（要求反馈自包含、不依赖学生答案才能理解）表现最佳，这说明让反馈更加通用化、更具迁移性，有助于模型学到更泛化的知识，而不只是针对单个具体尝试的修补建议。正式实验中使用的是Prompt 4。

从更宏观的角度来看，反馈蒸馏可以被理解为一种"在线知识蒸馏"的变体：当反馈模型比学生更强时，它相当于在不直接提供答案的情况下，向学生传递强模型的隐含知识——就像教练不直接告诉棋手该下哪步，但通过批评和建议，把自己对棋局的深层理解慢慢渗透给棋手。这种方式还有一个实践上的额外好处：由于知识是通过自然语言反馈传递的，而非通过直接的概率分布匹配，使用这一方法时不需要把教练模型和学生模型部署在同一套系统中，也不需要两者共享相同的词表。

归根结底，这篇论文讲的是一件很实际的事：当你要训练AI去解决一些真的很难、一开始几乎全部失败的问题时，仅仅告诉AI"对了/错了"是远远不够的。需要更精细的反馈，需要针对每个具体错误的针对性建议，需要保持AI在探索中的多样性和好奇心。研究团队提出的反馈蒸馏方法，通过引入"语言模型教练"和逐词级别的学习信号，在不牺牲多样性的前提下实现了有效的学习。

当然，这套方法目前也有明显的局限：在规模更大的SFT+GRPO流水线面前，反馈蒸馏的结果还没有达到最顶尖的水平；训练稳定性是一个还未完全解决的挑战；反馈提示词的设计对性能影响显著，这意味着还有很多人工调试的空间。研究团队也明确指出，这些都是未来工作的重要方向。

对于普通读者来说，这项研究传递的一个启示是：AI的学习方式其实与人类有很多相似之处——精准的、有针对性的反馈，往往比笼统的对错判断更有效。而如何让AI在持续学习的过程中不失去探索的广度，是当前AI研究中一个既有理论价值、又有实际意义的核心问题。有兴趣深入了解这项研究的读者，可以通过arXiv:2605.30861查阅完整的论文原文。

Q&A

Q1：反馈蒸馏与GRPO有什么本质区别？

A：GRPO是对整个答案给出"对/错"的结果反馈，当所有答案都错时完全没有学习信号。反馈蒸馏则通过语言模型对每次尝试给出具体建议，然后在逐词级别让学生模型学习"看到建议之后"的老师行为，能给出更细粒度的学习信号，即便尝试失败也能从中学习。

Q2：反馈蒸馏训练出来的模型，推理时还需要Claude参与吗？

A：不需要。这正是"内化"的意义所在。训练结束后，Claude的建议已经通过参数调整被写入了学生模型本身，模型在推理时无需再调用Claude，就会自然地表现出吸收了这些建议后的行为，就像棋手经过教练指导后，上场对弈时不再需要教练在旁边提示。

Q3：反馈蒸馏为什么能保持更高的多样性？

A：因为Claude的批评式建议不直接给出答案，只指出方向和问题，老师模型在此基础上仍需自行探索，保留了多种可能的应对路径。相比之下，地面真值直接提供正确答案，老师会以高确定性复现它，学生也趋向单一路径。GRPO则通过奖励信号不断强化已有的高分路径，导致越来越收窄。