通过自我指导扩展自我游戏

LLM 自对弈算法的值得注意之处在于，原则上没有任何东西限制它们的学习：猜想者模型为求解器创造问题，并且两者共同改进。然而，在实践中，现有的 LLM 自对弈方法不能很好地适应大量计算，反而会陷入学习瓶颈。我们认为这是因为在长时间的训练中，猜想者学会了破解其奖励，陷入人为的复杂问题，而这些问题无助于求解器的改进。为了克服这个问题，我们引入了自我引导的自我对弈（SGS），这是一种自我对弈算法，其中语言模型本身引导猜想者远离退化。在 SGS 中，模型承担三个角色：求解器、猜想器和指南，根据综合问题与未解决的目标问题的相关性以及它们的干净程度和自然程​​度对综合问题进行评分，从而对猜想器崩溃提供监督。我们的核心假设是语言模型可以评估子问题是否对实现目标有用。我们通过运行训练时间明显长于之前的工作以及将缩放法则拟合到累积求解率曲线来评估 SGS 的缩放属性。将 SGS 应用于 Lean4 中的形式定理证明，我们发现它在不到 80 轮的自我对弈中超越了我们最强的 RL 基线的渐近解决率，并且使得 7B 参数模型在 200 轮自我对弈后能够比 671B 参数模型 pass@4 解决更多的问题。