arXiv · AI· Gaetan Narozniak, G\'erard Biau, R\'emi Munos, Ahmad Rammal, Pierre Marion·· 12 小时前AI 评分38
基于 LLM 反馈蒸馏的 Lean4 定理证明训练方法
Distilling LLM Feedback for Lean Theorem Proving
AI 导读
研究人员提出 Feedback Distillation 方法，通过在 token 级别匹配 LLM 生成的特权反馈来训练模型，旨在解决 GRPO 在强化学习中面临的稀疏奖励与模式坍塌问题。
来源：arXiv · AI · arxiv.org