Distilling LLM Feedback for Lean Theorem Proving
Feedback Distillation is a training method that teaches a model to match its own output distribution based on privileged feedback from another language model. This technique improves reasoning in Lean theorem proving by maintaining greater trajectory diversity and higher policy entropy compared to standard methods like GRPO. It suggests that models can internalize self-reflective abilities for better complex reasoning.