arXiv Artificial Intelligence· Gaetan Narozniak, G\'erard Biau, R\'emi Munos, Ahmad Rammal, Pierre Marion·· 3 小时前AI 评分31
用 LLM 反馈蒸馏训练 Lean 定理证明模型
Distilling LLM Feedback for Lean Theorem Proving
AI 导读
研究者提出 Feedback Distillation 训练方法，让模型在 token 级别匹配自身在语言模型特权反馈条件下的分布，用于 Lean4 定理证明。相比 GRPO，该方法生成的轨迹多样性更高、策略熵更大、pass@k 扩展性更好；以 Feedback Distillation 检查点初始化 GRPO 后，效果优于两种方法单独使用。
来源：arXiv Artificial Intelligence · arxiv.org