| title | Distilling LLM Feedback for Lean Theorem Proving |
|---|---|
| authors | Gaetan Narozniak, Gérard Biau, Rémi Munos, Ahmad Rammal, Pierre Marion |
| date | 2026-05-29 |
| venue | arXiv (preprint, not peer reviewed) |
| id | arXiv:2605.30861 |
| affiliation | Meta Research |
| upvotes | 3 (Hugging Face Daily Papers, 2026-11-01) |
| links | abs pdf hf |
| abstract | Post-training for reasoning models typically combines supervised fine-tuning with reinforcement learning from verifiable rewards, most commonly with GRPO. However, this algorithm suffers from sparse rewards, limited exploration, and mode collapse. Building upon recent works on self-distillation, we propose Feedback Distillation, a training method where the model is trained to match, at the token level, its own distribution conditioned on privileged feedback produced by a language model. Feedback Distillation offers token-level supervision and can inject external knowledge. Evaluating our method for Lean4 theorem-proving, we find that Feedback Distillation maintains greater diversity in generated trajectories than GRPO, yielding higher policy entropy and better pass@k scaling. The two methods are complementary: initializing GRPO from a Feedback Distillation checkpoint outperforms either method alone. All in all, our results suggest a promising avenue to improve post-training for complex reasoning. |
cite
@misc{narozniak2026distilling,
title={Distilling LLM Feedback for Lean Theorem Proving},
author={Gaetan Narozniak and Gérard Biau and Rémi Munos and Ahmad Rammal and Pierre Marion},
year={2026},
eprint={2605.30861},
archivePrefix={arXiv},
url={https://arxiv.org/abs/2605.30861}
}