arXiv preprint · 2026

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¹

¹University of California, Santa Barbara ²Advanced Micro Devices

xiao_pu@ucsb.edu · Ximeng.Sun@amd.com

(a) CompassPlay loop: the proposer sends a task to the solver, a verifier checks the solution, and the proposer is rewarded by the alignment between the candidate loss gradient and the reference loss gradient. (b) Out-of-domain math accuracy over coding self-play training, ours above the difficulty reward. (c) Lean coverage over iterations: ours reaches the difficulty baseline's final coverage at iteration 93 instead of 150. — **(a)** The proposer is rewarded for aligning the current solver's loss gradients on verified candidate solutions with those on reference solutions. **(b)** Coding self-play, mean over five out-of-domain mathematics benchmarks, 3-point rolling mean of three seeds (±1 s.d.); ours uses cosine similarity. **(c)** Lean self-play, coverage of the 3323-statement target set from iteration 10; ours uses cosine similarity weighted by novelty.

+1.5pts

in-domain coding accuracy over AZR's difficulty reward, Qwen2.5-Coder-7B

+2.7pts

out-of-domain mathematics, with math seen only through a 32-problem reference set

40%fewer

GPU-hours to reach the difficulty baseline's final Lean 4 coverage (93 vs 150 iterations)

Abstract

In self-play, a proposer generates verifiable tasks to train a solver. Most proposer rewards 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 compares training gradients on proposed tasks with gradients on reference tasks representing the solver's target capabilities. It draws on a first-order approximation to learning progress and scores each 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 mathematics reference set guides task generation. CompassPlay improves over AZR's difficulty reward by 1.5 points on in-domain coding and 2.7 points on out-of-domain mathematics. In Lean 4 theorem proving, CompassPlay matches the difficulty baseline's final cumulative coverage with 40% fewer GPU-hours.

Method

Reward the direction a task moves the solver

A difficulty reward such as 1 − s(x̃) gives the same score to every task with the same solve rate. CompassPlay asks a different question: if the solver took one gradient step on this task, how much would its loss on the target capabilities drop?

For a candidate task x̃ with a verified solution, let g(x̃) be the solver's loss gradient on it, and let g_ref be the gradient of a reference loss. To first order, the reference-loss decrease from a small step on the candidate is their inner product:

U(x̃) = ℒ_ref(θ) − ℒ_ref(θ − η g(x̃)) = η ⟨g(x̃), g_ref⟩ + O(η²)

The inner product also grows with the candidate's gradient norm, which a proposer can raise without making its tasks more useful. We keep only the direction and pay the proposer the cosine:

r_cos(x̃) = cos(g(x̃), g_ref) = ⟨g(x̃), g_ref⟩ / (‖g(x̃)‖ ‖g_ref‖) bounded in [−1, 1], computed at the solver's current parameters

Each eligible candidate (well-posed, 0 < s(x̃) < 1) receives its own score for one extra forward/backward pass. There is no inner training run and no optimizer step, and the reference direction moves with the solver as training proceeds.

External reference · coding

32 held-out MATH problems

The reference loss is the cross-entropy of gold solutions to 32 MATH-train problems, disjoint from every evaluation set and never shown to the proposer. The proposer still writes coding tasks; the reward asks for coding tasks whose gradients point toward mathematical reasoning.

r = cos(g(x̃), g_ref)

Local reference · Lean 4

The solver's own proof of the seed

With no gold proofs available, g_ref is the gradient of the solver's verified proof of the seed theorem the proposer conditions on. A novelty factor, one minus token-Jaccard similarity to the seed, keeps the proposer from re-emitting renamed copies of that seed.

r = cos(g(x̃), g_ref) · (1 − J(x̃, x_seed))

Coding self-play

Better coding and better math than AZR's difficulty reward

Single-model self-play on Qwen2.5-Coder-7B following AZR's training configuration, task types and evaluation; methods differ only in the proposer reward. Scores are the mean over the final quarter of training (steps 150 to 200, 11 greedy evaluations), averaged over three seeds, ± sample s.d. CompassPlay is above the difficulty reward on all eight benchmarks.

In-domain coding accuracy (%)
Method	LiveCodeBench	CRUXEval-I	CRUXEval-O	Mean
Base model	40.02	48.98	50.89	46.63
Difficulty (AZR)	49.87 ±1.62	59.63 ±0.12	61.23 ±0.47	56.91 ±0.72
CompassPlay (cos)	52.60 ±0.17	60.08 ±0.34	62.56 ±0.44	58.41 ±0.18
Gain over AZR	+2.73	+0.45	+1.33	+1.50

Out-of-domain mathematics accuracy (%)
Method	MATH500	AMC23	GSM8K	Minerva	OlympiadBench	Mean
Base model	53.40	45.00	67.00	18.00	19.30	40.54
Difficulty (AZR)	60.73 ±2.63	43.94 ±0.92	76.98 ±1.83	26.54 ±1.40	30.40 ±2.04	47.72 ±1.07
CompassPlay (cos)	63.34 ±3.77	47.12 ±6.56	78.72 ±1.95	29.14 ±2.34	33.53 ±1.58	50.37 ±2.87
Gain over AZR	+2.61	+3.18	+1.74	+2.60	+3.14	+2.65

Accuracy against training step on eight benchmarks: three in-domain coding and five out-of-domain math. — Accuracy against training step. The first three panels are in-domain, the remaining five out-of-domain. Mean over three seeds with ±1 s.d. error bars; the shaded band is the final-quarter window used in the tables.

A first-order proxy beats measured utility at every budget

SOAR measures learning progress directly: it trains a copy of the solver on each group of candidates, evaluates it on held-out problems, and rewards the whole group with the accuracy gain. We reimplemented it on the same stack. Its 20 outer steps cost 109 GPU-hours, roughly what CompassPlay spends on 200 steps, and it trails CompassPlay at every GPU-hour budget. Each SOAR outer step yields only 2 to 4 distinct reward values spread over 256 candidates; CompassPlay gives every admissible candidate its own value.

In-domain and out-of-domain mean accuracy against cumulative GPU-hours for CompassPlay and SOAR. — In-domain and out-of-domain mean accuracy against cumulative GPU-hours (training wall-clock times number of GPUs, excluding evaluation), one point per method and training step.

Lean 4 theorem proving

The same coverage in 93 iterations instead of 150

Conjecture-and-prove self-play on DeepSeek-Prover-V2-7B, with proofs checked by Lean 4 against mathlib4 over a target set of 3323 statements, following the SGS training loop. The metric is cumulative coverage: the fraction of distinct targets ever solved.

A local reference opens a shortcut, and novelty closes it

Here the proposer sees the seed statement, and the reference gradient comes from the seed's own proof. The cosine is maximized when g(x̃) = g_ref, and a renamed copy of the seed reaches exactly that. Plain cos finds the shortcut: its copy rate climbs to 0.96 by iteration 75, and 77.5% of its in-band conjectures are exact renames. Multiplying by the novelty factor gives copies zero reward while keeping them in the batch, so the policy gradient pushes them down. The copy rate falls to zero and the rename rate to 1.0%.

Copy rate against iteration: cos climbs toward 1, cos times novelty falls to zero. — Copy rate: the fraction of each round's in-band training conjectures whose token-Jaccard to their seed exceeds 0.8.

Ablation of cos × novelty at iteration 115. Gain is the mean gain over difficulty in solved problems, averaged over iterations 15 to 115.
Reward	cos	novelty	Copy ↓	Gain ↑
cos × novelty (ours)	✓	✓	0.000	+13.6
cos	✓	×	0.712	+3.1
novelty only	×	✓	0.000	−7.9
difficulty	×	×	0.000	0.0

Both factors are needed. At the same zero copy rate, cos × novelty is ahead of novelty alone at all 101 shared iterations.

Faster coverage at matched GPU-hours

With the novelty-weighted reward, CompassPlay reaches the difficulty baseline's final coverage in 93 iterations rather than 150. It stays ahead of difficulty by 18 problems on average over the shared iterations and ends with the highest coverage of all methods. Per-iteration cost is about the same, so the saving carries onto the cost axis: 40% fewer GPU-hours.

Cumulative coverage against iteration for all Lean methods. — Cumulative coverage of the 3323-statement target set. The dotted line marks the coverage difficulty reaches after 150 iterations.

Cumulative coverage against cumulative GPU-hours. — Cumulative coverage against cumulative GPU-hours (per-iteration wall-clock times 8 GPUs), iterations 0 to 150.

Citation

BibTeX

@article{pu2026compassplay,
  title   = {CompassPlay: Rewarding the Proposer for Where It Moves the Solver},
  author  = {Pu, Sophia Xiao and Sun, Ximeng and Liu, Jiang and Wu, Jialian and
             Barsoum, Emad and Liu, Zicheng and Wang, William Yang},
  journal = {arXiv preprint arXiv:XXXX.XXXXX},
  year    = {2026}
}