Meta与Inria联手：教练式学习突破AI数学证明强化学习瓶颈

2026-06-18阅读 0热度 0

一、强化学习瓶颈：为何稀疏胜负反馈不足

教AI完成数学证明，难度超乎表面认知。人类需要从庞大引理库中筛选工具，在多个推理路径中判断。对AI而言，Lean 4的Mathlib核心库包含超过30万条声明，棋手每一步都要从中选择合适走法。

当前主流后训练方法结合监督微调（SFT）与强化学习中的GRPO算法。SFT模拟棋手学习名家棋局，GRPO让模型同时尝试多种走法，根据最终胜负优化策略。但研究团队指出三大问题。

首先，反馈稀疏。GRPO同时生成多个答案并对比胜负，但若所有答案均错误，则无法提供有效学习信号，模型难以定位错误。

其次，策略固化。近期研究表明，GRPO实际上会强化模型初始阶段的少数熟练策略，限制了探索新路径的能力。面对Mathlib中庞大引理库，这种固化导致无法灵活调用不同工具。

第三，模式坍塌。GRPO训练深入后，AI生成答案多样性下降，形成固定套路，对熟悉题型表现尚可，但面对需要新思维的局面时无力应对。

监督微调阶段还面临灾难性遗忘风险：训练数据标注成本高，且模型学习新样本时可能覆盖旧知识，如同棋手专攻特定开局后打乱其他开局感知。

二、反馈蒸馏：逐步骤指导与细粒度优化机制

反馈蒸馏建立在“自蒸馏”技术之上：模型同时扮演学生与老师，老师获取学生无法访问的额外信息，学生通过模仿成长。

具体流程：学生模型尝试证明数学题，生成过程后提交至反馈模型（主要实验使用Claude Opus 4.6），后者分析并给出1-3条操作建议，如“在Lean证明中使用Real.pi而非unicode符号π”。将建议附加于问题后，老师模型基于更完整信息生成答案，学生则模仿老师在此上下文中的输出。

核心设计在于损失函数：非简单判断答案对错，而是逐词计算学生与老师概率分布的KL散度。研究展示了具体案例：学生以56.1%概率输出unicode“π”，老师基于“使用Real.pi”的建议以98.1%概率输出“Real”。通过逐词比对，学生被精确引导至正确写法。

为降低计算成本，只关注老师概率最高的前25个词。同时，采用指数移动平均（EMA）更新老师权重，每隔五次梯度更新，按α=0.9将老师参数向学生靠拢，确保老师不会滞后于学生进步。

三、实验设计：Lean 4环境与多维度评估

实验配置：基于Qwen3-8B与Qwen3.5-9B，初始Lean 4能力极低（准确率2%和11%），确保进步来自学习。从LeanWorkbook抽取1万道有已知证明的数学陈述作为训练数据，评估集包括256道同数据集测试题和244道MiniF2F竞赛级数学题。

模型配备三个接口：lean_write_file写入代码，lean_check_file编译并返回错误或成功信息，rg_in_mathlib在Mathlib中搜索引理。实验验证这些工具能显著提升两种训练方法的表现。

反馈模型接收待证明陈述、完整尝试过程及编译器输出，要求输出1-3条简洁操作建议，长度10-50词，格式为“请做X”或“不要做X”。比较对象包括纯GRPO、纯反馈蒸馏，以及反馈蒸馏后切换GRPO的组合方法。

四、实验结果：反馈蒸馏+GRPO组合提升性能与策略熵

反馈蒸馏训练200、300或400步后切换GRPO，最终表现均超越纯GRPO。以Qwen3.5-9B为例，LeanWorkbook测试集上，纯GRPO pass@1约59%，而组合方法达到75%。反馈蒸馏提供了更扎实的基本功，使后续自我对弈在更高起点运作。

关键发现：反馈蒸馏全程保持更高策略熵，即AI面对同一局面时应对策略更多样。GRPO熵值持续下降，印证模式坍塌；反馈蒸馏则维持较高熵值，保留探索能力。

这项多样性优势在pass@k指标上体现：当pass@1相近时，反馈蒸馏在k=2、4、8、16时的表现均优于GRPO，差距随k扩大。此外，反馈蒸馏发现新Mathlib引理的速度更快且更持久，说明教练建议促使模型尝试新路径。

训练稳定性方面，GRPO和组合方法均存在后期准确率断崖式下降问题。研究通过学习率调整实验确认此问题非设置所致。Qwen3-8B训练稳定性优于Qwen3.5-9B，但组合方法峰值性能始终高于纯GRPO。

样本效率上，反馈蒸馏在训练早期更高效。需注意GRPO每批次处理数据量（640）是反馈蒸馏（128）的五倍。

五、反馈来源对比：批评式建议优于地面真值

研究比较三种反馈来源：Claude自然语言建议、地面真值反馈（直接提供正确答案证明）、Lean编译器输出（原始错误信息）。结果显示，Claude建议与地面真值均优于编译器输出。

有趣的是，Claude反馈比地面真值能保持更高策略熵。原因在于地面真值提供固定正确答案，老师以高确定性复现，学生被引导至单一路径；而Claude建议仅指出方向，老师仍需自行探索，保留更多生成多样性。

论文测试了“自反馈蒸馏”，即反馈来自被训练模型自身的冻结副本。自反馈蒸馏+GRPO仍优于纯GRPO，表明自我批评式学习也能提取有效信号，但峰值性能低于使用Claude版本。

六、EMA超参数配置：平衡学习速度与稳定性

EMA超参数α控制老师更新激进程度：α越接近0，更新越激进；α越接近1，更新越保守；α=1时老师完全冻结。若老师不更新，可能误判学生已掌握的知识，如学生正确使用Real.pi时仍给予低概率。

消融实验显示：α=0激进更新使早期训练快速推进但后期不稳定；α=1完全冻结学习缓慢。综合考虑，α=0.9提供最佳速度与稳定性平衡。但长期训练仍存在不稳定现象，留待后续解决。

七、内化验证：反馈是否转化为模型参数

研究设计实验验证反馈被内化，而非依赖Claude推理。使用固定字符串反馈（“请思考后再作答”或“请简洁作答”）并冻结老师。结果显示，接受“Think”反馈的学生平均回复长度增加，接受“Be concise”的则减少，且学生与老师KL散度收敛至接近零。这表明学生已学会将反馈行为编码入参数，训练结束后即使移除反馈，模型仍表现出相应倾向。

此外，地面真值反馈显著减少“wait”“hmm”“perhaps”等认知不确定性词语，导致模型过度自信；而Claude批评式建议和自反馈蒸馏未造成同样程度的减少，模型保留丰富思考过程表达。

使用批评式反馈训练的模型，平均回复长度远长于使用地面真值版本，与保持多样性和探索能力的总体结论一致。

八、提示词设计：结构化程度影响学习动态

研究测试四种不同结构化程度的反馈提示词，从简单“给一些建议”到包含格式要求、自包含性、工具使用鼓励的完整版本。结果显示，结构化程度越高，早期学习速度略慢，但训练更稳定、最终性能更优。正式实验使用Prompt 4。

宏观来看，反馈蒸馏可视为在线知识蒸馏变体：反馈模型比学生更强时，通过批评建议传递隐含知识，而非直接提供答案。实践中，因知识通过自然语言传递，无需教练模型与学生部署于同一系统或共享词表。

核心而言，训练AI解决全局失败的高难度问题时，仅靠“对/错”反馈远不足够。需要精细反馈、针对性建议，并保持探索的多样性与好奇心。反馈蒸馏通过引入语言模型教练与逐词学习信号，在不牺牲多样性的前提下实现有效学习。

当前局限包括：在更大规模SFT+GRPO流水线前尚未达到顶尖水平；训练稳定性问题待解决；提示词设计对性能影响显著，需人工调试。对普通读者而言，这印证了精准反馈优于笼统判断的人类学习原则。有兴趣者可通过arXiv:2605.30861查阅完整论文。

Q&A

Q1：反馈蒸馏与GRPO在优化信号上有何差异？

A： GRPO基于整个答案的对错结果提供奖励，当所有答案均错误时无法提供有效信号。反馈蒸馏通过语言模型生成具体建议，在逐词级别让学生模型学习“看到建议后”的老师行为，提供细粒度学习信号，即使尝试失败也能引导改进。

Q2：反馈蒸馏训练后的模型在推理阶段仍需Claude参与吗？

A：不需要。反馈内化于参数调整中，模型已学会在无外部反馈时表现更佳，如同棋手接受指导后独立对弈。

Q3：反馈蒸馏如何实现更高多样性的输出？

A：批评式建议不直接提供答案，仅指出方向，老师模型需自行探索，保留多种应对路径。而地面真值反馈导致单一路径，GRPO则通过奖励信号不断强化高分结果，导致策略收窄。