Search papers, labs, and topics across Lattice.
This paper introduces Self-Guided Self-Play (SGS), a novel self-play algorithm designed to mitigate the problem of Conjecturer reward hacking that limits the scalability of existing LLM self-play methods. SGS incorporates a Guide role for the LLM, which scores synthetic problems based on their relevance and naturalness, thereby preventing the Conjecturer from generating artificially complex and unhelpful problems. Experiments in formal theorem proving with Lean4 demonstrate that SGS enables a 7B parameter model to outperform a 671B parameter model after 200 rounds of self-play, showcasing improved scaling properties compared to RL baselines.
LLMs can guide their own self-play, leading to superhuman performance with smaller models and less compute.
LLM self-play algorithms are notable in that, in principle, nothing bounds their learning: a Conjecturer model creates problems for a Solver, and both improve together. However, in practice, existing LLM self-play methods do not scale well with large amounts of compute, instead hitting learning plateaus. We argue this is because over long training runs, the Conjecturer learns to hack its reward, collapsing to artificially complex problems that do not help the Solver improve. To overcome this, we introduce Self-Guided Self-Play (SGS), a self-play algorithm in which the language model itself guides the Conjecturer away from degeneracy. In SGS, the model takes on three roles: Solver, Conjecturer, and a Guide that scores synthetic problems by their relevance to unsolved target problems and how clean and natural they are, providing supervision against Conjecturer collapse. Our core hypothesis is that language models can assess whether a subproblem is useful for achieving a goal. We evaluate the scaling properties of SGS by running training for significantly longer than prior works and by fitting scaling laws to cumulative solve rate curves. Applying SGS to formal theorem proving in Lean4, we find that it surpasses the asymptotic solve rate of our strongest RL baseline in fewer than 80 rounds of self-play and enables a 7B parameter model, after 200 rounds of self-play, to solve more problems than a 671B parameter model pass@4.
