**蒸馏大模型反馈：提升Lean定理证明后训练的新方法**

_Distilling LLM Feedback for Lean Theorem Proving_

> 本文提出反馈蒸馏方法，通过让模型在词元级别匹配语言模型特权分布，解决GRPO奖励稀疏与探索不足的问题。在Lean4定理证明中，该方法比GRPO生成更多样化轨迹，策略熵更高，pass@k扩展性更优。与GRPO互补，使用反馈蒸馏初始化GRPO可进一步提升性能，为复杂推理后训练提供新思路。

**来源信息**
- **来源**：HuggingFace Daily Papers（社区热门论文）
- **分类**：论文
- **发布时间**：2026-06-11 08:00（北京时间）
- **原文**：[打开原文](https://huggingface.co/papers/2605.30861)