# Distilling LLM Feedback for Lean Theorem Proving

arXiv: https://arxiv.org/abs/2605.30861 · HTML: https://mlsanity.com/paper/2605.30861/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 21 of its 35 references that are in the map.
- First posted on arXiv 29 May 2026.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)
- Knowledge distillation / [On-policy and self-distillation for LLMs](https://mlsanity.com/distill/on-policy-and-self-distillation-for-llms/)

## Builds on (most cited first, 21 of 21)

- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [Momentum Contrast for Unsupervised Visual Representation Learning](https://mlsanity.com/paper/1911.05722/) (2019)
- [Bootstrap your own latent: A new approach to self-supervised Learning](https://mlsanity.com/paper/2006.07733/) (2020)
- [Let's Verify Step by Step](https://mlsanity.com/paper/2305.20050/) (2023)
- [Tree of Thoughts: Deliberate Problem Solving with Large Language Models](https://mlsanity.com/paper/2305.10601/) (2023)
- [GPQA: A Graduate-Level Google-Proof Q&A Benchmark](https://mlsanity.com/paper/2311.12022/) (2023)
- [Code Llama: Open Foundation Models for Code](https://mlsanity.com/paper/2308.12950/) (2023)
- [HybridFlow: A Flexible and Efficient RLHF Framework](https://mlsanity.com/paper/2409.19256/) (2024)
- [Competition-Level Code Generation with AlphaCode](https://mlsanity.com/paper/2203.07814/) (2022)
- [Self-Supervised Learning from Images with a Joint-Embedding Predictive Architecture](https://mlsanity.com/paper/2301.08243/) (2023)
- [Does Reinforcement Learning Really Incentivize Reasoning Capacity in LLMs Beyond the Base Model?](https://mlsanity.com/paper/2504.13837/) (2025)
- [On-Policy Distillation of Language Models: Learning from Self-Generated Mistakes](https://mlsanity.com/paper/2306.13649/) (2023)
- [Graph of Thoughts: Solving Elaborate Problems with Large Language Models](https://mlsanity.com/paper/2308.09687/) (2023)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [LLM Post-Training: A Deep Dive into Reasoning Large Language Models](https://mlsanity.com/paper/2502.21321/) (2025)
- [Why Does Self-Distillation (Sometimes) Degrade the Reasoning Capability of LLMs?](https://mlsanity.com/paper/2603.24472/) (2026)
- [The Invisible Leash: Why RLVR May or May Not Escape Its Origin](https://mlsanity.com/paper/2507.14843/) (2025)
- [Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics](https://mlsanity.com/paper/2601.14027/) (2026)
- [Asymmetric REINFORCE for off-Policy Reinforcement Learning: Balancing positive and negative rewards](https://mlsanity.com/paper/2506.20520/) (2025)
- [LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics](https://mlsanity.com/paper/2602.24173/) (2026)
- [Understanding Reasoning in LLMs through Strategic Information Allocation under Uncertainty](https://mlsanity.com/paper/2603.15500/) (2026)

## Built on by (most cited first, 1 of 1)

- [Train Ahead, Distill Back: Bootstrapping On-Policy Self-Distillation for Large Language Models](https://mlsanity.com/paper/2609.37132/) (2026)

## Abstract (arXiv)

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.