Distilling LLM Feedback for Lean Theorem Proving

• URL: http://arxiv.org/abs/2605.30861v1
• Date: Fri, 29 May 2026 05:35:00 GMT
• Title: Distilling LLM Feedback for Lean Theorem Proving
• Abstract summary: Post-training for reasoning models typically combines supervised fine-tuning with reinforcement learning from verifiable rewards.<n>This algorithm suffers from sparse rewards, limited exploration, and mode collapse.<n>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.
• Score: 20.86168010460303
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• 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.

Related papers

• Rethinking Reward Supervision: Rubric-Conditioned Self-Distillation [60.55792673956761]
  We propose textbfRubric-Conditioned Self-Distillation, a framework that incorporates rubrics as structured, fine-grained feedback for on-policy self-distillation.<n>We evaluate on a diverse suite of science reasoning benchmarks and results show that rubric-conditioned self-distillation effectively converts rubric-level criteria into token-level guidance.
  arXiv  Detail & Related papers  (2026-06-17T17:54:04Z)
• From Failure to Feedback: Group Revision Unlocks Hard Cases in Object-Level Grounding [35.008790179255136]
  We propose a group-revision optimisation paradigm that enhances learning on hard cases.<n>Inspired by reward shaping, we introduce a consolidation process that quantifies each candidate's improvement over the initial attempt.<n>Our method achieves consistent gains across referring and reasoning segmentation, REC, and counting benchmarks compared with prior GRPO-based models.
  arXiv  Detail & Related papers  (2026-05-15T13:41:41Z)
• Probing to Refine: Reinforcement Distillation of LLMs via Explanatory Inversion [84.20493238687187]
  We introduce a novel framework that moves beyond simple mimicry to instill a deeper conceptual understanding.<n>underlinetextitFirst, to address pattern memorization, Explanatory Inversion (EI) generates targeted explanatory probes''<n>underlinetextitSecond, to improve generalization, Explanatory GRPO (texttEXGRPO) uses a reinforcement learning algorithm with a novel Dialogue Structure Utility Bonus.
  arXiv  Detail & Related papers  (2026-02-26T23:01:46Z)
• Coupled Variational Reinforcement Learning for Language Model General Reasoning [83.82392089177841]
  We propose textitbCoupled bVari bReinforcement bLearning (CoVRL) to bridge variational inference and reinforcement learning.<n>CoVRL improves performance by 12.4% over the base model and achieves an additional 2.3% improvement over strong state-of-the-art verifier-free RL baselines.
  arXiv  Detail & Related papers  (2025-12-14T07:03:51Z)
• Can GRPO Help LLMs Transcend Their Pretraining Origin? [42.200901132315636]
  Group Relative Policy Optimization is a leading approach for enhancing the reasoning abilities of Large Language Models (LLMs)<n>Despite its wide adoption, GRPO's gains are often inconsistent.<n>This inconsistency raises a critical question: under what conditions does GRPO improve reasoning and generalize out-of-distribution (OOD)?<n>We first prove theoretically that GRPO is a conservative reweighting scheme, bounded by the base model's distribution and thus unable to discover completely novel solutions.
  arXiv  Detail & Related papers  (2025-10-14T00:37:52Z)
• Learning a Dense Reasoning Reward Model from Expert Demonstration via Inverse Reinforcement Learning [50.20267980386502]
  We learn a dense, token-level reward model for process supervision directly from expert demonstrations.<n>The learned reasoning reward serves two complementary roles: (i) it provides step-level feedback to optimise a reasoning policy during training; and (ii) it functions at inference as a critic to rerank sampled traces under fixed compute budgets.
  arXiv  Detail & Related papers  (2025-10-02T09:55:26Z)
• EDGE-GRPO: Entropy-Driven GRPO with Guided Error Correction for Advantage Diversity [7.818698554631196]
  Group Relative Policy Optimization (GRPO) algorithm relies on sparse reward rules, leading to the advantage collapse problem.<n>We propose the EDGE-GRPO algorithm, which adopts textbfEntropy-textbfDriven Advantage and textbfGuided textbfError Correction to effectively mitigate the problem of advantage collapse.
  arXiv  Detail & Related papers  (2025-07-29T14:23:58Z)
• ExPO: Unlocking Hard Reasoning with Self-Explanation-Guided Reinforcement Learning [12.83211408922535]
  Reinforcement learning-style post-training improves reasoning by optimizing model outputs based on reward or preference signals.<n> GRPO-style approaches implement this by using self-generated samples labeled by an outcome-based verifier.<n>We propose $textbfSelf-Explanation Policy Optimization (ExPO)$-a simple and modular framework that generates such samples by conditioning on the ground-truth answer.
  arXiv  Detail & Related papers  (2025-07-03T17:44:55Z)
• Intra-Trajectory Consistency for Reward Modeling [67.84522106537274]
  We develop an intra-trajectory consistency regularization to enforce that adjacent processes with higher next-token generation probability maintain more consistent rewards.<n>We show that the reward model trained with the proposed regularization induces better DPO-aligned policies and achieves better best-of-N (BON) inference-time verification results.
  arXiv  Detail & Related papers  (2025-06-10T12:59:14Z)
• A Minimalist Approach to LLM Reasoning: from Rejection Sampling to Reinforce [68.99924691391048]
  We revisit GRPO from a reinforce-like algorithm perspective and analyze its core components.<n>We find that a simple rejection sampling baseline, RAFT, yields competitive performance than GRPO and PPO.<n>Motivated by this insight, we propose Reinforce-Rej, a minimal extension of policy gradient that filters both entirely incorrect and entirely correct samples.
  arXiv  Detail & Related papers  (2025-04-15T16:15:02Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.