Distilling LLM Feedback for Lean Theorem Proving

2026/05/29 by Gaëtan Narozniak, Gaetan Narozniak, Gérard Biau +3 · 1 voice
Computer Science · #Distillation #Entropy (arrow of time) #Explainable Artificial Intelligence (XAI) #Initialization #Mode (computer interface) #Multimodal Machine Learning Applications #Reinforcement Learning in Robotics #Reinforcement learning #Verifiable secret sharing #cs.AI

paper · pdf · doi:10.48550/arxiv.2605.30861

openalex publication_date 2026/05/29 · arxiv published 2026/05/29 · arxiv updated 2026/05/29 · openalex created_date 2026/06/02 · openalex updated_date 2026/07/28

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.

Citations

• Why Does Self-Distillation (Sometimes) Degrade the Reasoning Capability of LLMs?
• LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics
• The Invisible Leash: Why RLVR May or May Not Escape Its Origin
• Asymmetric REINFORCE for off-Policy Reinforcement Learning: Balancing positive and negative rewards
• Does Reinforcement Learning Really Incentivize Reasoning Capacity in LLMs Beyond the Base Model?
• LLM Post-Training: A Deep Dive into Reasoning Large Language Models
• PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
• BioXP-0.5B: Explainable Medical-AI via RL-GRPO
• GPQA: A Graduate-Level Google-Proof Q&A Benchmark
• Code Llama: Open Foundation Models for Code
• Graph of Thoughts: Solving Elaborate Problems with Large Language Models
• On-Policy Distillation of Language Models: Learning from Self-Generated Mistakes
• Let's Verify Step by Step
• Tree of Thoughts: Deliberate Problem Solving with Large Language Models
• Self-Supervised Learning from Images with a Joint-Embedding Predictive Architecture
• Competition-Level Code Generation with AlphaCode
• Bootstrap your own latent: A new approach to self-supervised Learning
• Momentum Contrast for Unsupervised Visual Representation Learning
• Momentum Contrast for Unsupervised Visual Representation Learning

Discussions

• 🚨 New preprint: Distilling LLM Feedback for Lean Theorem Proving Paper: arxiv.org/abs/2605.30861. This research was led by Gaëtan Narozniak 🙏. [bsky, 0 points, 1 comments]

Related

• Learning from Language Feedback via Variational Policy Distillation
• Reinforcement Learning via Self-Distillation
• KDRL: Post-Training Reasoning LLMs via Unified Knowledge Distillation and Reinforcement Learning
• Self-Distilled Reasoner: On-Policy Self-Distillation for Large Language Models
• Post-Training Large Language Models via Reinforcement Learning from Self-Feedback