Distilling LLM Feedback for Lean Theorem Proving

# Distilling LLM Feedback for Lean Theorem Proving
Source: [https://arxiv.org/html/2605.30861](https://arxiv.org/html/2605.30861)
Gaëtan Narozniak FAIR at Meta, Inria gaetan@meta\.com &Gérard Biau Sorbonne Université, Institut universitaire de France &Rémi Munos FAIR at Meta Ahmad Rammal FAIR at Meta, CERMICS École des Ponts ParisTech &Pierre Marion Inria, ENS, PSL Research University pierre\.marion@inria\.fr

###### 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 Lean 4 theorem\-proving, we find that Feedback Distillation maintains greater diversity in generated trajectories than GRPO, yielding higher policy entropy and better pass@kkscaling\. 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\.

## 1Introduction

Recent advances in AI have demonstrated remarkable progress in complex reasoning tasks\(Liet al\.,[2022](https://arxiv.org/html/2605.30861#bib.bib40); Rozièreet al\.,[2023](https://arxiv.org/html/2605.30861#bib.bib41); Yaoet al\.,[2023](https://arxiv.org/html/2605.30861#bib.bib43); Bestaet al\.,[2024](https://arxiv.org/html/2605.30861#bib.bib44); Reinet al\.,[2024](https://arxiv.org/html/2605.30861#bib.bib42)\)\. Mathematical reasoning has emerged as a particularly valuable testbed for these approaches due to its challenging search spaces, clear correctness criteria, and rich problem structure ranging from formal theorem proving to informal problem\-solving\(Lightmanet al\.,[2023](https://arxiv.org/html/2605.30861#bib.bib38); Trinhet al\.,[2024](https://arxiv.org/html/2605.30861#bib.bib39); Hubertet al\.,[2025](https://arxiv.org/html/2605.30861#bib.bib31); Peyronnetet al\.,[2026](https://arxiv.org/html/2605.30861#bib.bib34)\)\. A fruitful strategy uses verifiable rewards, where deterministic verifiers \(e\.g\., Lean proof checkers\) evaluate model outputs\. In this setting, state\-of\-the\-art post\-training pipelines combine supervised fine\-tuning \(SFT\) on expert solutions \(coming either from human experts or from a stronger LLM\) with reinforcement learning \(RL\) to maximize the reward provided by the verifier\(Kumaret al\.,[2025](https://arxiv.org/html/2605.30861#bib.bib32)\)\. The RL algorithm is usually GRPO\(Shaoet al\.,[2024](https://arxiv.org/html/2605.30861#bib.bib33)\), an algorithm that samples multiple outputs per prompt and optimizes the policy by contrasting their rewards\.

However, this SFT\+GRPO paradigm has significant limitations\. First, the SFT phase is limited by the difficulty and cost of generating the fine\-tuning dataset\. Furthermore, because it trains on off\-policy demonstrations, it can cause catastrophic forgetting outside the narrow fine\-tuning distribution\(see, e\.g\., Ross and Bagnell,[2010](https://arxiv.org/html/2605.30861#bib.bib20); Agarwalet al\.,[2024](https://arxiv.org/html/2605.30861#bib.bib21); Shenfeldet al\.,[2026](https://arxiv.org/html/2605.30861#bib.bib2)\)\. Moreover, contrary to the popular belief that RL training leads to new reasoning capabilities, recent evidence suggests GRPO does not amplify the diversity of model answers nor favor exploration during training, but rather collapses onto modes with high reward already present before RL training\(Yueet al\.,[2025](https://arxiv.org/html/2605.30861#bib.bib1)\)\. This is particularly problematic in formal mathematics where exploration of large libraries of lemmas \(e\.g\., Lean’s Mathlib,The mathlib Community,[2020](https://arxiv.org/html/2605.30861#bib.bib7)\) is essential for success\. Finally, GRPO provides only trajectory\-level rewards, which offer no learning signal when all samples fail\.

These interconnected challenges motivate exploration of alternative training mechanisms\. A promising approach is the recently proposed self\-distillation algorithm\(Hübotteret al\.,[2026](https://arxiv.org/html/2605.30861#bib.bib3); Shenfeldet al\.,[2026](https://arxiv.org/html/2605.30861#bib.bib2); Zhaoet al\.,[2026](https://arxiv.org/html/2605.30861#bib.bib11)\), which trains the model to mimic its own outputs when conditioned on privileged information, effectively distilling the prompting strategy directly into the model’s weights\. This on\-policy approach is attractive because it provides fine\-grained credit assignment at the token level rather than distributing reward uniformly across entire trajectories \(see example in Figure[1](https://arxiv.org/html/2605.30861#S1.F1)\)\. Moreover, it can apply beyond verifiable reward settings since it does not directly rely on verifier signals, though in our setting we also leverage verifier outputs\.

![Refer to caption](https://arxiv.org/html/2605.30861v1/x1.png)Figure 1:Example of Feedback Distillation on a Lean statement from the MiniF2F dataset\(Zhenget al\.,[2022](https://arxiv.org/html/2605.30861#bib.bib9)\), with Qwen3\-8B as the student\. Claude provides feedback on the student’s attempt\. The student’s answer is then colored token\-by\-token bylog⁡pteacher−log⁡pstudent\\log p\_\{\\text\{teacher\}\}\-\\log p\_\{\\text\{student\}\}: green tokens are preferred by the teacher, red tokens by the student, and white tokens are assigned roughly equal probability\. The student writes “π\\pi” where the teacher would have written “Real” with 98% probability, reflecting Claude’s feedback\. Through the KL loss, the student is trained to increase the probability ofRealat this position, and thus learns to write better Lean code\.#### Contributions\.

In this work, we investigate the performance of self\-distillation in the context of training LLMs for mathematics\. More precisely,

- •We propose*Feedback Distillation*, a variant of self\-distillation in which the privileged information is feedback produced by a frozen copy of the model or a third\-party LLM in response to the model’s attempt and the verifier’s output, rather than raw environment signals or ground\-truth solutions \(Section[3](https://arxiv.org/html/2605.30861#S3)\)\.
- •We evaluate Feedback Distillation in the Lean 4 formal mathematics environment \(Section[4](https://arxiv.org/html/2605.30861#S4)\)\. We show that it maintains higher policy entropy than GRPO and achieves better pass@kkscaling, indicating greater output diversity\. Furthermore, we show that the two methods are complementary: initializing GRPO from a Feedback Distillation checkpoint outperforms GRPO alone\. After training on LeanWorkbook, Qwen3\.5\-9B achieves 59% pass@1 test accuracy on a test split of LeanWorkbook with GRPO alone compared to 75% with Feedback Distillation\+GRPO\.
- •We provide a detailed analysis of Feedback Distillation: we compare with other sources of feedback, and discuss training instability and qualitative consequences of our training methodology, which can be seen as a form of on\-policy knowledge transfer \(Section[5](https://arxiv.org/html/2605.30861#S5)\)\.

## 2Related work

#### Self\-distillation for LLMs\.

A recent line of work trains LLMs by minimizing the divergence between a student and a teacher that shares the same architecture but is conditioned on privileged information\.Hübotteret al\.\([2026](https://arxiv.org/html/2605.30861#bib.bib3)\)use environment outputs as the privileged signal whileShenfeldet al\.\([2026](https://arxiv.org/html/2605.30861#bib.bib2)\); Zhaoet al\.\([2026](https://arxiv.org/html/2605.30861#bib.bib11)\)use a ground\-truth solution as the privileged information\. Our work extends this line of research by using feedback from a frozen copy of the model or from a third\-party LLM\. Furthermore, we perform a careful analysis of the properties of self\-distillation, demonstrating in particular that it maintains greater trajectory diversity than GRPO, which translates into better test\-time scaling when starting from a weak student in a difficult RL environment \(formal mathematics\)\.

#### RL for formal mathematics\.

State\-of\-the\-art provers in formal mathematics usually follow a two\-phase pipeline\(Linet al\.,[2025](https://arxiv.org/html/2605.30861#bib.bib13); Renet al\.,[2025](https://arxiv.org/html/2605.30861#bib.bib14)\): supervised fine\-tuning on synthetic proof data coming from the formalization of natural\-language proofs, followed by GRPO\-based RL, often referred to as reinforcement learning with verifiable rewards \(RLVR\)\. Recent progress on benchmarks such as MiniF2F\(Zhenget al\.,[2022](https://arxiv.org/html/2605.30861#bib.bib9)\)and PutnamBench\(Tsoukalaset al\.,[2024](https://arxiv.org/html/2605.30861#bib.bib22)\)has increasingly come from test\-time scaling rather than improved training\(e\.g\., Varamballyet al\.,[2026](https://arxiv.org/html/2605.30861#bib.bib15)\)\. This scaling is achieved through agentic pipelines combining a trained prover with a reasoning model and iterative interaction with the Lean environment\. While these scaffolding strategies are orthogonal to our work, they underscore the continued importance of strong base provers, whose training we aim to improve\.

## 3Feedback Distillation

Following the self\-distillation methodology\(Hübotteret al\.,[2026](https://arxiv.org/html/2605.30861#bib.bib3); Shenfeldet al\.,[2026](https://arxiv.org/html/2605.30861#bib.bib2); Zhaoet al\.,[2026](https://arxiv.org/html/2605.30861#bib.bib11)\), our training loss measures the divergence between two instances of the same model with independent weights, a*student*and a*teacher*, the latter receiving privileged information in its prompt\. Both instances are initialized from the same pretrained LLMπ\\pi\. We seek to post\-train on a task for which we have a datasetDDof problems without solutions \(e\.g\., Lean statements without proofs\)\.

Specifically, given an attempted proofy∼πθ\(⋅∣x\)y\\sim\\pi\_\{\\theta\}\(\\cdot\\mid x\)for a problemx∼Dx\\sim D, we define the teacher as

πμ,y′\(⋅∣x\)=πμ\(⋅∣x,F\(y\)\),\\pi^\{\\prime\}\_\{\\mu,y\}\(\\cdot\\mid x\)\\;=\\;\\pi\_\{\\mu\}\(\\cdot\\mid x,\\,F\(y\)\),whereFFis a function that takes an attempted responseyyand returns a textual feedback signal \(the privileged information\)\. For consistency with prior work, we refer toπμ,y′\\pi^\{\\prime\}\_\{\\mu,y\}as the teacher model, though it would be more accurate to describe it as an augmented student\. In our setting, the feedbackFFis an LLM that analyzes the attemptyy\. Since the feedback may originate from a stronger model, we use the term*Feedback Distillation*\. The feedback model may also be a frozen copy ofπ\\pi, which we sometimes refer to as Self\-Feedback Distillation\. We refer to Sections[2](https://arxiv.org/html/2605.30861#S2)and[5\.1](https://arxiv.org/html/2605.30861#S5.SS1)for discussion on other sources of feedback\. We give examples of feedback in Figure[1](https://arxiv.org/html/2605.30861#S1.F1)and Appendix[D](https://arxiv.org/html/2605.30861#A4)\.

FollowingHübotteret al\.\([2026](https://arxiv.org/html/2605.30861#bib.bib3)\), we update the teacher’s weights via exponential moving average \(EMA\): every five gradient steps, we setμ←α​μ\+\(1−α\)​θ\\mu\\leftarrow\\alpha\\,\\mu\+\(1\-\\alpha\)\\,\\theta, whereα∈\[0,1\]\\alpha\\in\[0,1\]is a hyperparameter\. This hyperparameter has a critical impact on stability and performance \(see Section[5\.2](https://arxiv.org/html/2605.30861#S5.SS2)\)\.

Our loss is the per\-token Kullback\-Leibler divergence between the teacher and student distributions along trajectories sampled from the student, namely:

ℒθ=𝔼x∼D,y∼πθ\(⋅∣x\)\[∑t=1\|y\|KL\(πμ,y′\(⋅∣x,y<t\)∥πθ\(⋅∣x,y<t\)\)\],\\mathcal\{L\}\_\{\\theta\}\\;=\\;\\mathbb\{E\}\_\{x\\sim D,\\;y\\sim\\pi\_\{\\theta\}\(\\cdot\\mid x\)\}\\bigg\[\\sum\_\{t=1\}^\{\|y\|\}\\mathrm\{KL\}\\\!\\left\(\\pi^\{\\prime\}\_\{\\mu,y\}\(\\cdot\\mid x,y\_\{<t\}\)\\;\\\|\\;\\pi\_\{\\theta\}\(\\cdot\\mid x,y\_\{<t\}\)\\right\)\\bigg\],where gradients are not propagated through the sampling ofyy, and\|y\|\|y\|denotes the length of the sequenceyy\. WithVVthe vocabulary, the per\-token KL divergence is

KL\(πμ,y′\(⋅∣x,y<t\)∥πθ\(⋅∣x,y<t\)\)=∑a∈Vπμ,y′\(a∣x,y<t\)logπμ,y′​\(a∣x,y<t\)πθ​\(a∣x,y<t\)\.\\mathrm\{KL\}\\\!\\left\(\\pi^\{\\prime\}\_\{\\mu,y\}\(\\cdot\\mid x,y\_\{<t\}\)\\;\\\|\\;\\pi\_\{\\theta\}\(\\cdot\\mid x,y\_\{<t\}\)\\right\)\\;=\\;\\sum\_\{a\\in V\}\\pi^\{\\prime\}\_\{\\mu,y\}\(a\\mid x,y\_\{<t\}\)\\log\\frac\{\\pi^\{\\prime\}\_\{\\mu,y\}\(a\\mid x,y\_\{<t\}\)\}\{\\pi\_\{\\theta\}\(a\\mid x,y\_\{<t\}\)\}\.
Since the teacher’s distribution does not depend onθ\\theta, the KL divergence and the cross\-entropy have the same gradient with respect toθ\\theta\(see Appendix[B](https://arxiv.org/html/2605.30861#A2)\)\. For a sampled problemx∼Dx\\sim Dand attempty∼πθ\(⋅∣x\)y\\sim\\pi\_\{\\theta\}\(\\cdot\\mid x\)with feedbackF​\(y\)F\(y\), this yields the following equivalent loss, which we use in practice:

ℒ^θ=−∑t=1\|y\|∑a∈Vπμ​\(a∣x,F​\(y\),y<t\)​log⁡πθ​\(a∣x,y<t\)\.\\hat\{\\mathcal\{L\}\}\_\{\\theta\}\\;=\\;\-\\sum\_\{t=1\}^\{\|y\|\}\\sum\_\{a\\in V\}\\pi\_\{\\mu\}\(a\\mid x,\\,F\(y\),\\,y\_\{<t\}\)\\;\\log\\pi\_\{\\theta\}\(a\\mid x,\\,y\_\{<t\}\)\.
#### Top\-KKtruncation\.

To reduce computational cost, we truncate the sum over the vocabulary to theKKtokens with the highest probability under the teacherπμ,y′\\pi^\{\\prime\}\_\{\\mu,y\}, usingK=25K=25in practice\.

## 4Capabilities of Feedback Distillation for Lean Theorem Proving

In this section, we provide evidence that training with Feedback Distillation enables the model to learn efficiently, outperforming GRPO in performance and policy diversity\.

### 4\.1Lean environment

Our experimental setting is the Lean 4 formal mathematics environment\(de Moura and Ullrich,[2021](https://arxiv.org/html/2605.30861#bib.bib6)\)\. It is a well\-suited testbed for studying RL for complex reasoning for several reasons: \(i\) our base models \(Qwen3\-8B,Team,[2025](https://arxiv.org/html/2605.30861#bib.bib4), and Qwen3\.5\-9B,Team,[2026](https://arxiv.org/html/2605.30861#bib.bib53)\) have little proficiency in Lean 4, scoring respectively 2% and 11% on MiniF2F at initialization in our setup, so any meaningful improvement requires discovering new capabilities; \(ii\) the search space is vast, as the model must learn to invoke appropriate tactics and reference lemmas from Mathlib, Lean’s main mathematical library comprising over 300,000 declarations; \(iii\) the Lean verifier provides ground\-truth feedback on whether a proof attempt is correct\. Results in the main paper are given for Qwen3\.5\-9B and in the appendix for Qwen3\-8B\.

#### Tool interface\.

Tool use is a key component of state\-of\-the\-art formal mathematics models\(Liuet al\.,[2026](https://arxiv.org/html/2605.30861#bib.bib49)\), enabling iterative interaction with the proof assistant rather than single\-shot generation\. When the model produces a tool call, generation stops, the tool is executed, and its output is appended to the context before resuming generation\. We equip the model with three tools to interact with the Lean environment\.

- •lean\_write\_file: write a Lean source file;
- •lean\_check\_file: compile a previously written file and return the compiler output \(errors, warnings, or success\);
- •rg\_in\_mathlib: search Mathlib using regular expressions to find relevant lemmas\.

We confirm in Appendix[A\.2](https://arxiv.org/html/2605.30861#A1.SS2)that tool use improves performance in our setting\. A problem is considered solved when the model writes a Lean file that compiles and proves the statement\.

### 4\.2Experimental setting

We describe here the main ingredients of the experimental setting\. Hyperparameters used can be found in Appendix[A\.1](https://arxiv.org/html/2605.30861#A1.SS1)\.

#### Datasets and generation\.

We train on a subset of 10,000 statements with known proofs drawn from LeanWorkbook\(Yinget al\.,[2025](https://arxiv.org/html/2605.30861#bib.bib8)\)\. For evaluation, we use a test set of LeanWorkbook comprising 256 statements as well as the test split of MiniF2F\(Zhenget al\.,[2022](https://arxiv.org/html/2605.30861#bib.bib9)\), a standard benchmark of 244 competition\-level problems formalized in Lean\. Each attempt consists of a single generation of up to 8,192 tokens, within which the model may invoke multiple tool calls\. All experiments are run on a single node equipped with 8× NVIDIA H200 GPUs\. GRPO experiments take on average550550s per training step, while Feedback Distillation requires300300s per step\. We use theverlcodebase for the experiments\(Shenget al\.,[2024](https://arxiv.org/html/2605.30861#bib.bib56)\)and the Kimina Lean Server\(Santoset al\.,[2025](https://arxiv.org/html/2605.30861#bib.bib57)\)to assess the correctness of Lean proofs\.

#### Feedback model\.

We experiment with Claude Opus 4\.6\(Anthropic,[2026](https://arxiv.org/html/2605.30861#bib.bib10)\)as the feedback model \(see Section[5\.1](https://arxiv.org/html/2605.30861#S5.SS1)for discussion on sources of feedback\)\. The feedback model receives the formal statementxx, the model’s attemptyy\(including all tool calls and their outputs\), and the final Lean compiler output\. It is prompted to produce a few actionable directives of the form*“Do X”*or*“Don’t do X”*, identifying proof strategy errors, flagging misuse of tactics or lemmas, or encouraging better tool usage \(see Appendix[A\.3](https://arxiv.org/html/2605.30861#A1.SS3)\)\. The feedback is framed to be useful for a new attempt at the same problem\. Examples of feedback are shown in Appendix[D](https://arxiv.org/html/2605.30861#A4)\.

### 4\.3Results

Figure[2](https://arxiv.org/html/2605.30861#S4.F2)shows the training accuracy, test accuracy on LeanWorkbook and MiniF2F, and policy entropy over the course of training for both GRPO and Feedback Distillation\. We also experiment with*GRPO over Feedback Distillation*, meaning that we take a checkpoint from Feedback Distillation and continue training with GRPO\. Overall,Feedback Distillation is able to learn efficiently while maintaining diversity in the generated trajectories, as evidenced by the observations detailed below\. This is a desirable property in light of recent findings that GRPO tends to reduce the diversity of model outputs during training\(Danget al\.,[2025](https://arxiv.org/html/2605.30861#bib.bib19); Yueet al\.,[2025](https://arxiv.org/html/2605.30861#bib.bib1); Wuet al\.,[2026](https://arxiv.org/html/2605.30861#bib.bib18)\)\.

#### GRPO over Feedback Distillation performs best\.

We take checkpoints after200200,300300, and400400steps of Feedback Distillation and continue training with GRPO\. As shown in Figure[2](https://arxiv.org/html/2605.30861#S4.F2), this combination outperforms GRPO alone\. This suggests that the two methods provide complementary benefits\.

#### Entropy and pass@kk\.

Feedback Distillation maintains significantly higher entropy than GRPO throughout training, indicating that the policy preserves more diversity \(Figure[2](https://arxiv.org/html/2605.30861#S4.F2)\)\. This translates into better test\-time scaling: at checkpoints where GRPO and Feedback Distillation achieve similar pass@1, Feedback Distillation scales significantly better with increasingkk\(Figure[3](https://arxiv.org/html/2605.30861#S4.F3)\), confirming that the higher entropy reflects answer diversity rather than uniform noise\.

#### Number of used tactics\.

A concrete manifestation of Feedback Distillation’s greater trajectory diversity is the rate at which the model uses new Lean tactics and Mathlib lemmas in successful proofs over the course of training\. As shown in Figure[3](https://arxiv.org/html/2605.30861#S4.F3), Feedback Distillation leads to a faster and more sustained increase in the number of distinct tactics and lemmas invoked, compared to GRPO\.

#### Training instabilities\.

We observe training instabilities with GRPO and GRPO over Feedback Distillation\. This behavior was already noted in prior works\(Arnalet al\.,[2025](https://arxiv.org/html/2605.30861#bib.bib55); Simoniet al\.,[2025](https://arxiv.org/html/2605.30861#bib.bib54)\)\. We check that the maximum performance of GRPO over Feedback Distillation cannot be reproduced by GRPO alone simply by tuning the learning rate to delay instability \(see Appendix[C\.1](https://arxiv.org/html/2605.30861#A3.SS1)for details\)\. We also note that GRPO suffers from fewer instabilities with Qwen3\-8B \(see Appendix[C\.2](https://arxiv.org/html/2605.30861#A3.SS2)\)\. Importantly, the observation that GRPO combined with Feedback Distillation outperforms GRPO alone also holds for Qwen3\-8B, confirming that the improvements brought by Feedback Distillation are not merely a byproduct of GRPO instabilities\.

#### Sample efficiency\.

The results of Feedback Distillation in terms of sample efficiency are encouraging\. In particular, when using Qwen3\.5\-9B as a base model, Feedback Distillation is significantly more sample\-efficient in the early stages of training than GRPO, although GRPO eventually catches up before crashing\. Note that the batch size used for GRPO is five times larger than that used for Feedback Distillation, due to the group size of 5 \(see Appendix[A\.1](https://arxiv.org/html/2605.30861#A1.SS1)\)\. For Qwen3\-8B \(see Appendix[C\.2](https://arxiv.org/html/2605.30861#A3.SS2)\), we observe the same behavior, with Feedback Distillation being more sample\-efficient in the early stages of training\. We leave a more thorough assessment of sample efficiency for future work\.

![Refer to caption](https://arxiv.org/html/2605.30861v1/x2.png)Figure 2:Test accuracy, train accuracy, policy entropy, and MiniF2F accuracy for Claude Feedback Distillation, GRPO, and GRPO initialized from three different checkpoints from Claude Feedback Distillation\. GRPO over Feedback Distillation outperforms either method alone\.![Refer to caption](https://arxiv.org/html/2605.30861v1/x3.png)Figure 3:\(Left\) Rate of discovery of Mathlib lemmas: cumulative number of distinct lemmas used in correct proofs during training, divided by the training step\. Feedback Distillation leads to faster discovery of new lemmas from the Mathlib library\. \(Right\) Pass@kkscaling for two checkpoints at 200 steps of training with GRPO and Feedback Distillation \(from the experiment in Figure[2](https://arxiv.org/html/2605.30861#S4.F2)\), selected at peak GRPO performance where both methods have similar pass@1 accuracy\. Feedback Distillation scales better withkk, confirming that its higher entropy translates into greater answer diversity\.

## 5Analysis of Feedback Distillation

This section provides further analysis of Feedback Distillation\. We begin by discussing other sources of feedback than LLM\-generated advice based on a prior attempt, then the key role of EMA and its connection to training instability, before some qualitative comments\.

### 5\.1Other sources of feedback

We consider two baselines on top of Claude for the feedback source: ground truth feedback\(Shenfeldet al\.,[2026](https://arxiv.org/html/2605.30861#bib.bib2); Zhaoet al\.,[2026](https://arxiv.org/html/2605.30861#bib.bib11)\)and Lean output\(Hübotteret al\.,[2026](https://arxiv.org/html/2605.30861#bib.bib3)\)\. The ground truth feedback is a correct proof for the LeanWorkbook statement, formatted as‘‘Example of a correct solution:\{solution\}’’\. In case of failure, the Lean output feedback is the raw Lean compiler output formatted as‘‘The following is feedback from your unsuccessful earlier attempt: \{environment\_output\}’’, and in case of success it is the solution found, with the same format as for the ground truth feedback\.

A comparison of the performance is presented in Figure[4](https://arxiv.org/html/2605.30861#S5.F4)\. We observe that Claude and ground\-truth as feedback sources outperform Lean output\. This is expected, as both settings provide access to stronger sources of information\. We hypothesize that the performance of Claude\-based feedback could be further improved through better prompt design\. In principle, it could even outperform both Lean output and ground truth, since Claude has access to compiler outputs and is sufficiently capable to generate correct solutions for LeanWorkbook problems\. Notably, using Claude as a feedback model induces higher entropy than relying on ground\-truth solutions, which we attribute to the use of hints and corrections rather than fully specified answers\. We discuss the impact of prompt formulation in Section[5\.3](https://arxiv.org/html/2605.30861#S5.SS3)and leave further prompt engineering to future work\.

![Refer to caption](https://arxiv.org/html/2605.30861v1/x4.png)Figure 4:Feedback Distillation and GRPO over Feedback Distillation for different feedback sources: Claude, a ground truth Lean solution, and Lean compiler output\. Claude and ground truth feedback sources are a better initialization for the GRPO training\.#### Self\-Feedback Distillation\.

We consider an alternative source of feedback in which the feedback model is not a stronger external model, but the same model being trained, with frozen weights\. We refer to this setting as*Self\-Feedback Distillation*\. This setup enables a fair comparison with GRPO, as it does not introduce any additional source of information, and thus isolates the model’s ability to improve based on its own analysis of its generations\. As shown in Figure[5](https://arxiv.org/html/2605.30861#S5.F5), combining GRPO with Self\-Feedback Distillation leads to higher peak performance than GRPO alone, suggesting that the model is able to extract useful learning signals from its own feedback that are not discovered by GRPO in isolation\. However, performance remains below that obtained with Lean compilation feedback, despite the feedback model having access to this information in its context\. This suggests that further improvements may be achieved by refining the content and formulation of the feedback, pointing to promising directions for future work\.

![Refer to caption](https://arxiv.org/html/2605.30861v1/x5.png)Figure 5:GRPO over Self\-Feedback Distillation: when the feedback model is the same as the one we train \(Qwen3\.5\-9B\), GRPO over Self\-Feedback Distillation still outperforms GRPO alone\.

### 5\.2EMA and training instability

Since the model learns from multiple feedback signals over the course of training, a frozen teacher would be problematic: knowledge acquired from earlier feedback would be penalized, since the teacher would not internalize this information and assign it low probability\. EMA updates of the teacher address this issue by letting it progressively track the student \(Section[3](https://arxiv.org/html/2605.30861#S3)\)\. This echoes self\-supervised learning, where EMA target networks are widely used to prevent the representational collapse arising from moving targets\(see, e\.g\., Grillet al\.,[2020](https://arxiv.org/html/2605.30861#bib.bib35); Heet al\.,[2020](https://arxiv.org/html/2605.30861#bib.bib36); Assranet al\.,[2023](https://arxiv.org/html/2605.30861#bib.bib37)\)\. The EMA interpolation parameterα∈\[0,1\]\\alpha\\in\[0,1\]controls the tradeoff between adaptivity and stability\. To assess this, we report in Figure[6](https://arxiv.org/html/2605.30861#S5.F6)a sweep overα\\alpha\. We find that more aggressive updates lead to faster learning early in training, whileα=1\\alpha=1avoids instability at the cost of slow learning\. With our training budget,α=0\.9\\alpha=0\.9provides the best tradeoff\. Nevertheless, the long\-term instability of training even with largeα\\alphasuggests stabilization as an important area for future work\.

![Refer to caption](https://arxiv.org/html/2605.30861v1/x6.png)Figure 6:Test accuracy for different values of the EMA interpolation parameterα\\alpha\. A more aggressive EMA \(i\.e\., a lower value ofα\\alpha\) leads to faster training but also more instability\.α=1\\alpha=1is the same as freezing the teacher weights\. We useα=0\.9\\alpha=0\.9for all the experiments\.
### 5\.3Qualitative comments on Feedback Distillation

We give below a few additional qualitative comments on Feedback Distillation\.

#### The feedback is internalized into the model’s weights\.

To verify this, we study a simplified setting where the feedbackF​\(y\)F\(y\)is a fixed string throughout training\. We consider two cases: “Be concise” or “Think carefully before answering\. Verify that the solution is correct\.” In this experiment, the teacher is frozen\. As shown in Figure[7](https://arxiv.org/html/2605.30861#S5.F7), the average response length evolves consistently with the feedback, and the KL divergence between student and teacher vanishes\. This confirms that the student learns to match the teacher’s behavior by distilling the privileged information into its weights:after training, the student behaves as if the feedback were concatenated to every prompt\.

![Refer to caption](https://arxiv.org/html/2605.30861v1/x7.png)Figure 7:Effect of constant feedback on response length and policy entropy\. “Think” feedback increases response length while “Be concise” decreases it\. The KL divergence between student and teacher converges to zero, confirming that the feedback is internalized into the model’s weights\.
#### Feedback formulation\.

The formulation of the prompt sent to the feedback model to generate feedback plays a key role in training performance\. Increasing the level of structure and guidance in this prompt \(e\.g\., enforcing formatting constraints and requiring self\-contained feedback\) improves stability and final performance, while slowing early learning\. We refer to Appendix[C\.3](https://arxiv.org/html/2605.30861#A3.SS3)for a detailed analysis\.

#### Epistemic verbalization\.

Kimet al\.\([2026a](https://arxiv.org/html/2605.30861#bib.bib48)\)show that self\-distillation with rich privileged information \(e\.g\., a ground\-truth solution\) can suppress epistemic verbalization, i\.e\., the model’s use of uncertainty words such aswait,hmm,perhaps, leading to degraded out\-of\-distribution performance\. We observe in Appendix[C\.4](https://arxiv.org/html/2605.30861#A3.SS4)that this suppression occurs significantly less often when the feedback is phrased as a critique, as in Feedback Distillation, suggesting that the information content of the conditioning signal can control this effect\.

#### Feedback Distillation as on\-policy knowledge transfer\.

When the feedback model is stronger than the student, Feedback Distillation acts as indirect knowledge distillation: the strong model provides information without needing to supply a full solution, unlike in standard distillation\. The process is also inherently on\-policy, as the training signal is computed on the student’s generations, a property shown to improve generalization and reduce catastrophic forgetting compared to off\-policy methods such as SFT\(Shenfeldet al\.,[2026](https://arxiv.org/html/2605.30861#bib.bib2)\)\. A further practical advantage over standard on\-policy distillation\(Agarwalet al\.,[2024](https://arxiv.org/html/2605.30861#bib.bib21)\)is that knowledge is transferred through natural\-language feedback rather than logit matching, removing the need to host the feedback model or share its tokenizer\.

## 6Conclusion

While our current results do not yet match state\-of\-the\-art SFT\+GRPO pipelines trained at scale, we view Feedback Distillation as a promising mechanism that addresses fundamental limitations of existing approaches by injecting external knowledge, maintaining diversity, and providing fine\-grained credit assignment\. More broadly, current LLMs appear to have sufficient reasoning capabilities to analyze their own successes and failures in grounded environments like formal mathematics, and Feedback Distillation offers a way to internalize this self\-reflective ability into the model’s weights\. Our work opens several directions for future work\. Training stability remains a challenge for Feedback Distillation; developing more robust stabilization mechanisms is a natural next step toward scaling to longer training runs\. Additionally, while our results in Lean theorem proving are encouraging, extending Feedback Distillation to other formal and informal reasoning tasks could further demonstrate the generality of the approach\.

## References

- On\-policy distillation of language models: learning from self\-generated mistakes\.InThe Twelfth International Conference on Learning Representations,Cited by:[§1](https://arxiv.org/html/2605.30861#S1.p2.1),[§5\.3](https://arxiv.org/html/2605.30861#S5.SS3.SSS0.Px4.p1.1)\.
- Anthropic \(2026\)Note:Accessed: 2026\-04\-14External Links:[Link](https://www.anthropic.com/news/claude-opus-4-6)Cited by:[§4\.2](https://arxiv.org/html/2605.30861#S4.SS2.SSS0.Px2.p1.2)\.
- C\. Arnal, G\. Narozniak, V\. Cabannes, Y\. Tang, J\. Kempe, and R\. Munos \(2025\)Asymmetric reinforce for off\-policy reinforcement learning: balancing positive and negative rewards\.InAdvances in Neural Information Processing Systems,Cited by:[§4\.3](https://arxiv.org/html/2605.30861#S4.SS3.SSS0.Px4.p1.1)\.
- M\. Assran, Q\. Duval, I\. Misra, P\. Bojanowski, P\. Vincent, M\. Rabbat, Y\. LeCun, and N\. Ballas \(2023\)Self\-supervised learning from images with a joint\-embedding predictive architecture\.InProceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition,pp\. 15619–15629\.Cited by:[§5\.2](https://arxiv.org/html/2605.30861#S5.SS2.p1.5)\.
- M\. Besta, N\. Blach, A\. Kubicek, R\. Gerstenberger, M\. Podstawski, L\. Gianinazzi, J\. Gajda, T\. Lehmann, H\. Niewiadomski, P\. Nyczyk,et al\.\(2024\)Graph of thoughts: solving elaborate problems with large language models\.Proceedings of the AAAI Conference on Artificial Intelligence38\(16\),pp\. 17682–17690\.Cited by:[§1](https://arxiv.org/html/2605.30861#S1.p1.1)\.
- X\. Dang, C\. Baek, J\. Z\. Kolter, and A\. Raghunathan \(2025\)Assessing diversity collapse in reasoning\.InScaling Self\-Improving Foundation Models without Human Supervision,Cited by:[§4\.3](https://arxiv.org/html/2605.30861#S4.SS3.p1.1)\.
- L\. de Moura and S\. Ullrich \(2021\)The Lean 4 theorem prover and programming language\.InAutomated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings,Berlin,pp\. 625–635\.Cited by:[§4\.1](https://arxiv.org/html/2605.30861#S4.SS1.p1.1)\.
- J\. Grill, F\. Strub, F\. Altché, C\. Tallec, P\. H\. Richemond, E\. Buchatskaya, C\. Doersch, B\. A\. Pires, Z\. D\. Guo, M\. G\. Azar,et al\.\(2020\)Bootstrap your own latent: a new approach to self\-supervised learning\.InAdvances in Neural Information Processing Systems,Vol\.33,pp\. 21271–21284\.Cited by:[§5\.2](https://arxiv.org/html/2605.30861#S5.SS2.p1.5)\.
- K\. He, H\. Fan, Y\. Wu, S\. Xie, and R\. Girshick \(2020\)Momentum contrast for unsupervised visual representation learning\.InProceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition,pp\. 9729–9738\.Cited by:[§5\.2](https://arxiv.org/html/2605.30861#S5.SS2.p1.5)\.
- T\. Hubert, R\. Mehta, L\. Sartran, M\. Z\. Horváth, G\. Žužić, E\. Wieser, A\. Huang, J\. Schrittwieser, Y\. Schroecker, H\. Masoom,et al\.\(2025\)Olympiad\-level formal mathematical reasoning with reinforcement learning\.Nature,pp\. 1–3\.Cited by:[§1](https://arxiv.org/html/2605.30861#S1.p1.1)\.
- J\. Hübotter, F\. Lübeck, L\. Behric, A\. Baumann, M\. Bagatella, D\. Marta, I\. Hakimi, I\. Shenfeld, T\. K\. Buening, C\. Guestrin, and A\. Krause \(2026\)Reinforcement learning via self\-distillation\.External Links:2601\.20802Cited by:[§1](https://arxiv.org/html/2605.30861#S1.p3.1),[§2](https://arxiv.org/html/2605.30861#S2.SS0.SSS0.Px1.p1.1),[§3](https://arxiv.org/html/2605.30861#S3.p1.2),[§3](https://arxiv.org/html/2605.30861#S3.p3.2),[§5\.1](https://arxiv.org/html/2605.30861#S5.SS1.p1.1)\.
- J\. Kim, X\. Luo, M\. Kim, S\. Lee, D\. Kim, J\. Jeon, D\. Li, and Y\. Yang \(2026a\)Why does self\-distillation \(sometimes\) degrade the reasoning capability of llms?\.arXiv preprint arXiv:2603\.24472\.Cited by:[§5\.3](https://arxiv.org/html/2605.30861#S5.SS3.SSS0.Px3.p1.1)\.
- J\. Kim, X\. Luo, M\. Kim, S\. Lee, D\. Li, and Y\. Yang \(2026b\)Understanding reasoning in llms through strategic information allocation under uncertainty\.arXiv preprint arXiv:2603\.15500\.Cited by:[§C\.4](https://arxiv.org/html/2605.30861#A3.SS4.p1.1)\.
- K\. Kumar, T\. Ashraf, O\. Thawakar, R\. M\. Anwer, H\. Cholakkal, M\. Shah, M\. Yang, P\. H\. Torr, F\. S\. Khan, and S\. Khan \(2025\)LLM post\-training: a deep dive into reasoning large language models\.arXiv preprint arXiv:2502\.21321\.Cited by:[§1](https://arxiv.org/html/2605.30861#S1.p1.1)\.
- Y\. Li, D\. Choi, J\. Chung, N\. Kushman, J\. Schrittwieser, R\. Leblond, T\. Eccles, J\. Keeling, F\. Gimeno, A\. Dal Lago,et al\.\(2022\)Competition\-level code generation with alphacode\.Science378\(6624\),pp\. 1092–1097\.Cited by:[§1](https://arxiv.org/html/2605.30861#S1.p1.1)\.
- H\. Lightman, V\. Kosaraju, Y\. Burda, H\. Edwards, B\. Baker, T\. Lee, J\. Leike, J\. Schulman, I\. Sutskever, and K\. Cobbe \(2023\)Let’s verify step by step\.arXiv preprint arXiv:2305\.20050\.Cited by:[§1](https://arxiv.org/html/2605.30861#S1.p1.1)\.
- Y\. Lin, S\. Tang, B\. Lyu, Z\. Yang, J\. Chung, H\. Zhao, L\. Jiang, Y\. Geng, J\. Ge, J\. Sun, J\. Wu, J\. Gesi, X\. Lu, D\. Acuna, K\. Yang, H\. Lin, Y\. Choi, D\. Chen, S\. Arora, and C\. Jin \(2025\)Goedel\-prover\-V2: scaling formal theorem proving with scaffolded data synthesis and self\-correction\.External Links:2508\.03613Cited by:[§2](https://arxiv.org/html/2605.30861#S2.SS0.SSS0.Px2.p1.1)\.
- J\. Liu, Z\. Zhou, Z\. Zhu, M\. D\. Santos, W\. He, J\. Liu, R\. Wang, Y\. Xie, J\. Zhao, Q\. Wang,et al\.\(2026\)Numina\-lean\-agent: an open and general agentic reasoning system for formal mathematics\.arXiv preprint arXiv:2601\.14027\.Cited by:[§A\.2](https://arxiv.org/html/2605.30861#A1.SS2.p1.1),[§4\.1](https://arxiv.org/html/2605.30861#S4.SS1.SSS0.Px1.p1.1)\.
- A\. Peyronnet, F\. Gloeckle, and A\. Hayat \(2026\)LemmaBench: a live, research\-level benchmark to evaluate LLM capabilities in mathematics\.arXiv preprint arXiv:2602\.24173\.Cited by:[§1](https://arxiv.org/html/2605.30861#S1.p1.1)\.
- D\. Rein, B\. L\. Hou, A\. C\. Stickland, J\. Petty, R\. Y\. Pang, J\. Dirani, J\. Michael, and S\. R\. Bowman \(2024\)GPQA: a graduate\-level google\-proof q&a benchmark\.InFirst Conference on Language Modeling,Cited by:[§1](https://arxiv.org/html/2605.30861#S1.p1.1)\.
- Z\. Z\. Ren, Z\. Shao, J\. Song, H\. Xin, H\. Wang, W\. Zhao, L\. Zhang, Z\. Fu, Q\. Zhu, D\. Yang, Z\. F\. Wu, Z\. Gou, S\. Ma, H\. Tang, Y\. Liu, W\. Gao, D\. Guo, and C\. Ruan \(2025\)DeepSeek\-prover\-V2: advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition\.External Links:2504\.21801Cited by:[§2](https://arxiv.org/html/2605.30861#S2.SS0.SSS0.Px2.p1.1)\.
- S\. Ross and D\. Bagnell \(2010\)Efficient reductions for imitation learning\.InProceedings of the Thirteenth International Conference on Artificial Intelligence and Statistics,Vol\.9,pp\. 661–668\.Cited by:[§1](https://arxiv.org/html/2605.30861#S1.p2.1)\.
- B\. Rozière, J\. Gehring, F\. Gloeckle, S\. Sootla, I\. Gat, X\. E\. Tan, Y\. Adi, J\. Liu, R\. Sauvestre, T\. Remez, J\. Rapin,et al\.\(2023\)Code llama: open foundation models for code\.arXiv preprint arXiv:2308\.12950\.Cited by:[§1](https://arxiv.org/html/2605.30861#S1.p1.1)\.
- M\. D\. Santos, H\. Wang, H\. de Saxcé, R\. Wang, M\. Baksys, M\. Unsal, J\. Liu, Z\. Liu, and J\. Li \(2025\)Kimina lean server: technical report\.External Links:2504\.21230,[Link](https://arxiv.org/abs/2504.21230)Cited by:[§4\.2](https://arxiv.org/html/2605.30861#S4.SS2.SSS0.Px1.p1.2)\.
- Z\. Shao, P\. Wang, Q\. Zhu, R\. Xu, J\. Song, X\. Bi, H\. Zhang, M\. Zhang, Y\. Li,et al\.\(2024\)Deepseekmath: pushing the limits of mathematical reasoning in open language models\.arXiv preprint arXiv:2402\.03300\.Cited by:[§1](https://arxiv.org/html/2605.30861#S1.p1.1)\.
- I\. Shenfeld, M\. Damani, J\. Hübotter, and P\. Agrawal \(2026\)Self\-distillation enables continual learning\.External Links:2601\.19897Cited by:[§1](https://arxiv.org/html/2605.30861#S1.p2.1),[§1](https://arxiv.org/html/2605.30861#S1.p3.1),[§2](https://arxiv.org/html/2605.30861#S2.SS0.SSS0.Px1.p1.1),[§3](https://arxiv.org/html/2605.30861#S3.p1.2),[§5\.1](https://arxiv.org/html/2605.30861#S5.SS1.p1.1),[§5\.3](https://arxiv.org/html/2605.30861#S5.SS3.SSS0.Px4.p1.1)\.
- G\. Sheng, C\. Zhang, Z\. Ye, X\. Wu, W\. Zhang, R\. Zhang, Y\. Peng, H\. Lin, and C\. Wu \(2024\)HybridFlow: a flexible and efficient rlhf framework\.arXiv preprint arXiv: 2409\.19256\.Cited by:[§4\.2](https://arxiv.org/html/2605.30861#S4.SS2.SSS0.Px1.p1.2)\.
- M\. Simoni, A\. Fontana, G\. Rossolini, A\. Saracino, and P\. Mori \(2025\)Gtpo: stabilizing group relative policy optimization via gradient and entropy control\.arXiv preprint arXiv:2508\.03772\.Cited by:[§4\.3](https://arxiv.org/html/2605.30861#S4.SS3.SSS0.Px4.p1.1)\.
- Q\. Team \(2025\)Qwen3 technical report\.External Links:2505\.09388Cited by:[§4\.1](https://arxiv.org/html/2605.30861#S4.SS1.p1.1)\.
- Q\. Team \(2026\)Qwen3\.5: accelerating productivity with native multimodal agents\.External Links:[Link](https://qwen.ai/blog?id=qwen3.5)Cited by:[§4\.1](https://arxiv.org/html/2605.30861#S4.SS1.p1.1)\.
- The mathlib Community \(2020\)The Lean Mathematical Library\.InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs,CPP 2020,New Orleans\.Cited by:[§1](https://arxiv.org/html/2605.30861#S1.p2.1)\.
- T\. H\. Trinh, Y\. Wu, Q\. V\. Le, H\. He, and T\. Luong \(2024\)Solving olympiad geometry without human demonstrations\.Nature625\(7995\),pp\. 476–482\.Cited by:[§1](https://arxiv.org/html/2605.30861#S1.p1.1)\.
- G\. Tsoukalas, J\. Lee, J\. Jennings, J\. Xin, M\. Ding, M\. Jennings, A\. Thakur, and S\. Chaudhuri \(2024\)PutnamBench: evaluating neural theorem\-provers on the putnam mathematical competition\.InAdvances in Neural Information Processing Systems,Vol\.37,pp\. 11545–11569\.Cited by:[§2](https://arxiv.org/html/2605.30861#S2.SS0.SSS0.Px2.p1.1)\.
- S\. Varambally, T\. Voice, Y\. Sun, Z\. Chen, R\. Yu, and K\. Ye \(2026\)Hilbert: recursively building formal proofs with informal reasoning\.External Links:2509\.22819Cited by:[§2](https://arxiv.org/html/2605.30861#S2.SS0.SSS0.Px2.p1.1)\.
- F\. Wu, W\. Xuan, X\. Lu, M\. Liu, Y\. Dong, Z\. Harchaoui, and Y\. Choi \(2026\)The invisible leash: why RLVR may or may not escape its origin\.External Links:2507\.14843Cited by:[§4\.3](https://arxiv.org/html/2605.30861#S4.SS3.p1.1)\.
- S\. Yao, D\. Yu, J\. Zhao, I\. Shafran, T\. Griffiths, Y\. Cao, and K\. Narasimhan \(2023\)Tree of thoughts: deliberate problem solving with large language models\.Advances in neural information processing systems36,pp\. 11809–11822\.Cited by:[§1](https://arxiv.org/html/2605.30861#S1.p1.1)\.
- H\. Ying, Z\. Wu, Y\. Geng, Z\. Yuan, D\. Lin, and K\. Chen \(2025\)Lean workbook: a large\-scale Lean problem set formalized from natural language math problems\.External Links:2406\.03847Cited by:[§4\.2](https://arxiv.org/html/2605.30861#S4.SS2.SSS0.Px1.p1.2)\.
- Y\. Yue, Z\. Chen, R\. Lu, A\. Zhao, Z\. Wang, Y\. Yue, S\. Song, and G\. Huang \(2025\)Does reinforcement learning really incentivize reasoning capacity in LLMs beyond the base model?\.External Links:2504\.13837Cited by:[§1](https://arxiv.org/html/2605.30861#S1.p2.1),[§4\.3](https://arxiv.org/html/2605.30861#S4.SS3.p1.1)\.
- S\. Zhao, Z\. Xie, M\. Liu, J\. Huang, G\. Pang, F\. Chen, and A\. Grover \(2026\)Self\-distilled reasoner: on\-policy self\-distillation for large language models\.External Links:2601\.18734Cited by:[§1](https://arxiv.org/html/2605.30861#S1.p3.1),[§2](https://arxiv.org/html/2605.30861#S2.SS0.SSS0.Px1.p1.1),[§3](https://arxiv.org/html/2605.30861#S3.p1.2),[§5\.1](https://arxiv.org/html/2605.30861#S5.SS1.p1.1)\.
- K\. Zheng, J\. M\. Han, and S\. Polu \(2022\)MiniF2F: a cross\-system benchmark for formal Olympiad\-level mathematics\.External Links:2109\.00110Cited by:[Figure 1](https://arxiv.org/html/2605.30861#S1.F1),[§2](https://arxiv.org/html/2605.30861#S2.SS0.SSS0.Px2.p1.1),[§4\.2](https://arxiv.org/html/2605.30861#S4.SS2.SSS0.Px1.p1.2)\.

## Acknowledgments and Disclosure of Funding

We are grateful to Julia Kempe for her help and valuable advice throughout the writing of this article\.

## Appendix ASetup and Implementation

### A\.1Training hyperparameters

Table[1](https://arxiv.org/html/2605.30861#A1.T1)lists the hyperparameters used in all Feedback Distillation and GRPO experiments reported in the paper\.

Table 1:Training hyperparameters for Feedback Distillation and GRPO experiments\.
### A\.2Tool use ablation

Figure[8](https://arxiv.org/html/2605.30861#A1.F8)compares training with and without tool access for both Claude Feedback Distillation and GRPO with Qwen3\-8B\. In both cases, tool use leads to higher MiniF2F accuracy and better training accuracy, confirming that iterative interaction with the Lean compiler is a driver of performance\(Liuet al\.,[2026](https://arxiv.org/html/2605.30861#bib.bib49)\)\.

![Refer to caption](https://arxiv.org/html/2605.30861v1/x8.png)Figure 8:Qwen3\-8B MiniF2F accuracy and training reward for Feedback Distillation and GRPO, with and without tool access\. Tool use improves performance for both methods\.
### A\.3Feedback prompt

The following prompt is given to the feedback model \(Claude Opus 4\.6\) along with the formal statementxx, the model’s attemptyy\(including tool calls and their outputs\), and the final Lean compiler output\.

> You are an expert feedback tutor\. Given a problem and a student’s attempt, write concise, actionable pieces of advice that will provide general feedback from the student’s experience\. Write between 1 and 3 numbered pieces of feedback about errors, things that were useful, or things that were not\. The feedback must be self\-contained and useful to someone who does not have access to the student’s answer\. It must be framed as orders, like “Do X” or “Don’t do X”, without mentioning the student\. Each piece of feedback must be between 10 and 50 words\. The goal is not to comment on the performance of the student, but to provide useful feedback for someone who might want to try the same problem in the future\. Do not use “you”, “your”, or the second person in general\. It must be useful to someone who does not know there is a student\. It must encourage the usage of tools\. Do not output anything other than the feedback — no introduction, directly the 1\. of the first piece of advice\. If the answer seems truncated at the end, it may be because the student reached the token limit; in this case, order to be more concise\.

## Appendix BLoss derivation

Since gradients are not propagated through the sampling ofyy\(stop\-gradient\), the gradient ofℒθ\\mathcal\{L\}\_\{\\theta\}with respect toθ\\thetareduces to differentiating only throughπθ\\pi\_\{\\theta\}inside the KL:

∇θℒθ=−𝔼x∼D,y∼πθ\(⋅∣x\)​\[∑t=1\|y\|∑a∈Vπμ,y′​\(a∣x,y<t\)​∇θlog⁡πθ​\(a∣x,y<t\)\]\.\\nabla\_\{\\theta\}\\mathcal\{L\}\_\{\\theta\}\\;=\\;\-\\mathbb\{E\}\_\{x\\sim D,\\;y\\sim\\pi\_\{\\theta\}\(\\cdot\\mid x\)\}\\left\[\\sum\_\{t=1\}^\{\|y\|\}\\sum\_\{a\\in V\}\\pi^\{\\prime\}\_\{\\mu,y\}\(a\\mid x,y\_\{<t\}\)\\;\\nabla\_\{\\theta\}\\log\\pi\_\{\\theta\}\(a\\mid x,y\_\{<t\}\)\\right\]\.Since the entropy of the teacherH​\(πμ,y′\)H\(\\pi^\{\\prime\}\_\{\\mu,y\}\)does not depend onθ\\theta, the KL divergence and the cross\-entropy have the same gradient with respect toθ\\theta\. Expandingπμ,y′\\pi^\{\\prime\}\_\{\\mu,y\}by its definition, we obtain the gradient\-equivalent loss used in practice:

ℒ^θ=−∑t=1\|y\|∑a∈Vπμ​\(a∣x,F​\(y\),y<t\)​log⁡πθ​\(a∣x,y<t\)\.\\hat\{\\mathcal\{L\}\}\_\{\\theta\}\\;=\\;\-\\sum\_\{t=1\}^\{\|y\|\}\\sum\_\{a\\in V\}\\pi\_\{\\mu\}\(a\\mid x,\\,F\(y\),\\,y\_\{<t\}\)\\;\\log\\pi\_\{\\theta\}\(a\\mid x,\\,y\_\{<t\}\)\.

## Appendix CAdditional Results and Analysis

### C\.1Learning rate sweep for GRPO

In this section, we verify that the best performance achieved by GRPO is consistent with the results shown in Figure[2](https://arxiv.org/html/2605.30861#S4.F2), regardless of the choice of learning rate around10−710^\{\-7\}\. To this end, we evaluate two additional values,3⋅10−73\\cdot 10^\{\-7\}and3⋅10−83\\cdot 10^\{\-8\}\. As shown in Figure[9](https://arxiv.org/html/2605.30861#A3.F9), all three learning rates lead to similar peak performance\.

![Refer to caption](https://arxiv.org/html/2605.30861v1/x9.png)Figure 9:Accuracy on the LeanWorkbook test set and MiniF2F when training with GRPO using three different learning rates\. All configurations reach similar peak performance\.
### C\.2Results with Qwen3\-8B

We confirm in this section that the same conclusions hold for Qwen3\-8B as for Qwen3\.5\-9B\.

#### GRPO over Feedback Distillation\.

Training is more stable with Qwen3\-8B, and we still observe the same conclusion as in Figure[2](https://arxiv.org/html/2605.30861#S4.F2): GRPO over Feedback Distillation outperforms GRPO alone \(we also use Claude Opus 4\.6 as the feedback model for Feedback Distillation\)\.

![Refer to caption](https://arxiv.org/html/2605.30861v1/x10.png)Figure 10:MiniF2F accuracy and policy entropy for Claude Feedback Distillation, GRPO, and GRPO initialized from a checkpoint from Claude Feedback Distillation, for Qwen3\-8B\. GRPO over Feedback Distillation outperforms either method alone\.
#### EMA and training instability\.

Consistent with the observations in Figure[6](https://arxiv.org/html/2605.30861#S5.F6)for Qwen3\.5\-9B, we find in Figure[11](https://arxiv.org/html/2605.30861#A3.F11)that the same trend holds for Qwen3\-8B: more aggressive EMA updates lead to faster early learning, but induce greater instability and ultimately limit peak performance\.

![Refer to caption](https://arxiv.org/html/2605.30861v1/x11.png)Figure 11:MiniF2F accuracy for Qwen3\-8B during training for different values of the EMA interpolation parameterα\\alpha\. More aggressive EMA updates \(i\.e\., lower values ofα\\alpha\) accelerate early learning but result in increased instability\. The caseα=1\\alpha=1corresponds to freezing the teacher weights\.

### C\.3Feedback formulation

We investigate how the formulation of feedback affects training performance\. To this end, we evaluate four different prompt styles for Claude Opus 4\.6 as the feedback model, while keeping all other hyperparameters fixed\. The prompts are ordered from \(1\) to \(4\) by increasing level of structure and guidance, with each successive prompt introducing additional instructions: \(1\) a minimal prompt requesting feedback, \(2\) the addition of formatting constraints \(e\.g\., length and number of feedback items\), \(3\) a requirement that the feedback be self\-contained and useful to a reader without access to the student’s answer, and \(4\) additional guidance encouraging the use of tools and limiting generation length in case of truncation\. We use Prompt \(4\) in all experiments\.

#### Prompt templates\.

We provide below the four prompt formulations used in this study:

- •Prompt \(1\): Minimal feedback request > You are an expert feedback tutor\. Given a problem and a student’s attempt, write concise, actionable pieces of advice based on what the student did\.
- •Prompt \(2\): \+ Formatting constraints > You are an expert feedback tutor\. Given a problem and a student’s attempt, write concise, actionable pieces of advice based on what the student did\. Write between 1 and 3 numbered feedbacks about errors, things that were useful, or things that were not\. They must not be too long — between 10 and 50 words each\. Do not output anything else than the feedbacks, no introduction, directly the "1\." of the first advice\.
- •Prompt \(3\): \+ Self\-contained feedback requirement > You are an expert feedback tutor\. Given a problem and a student’s attempt, write concise, actionable pieces of advice based on what the student did\. Write between 1 and 3 numbered feedbacks about errors, things that were useful, or things that were not\. They must not be too long — between 10 and 50 words each\. Do not output anything else than the feedbacks, no introduction, directly the "1\." of the first advice\. The feedback must be self\-contained and useful to someone who does not have access to the student’s answer\. Don’t use "you", "your", or the second person in general — it must be useful to someone who doesn’t know there is a student\. It must be framed as orders, like "Do x" or "Don’t do x", without mentioning the student\. The goal is not to comment on the performance of the student, but to provide useful guidance for someone who might want to try the same problem in the future\.
- •Prompt \(4\): \+ Tool use and truncation guidance > You are an expert feedback tutor\. Given a problem and a student’s attempt, write concise, actionable pieces of advice that will provide general feedback from the student’s experience\. Write between 1 and 3 numbered pieces of feedback about errors, things that were useful, or things that were not\. The feedback must be self\-contained and useful to someone who does not have access to the student’s answer\. It must be framed as orders, like “Do X” or “Don’t do X”, without mentioning the student\. Each piece of feedback must be between 10 and 50 words\. The goal is not to comment on the performance of the student, but to provide useful feedback for someone who might want to try the same problem in the future\. Do not use “you”, “your”, or the second person in general\. It must be useful to someone who does not know there is a student\. It must encourage the usage of tools\. Do not output anything other than the feedback — no introduction, directly the 1\. of the first piece of advice\. If the answer seems truncated at the end, it may be because the student reached the token limit; in this case, order to be more concise\.

Figure[12](https://arxiv.org/html/2605.30861#A3.F12)shows that the formulation of the feedback has a significant impact on training dynamics\. More structured prompts, which provide richer and more constrained feedback, tend to yield slower initial performance gains but result in more stable training and higher peak performance\. In particular, prompts that encourage generic, self\-contained feedback \(Prompts 3 and 4\) appear to be especially beneficial\.

![Refer to caption](https://arxiv.org/html/2605.30861v1/x12.png)Figure 12:Impact of feedback prompt formulation on training performance\. Increasing the level of structure in the prompt improves stability and peak performance\.

### C\.4Epistemic verbalization and response length

FollowingKimet al\.\([2026b](https://arxiv.org/html/2605.30861#bib.bib50)\), we measure epistemic verbalization by counting the average number of uncertainty words generated by the student during training\. Figure[13](https://arxiv.org/html/2605.30861#A3.F13)reports the per\-step occurrence counts of three representative epistemic word categories \(see Section[5\.3](https://arxiv.org/html/2605.30861#S5.SS3)\) across training runs\. When the feedback consists of a ground\-truth solution, all three counts drop sharply early in training, reflecting the suppression of epistemic verbalization\. By contrast, when feedback is framed as a critique by a language model, whether the model itself or a stronger one, the counts do not follow the same dynamic throughout training \(especially when using Claude as the feedback model\), indicating that it is possible to preserve the epistemic ability of the student\. We attribute this to the student mimicking the teacher’s style, which is itself shaped by the feedback: a directive signal such as a worked\-out solution leads the teacher to reason with greater confidence, while a critique preserves more uncertainty expression\.

![Refer to caption](https://arxiv.org/html/2605.30861v1/x13.png)Figure 13:Occurrence counts of epistemic words \(*“check”*,*“wait”*, and a combined epistemic total aggregating*wait, hmm, perhaps, maybe, actually, alternatively, seems, might, likely, check*\) over training steps for Qwen3\-8B\. Ground\-truth feedback causes a marked decline in all three counts, whereas feedback framed as a critique by a language model — regardless of whether it comes from the student itself or a stronger model — preserves the student’s epistemic verbalization\.Critique\-based feedback is also associated with longer responses than ground\-truth feedback \(Figure[14](https://arxiv.org/html/2605.30861#A3.F14)\), consistent with models that maintain diversity in their generated trajectories rather than converging to short, confident proofs\.

![Refer to caption](https://arxiv.org/html/2605.30861v1/x14.png)Figure 14:Qwen3\-8B mean response length \(in tokens\) over training steps\. Critique\-based feedback \(Claude and self\-feedback\) is associated with longer responses than ground\-truth feedback, reflecting preserved diversity in generated trajectories\.

## Appendix DFeedback examples

The following are four representative feedback messages produced by Claude Opus 4\.6 at step 100 of Qwen3\-8B training with Feedback Distillation\. Each box corresponds to a different theorem\-proving attempt\.

1\.When proving inequalities involving absolute values in Lean 4, usercases le\_or\_lt b aandrcases le\_or\_lt c ato split into cases based on the sign of each expression inside the absolute values, then simplify usingabs\_of\_nonnegandabs\_of\_nonposbefore finishing withlinarith\.2\.Always write and test intermediate Lean files using thelean\_write\_filetool rather than reasoning entirely in one’s head — this ensures syntax errors and tactic failures are caught early and iteratively corrected\.3\.Structure the proof by first splitting onle\_or\_lt \(b \+ c\) ato handle\|a \- b \- c\|, then within thea < b \+ cbranch, further split on the signs ofa \- banda \- cto reduce all absolute values to linear expressions before applyinglinarith\.

1\.When working with natural number division in Lean 4, avoid assumingfield\_simpwill clear denominators as it does for fields; instead, useNat\.div\_mul\_cancelor establish divisibility \(n∣\\mid175\) first, then rewrite to eliminate the division before algebraic manipulation\.2\.Useomegaorinterval\_casesafter boundingnn\(e\.g\., from the equation deducen≤175n\\leq 175\) to let Lean automatically check all possible natural number values, which is often simpler than manual algebraic factoring for small search spaces\.3\.Write candidate proofs to a file usinglean\_write\_fileand check them withlean\_check\_fileiteratively, fixing errors based on compiler output rather than reasoning abstractly about tactic behavior\.

1\.Avoid division in Lean proofs over reals; instead, multiply through to keep all expressions polynomial, enablingringandnlinarithto close goals without needing to prove denominators are nonzero\.2\.Derive the key intermediate factx \* y \+ z \* \(x \+ y\) = 0by showing\(x \- y\) \* \(x \* y \+ z \* \(x \+ y\)\) = 0viahave : \.\.\. = xˆ2 \* \(y \+ z\) \- yˆ2 \* \(z \+ x\) := by ringcombined withlinarith \[h1, h2\], then usemul\_left\_cancel0withsub\_ne\_zero\.mpr hxy\.3\.After establishingx \* y \+ z \* \(x \+ y\) = 0, close the final goal usingnlinarith \[h1, h2, sq\_nonneg x, sq\_nonneg y, sq\_nonneg z, sq\_nonneg \(x \- y\)\]to let the nonlinear arithmetic solver combine all hypotheses without manual algebraic manipulation\.

1\.Decompose the inequality into provinga2\+b2\+c2\+d2≥4a^\{2\}\+b^\{2\}\+c^\{2\}\+d^\{2\}\\geq 4\(AM\-GM on squares with product\(a​b​c​d\)2=1\(abcd\)^\{2\}=1\) anda​b\+a​c\+a​d\+b​c\+b​d\+c​d≥6ab\+ac\+ad\+bc\+bd\+cd\\geq 6\(AM\-GM on six pairwise products with product\(a​b​c​d\)3=1\(abcd\)^\{3\}=1\), then combine withlinarith\.2\.When usingnlinarith, supply auxiliary lemmas as hints — e\.g\.,sq\_nonneg \(a\*b \- 1\),sq\_nonneg \(a\*c \- 1\),mul\_pos ha hb, and the hypothesish— so the solver can close the nonlinear arithmetic gap created by the constrainta​b​c​d=1abcd=1\.3\.Always write a complete, syntactically valid Lean file and verify it compiles using the tool before submitting; an incomplete or unreadable file scores zero regardless of mathematical correctness\.