Lean 정리 증명을 위한 LLM 피드백 증류

초록

추론 모델을 위한 사후 훈련은 일반적으로 감독형 미세 조정과 검증 가능한 보상에 기반한 강화 학습을 결합하며, 가장 흔히 GRPO를 사용한다. 그러나 이 알고리즘은 희소 보상, 제한된 탐색, 그리고 모드 붕괴 문제를 겪는다. 본 논문은 최근의 자기 증류 연구를 기반으로, 모델이 언어 모델에 의해 생성된 특권 피드백을 조건으로 한 자신의 분포를 토큰 수준에서 일치하도록 훈련하는 기법인 피드백 증류(Feedback Distillation)를 제안한다. 피드백 증류는 토큰 수준의 감독을 제공하며 외부 지식을 주입할 수 있다. Lean4 정리 증명에서 본 방법을 평가한 결과, 피드백 증류는 GRPO보다 생성된 궤적에서 더 큰 다양성을 유지하며, 더 높은 정책 엔트로피와 더 나은 pass@k 스케일링을 보였다. 두 방법은 상호 보완적이다. 피드백 증류 체크포인트에서 GRPO를 초기화하면 단일 방법만 사용할 때보다 우수한 성능을 나타낸다. 종합적으로, 본 연구 결과는 복잡한 추론을 위한 사후 훈련을 개선할 유망한 방향을 제시한다.

English

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.