Distilling LLM Feedback for Lean Theorem Proving.

arXiv:2605.30861v2 Announce Type: replace 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,