Research map / Large language models / Reasoning and chain of thought

Distilling LLM Feedback for Lean Theorem Proving

NeurIPS 2026 · Large language models › Reasoning and chain of thought · approach: RL with verifiable rewards for reasoning · 0 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Proposes Feedback Distillation, a self-distillation method where a student is trained to match token-level distributions of an EMA teacher conditioned on LLM-generated feedback on its Lean proof attempts, showing higher entropy and better pass@k than GRPO and gains when used as GRPO initialization.

Problem

GRPO-based post-training for formal theorem proving suffers from sparse trajectory-level rewards, limited exploration, and mode collapse, reducing output diversity.

Approach

Train the student to match, token by token, the distribution of an EMA teacher that is conditioned on natural-language feedback (produced by a stronger LLM or a frozen copy of the model) about the student's own attempt and Lean compiler output, distilling the feedback into weights on-policy.

Key results

• On LeanWorkbook test, Qwen3.5-9B reaches 59% pass@1 with GRPO alone versus 75% with Feedback Distillation followed by GRPO.
• Feedback Distillation maintains significantly higher policy entropy than GRPO and scales better with pass@k at matched pass@1.
• Qwen3.5-9B base scores 11% on MiniF2F at initialization and Qwen3-8B scores 2% in the authors' setup.

Surprising findings

• Constant feedback such as 'Be concise' or 'Think carefully' is internalized, so the student behaves as if the feedback were in every prompt.
• Ground-truth solution feedback causes epistemic verbalization (e.g., 'wait', 'hmm') to drop sharply, whereas critique-style feedback preserves it.

Limitations

• Training instability with GRPO and GRPO over Feedback Distillation, and long-term instability even with large EMA coefficient.
• Results do not yet match state-of-the-art SFT+GRPO pipelines trained at scale.
• Self-feedback performs below Lean-output-informed feedback, and feedback prompt design has large effects on results.

Experimental setup

Datasets: LeanWorkbook MiniF2F

Benchmarks: LeanWorkbook test split (256 statements) MiniF2F test split (244 problems)

Metrics: pass@1 accuracy pass@k policy entropy number of distinct tactics and lemmas used

Baselines: GRPO Ground-truth solution feedback Lean compiler output feedback Self-Feedback Distillation

Builds on: GRPO self-distillation on-policy distillation verl

Closest papers by meaning

• Process-Verified Reinforcement Learning for Theorem Proving via Lean (ICLR 2026 · similarity 0.90)
• DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search (ICLR 2025 · similarity 0.88)
• Lean-STaR: Learning to Interleave Thinking and Proving (ICLR 2025 · similarity 0.87)
• Self-Distilled Reasoner: On-Policy Self-Distillation for Large Language Models (ICML 2026 · similarity 0.87)
• Learning from Language Feedback via Variational Policy Distillation (NeurIPS 2026 · similarity 0.87)
• GLoRe: When, Where, and How to Improve LLM Reasoning via Global and Local Refinements (ICML 2024 · similarity 0.87)