CompassPlay: Rewarding the Proposer for Where It Moves the Solver
Sophia Xiao Pu, Ximeng Sun, Jiang Liu, Jialian Wu, Emad Barsoum, Zicheng Liu, William Yang Wang
cs.LG
Sep 26, 2026 · v1
TL;DR
Applies gradient-alignment proposer rewards to Lean 4 theorem-proving self-play with DeepSeek-Prover-V2, verifying proofs against mathlib4.
Abstract
In self-play, a proposer generates verifiable tasks to train a solver. Proposer rewards often depend on the solver's success rate, but equally difficult tasks can differ in their training value. We introduce CompassPlay, a self-play method that rewards the proposer through gradient alignment. The reward favors tasks whose solver loss gradients align with those of reference tasks representing the target capabilities. It draws on a first-order approximation to learning progress and scores each eligible task without additional solver training. Our experiments show gains in performance and training efficiency. In coding self-play with Qwen2.5-Coder-7B, a small external reference set guides task generation. CompassPlay improves average accuracy over AZR's difficulty reward by 1.5 percentage points on in-domain coding and 2.7 on out-of-domain mathematics. In Lean4 theorem proving, CompassPlay matches the difficulty baseline's 150-iteration cumulative coverage with 40% fewer GPU-hours.
Problem
In self-play, a proposer generates verifiable tasks to train a solver, but rewards based only on solver success rate cannot distinguish tasks of equal difficulty that differ in training value.
Approach
CompassPlay rewards the proposer through gradient alignment, favoring tasks whose solver loss gradients align (cosine similarity) with gradients of reference tasks representing target capabilities. This is a first-order proxy for learning progress that scores each candidate without extra solver training. It is evaluated in coding self-play (Qwen2.5-Coder-7B, Python execution verifier) and in Lean 4 theorem proving using separate DeepSeek-Prover-V2-7B proposer and solver models, checking proofs with the Lean 4 compiler against mathlib4. A novelty weighting is added to reduce seed-copying.
Results
In coding, CompassPlay improves average accuracy over AZR's difficulty reward by 1.5 points in-domain and 2.7 points on out-of-domain mathematics. In Lean, with novelty weighting it matches the difficulty baseline's 150-iteration cumulative coverage using 40% fewer GPU-hours and reduces the copy rate to zero.
| Method | Alignment | Novelty | Copy rate ↓ | Gain (targets) ↑ |
|---|
| CompassPlay (cos) | ✓ | ✗ | 0.712 | +3.1 |
| novelty-only | ✗ | ✓ | 0.000 | -7.9 |
| CompassPlay (cos×novelty) | ✓ | ✓ | 0.000 | +13.6 |
Lean self-play: alignment and novelty ablation (copy rate and coverage gain on targets)
