蒸餾 LLM 回饋用於 Lean 定理證明

研究論文提出了一種名為 Feedback Distillation 的訓練方法，旨在改善大型語言模型在後訓練階段的推理能力。論文指出，傳統後訓練方式結合監督微調與基於可驗證獎勵的強化學習，其中 GRPO 是常用算法，但存在獎勵稀疏、探索有限和模式崩潰等問題。Feedback Distillation 通過在 token 層面匹配模型自身在特權回饋下的分佈來進行訓練，提供 token 層面的監督並注入外部知識。在 Lean4 定理證明的評估中，Feedback Distillation 生成的軌跡展現出更大的多樣性，具有更高的策略熵和更好的 pass@k 擴展性。論文進一步指出，兩種方法具有互補性：從 Feedback Distillation 檢查點初始化 GRPO 的表現優於單獨使用任一方法。總體而言，研究結果表明 Feedback Distillation 為改善複雜推理的後訓練提供了 promising 的途徑。