ANCORA: Learning to Question via Manifold-Anchored Self-Play for Verifiable Reasoning
For researchers in automated reasoning and code generation, this provides a method for self-improvement in verifiable domains, though it is domain-specific and incremental over existing self-play approaches.
ANCORA introduces a self-play framework where a language model generates verifiable problems, solves them, and uses feedback for self-improvement without human supervision, achieving 81.5% pass@1 on Dafny2Verus (up from 26.6% SFT baseline) and outperforming PSV by 15.8 points.
We propose a paradigm shift from learning to answer to learning to question: can a language model generate verifiable problems, solve them, and turn the resulting feedback into self-improvement without human supervision? We introduce ANCORA, an anchored-curriculum framework in which a unified policy alternates between a Proposer that synthesizes novel specifications and a Solver that produces verified solutions. ANCORA rests on three load-bearing mechanisms: a two-level group-relative update that couples Proposer advantages across specifications with Solver advantages across solution attempts; iterative self-distilled SFT that projects the base model onto its valid-output manifold before RL; and a UCB-guided Curriculum DAG that grows only through strictly filtered, novel, Solver-verified specifications. These stabilizers are necessary because sparse verifier feedback otherwise drives Proposer collapse even under MLRL-aligned rewards. Instantiated in Verus, ANCORA lifts Dafny2Verus pass@1 from a 26.6% SFT baseline to 81.5% in the test-time-training setting under 0-shot evaluation, outperforming the PSV self-play baseline by 15.8 points despite PSV using 1-shot inference; in a separate transfer setting, training from Dafny2Verus seeds yields 36.2% and 17.2% pass@1 on held-out MBPP and HumanEval.