CompassPlay 用梯度对齐奖励自博弈 proposer，在 Lean 证明中以更少 GPU 时间达到相同覆盖

CompassPlay 重新设计 self-play 中 proposer 的奖励：不只奖励“题目有多难”，而是根据候选任务与目标 reference tasks 的 solver gradient alignment 衡量其训练价值。论文在 Lean 4 theorem proving 中报告，达到 difficulty baseline 150 次迭代的累计覆盖时，CompassPlay 可节省约 40% GPU-hours。