SAGE combines algebraic sparsification and hyperbolic structural guidance to curb long-horizon reasoning biases, beating baselines across 12 benchmarks and 7 model families with up to 8-fold gains on Andrews-Curtis
Synopsis
The work introduces Symbolic Closure Analysis (SCA) to characterize exploration bias and compounding bias in long-horizon reasoning, and builds SAGE, a framework that injects structural priors during post-training via algebraic sparsification and hyperbolic structural guidance, outperforming SFT, GRPO, EMPO, and GRPO-PRM across 12 benchmarks and 7 model families and achieving up to an 8-fold improvement in Lean-verified proofs on the open Andrews-Curtis task.
Interpretation
The paper proposes Symbolic Closure Analysis (SCA), modeling long-horizon reasoning as sequences of locally admissible transformations and characterizing two biases through a prefix-closed feasible region: exploration bias from structural complexity and compounding bias from sparse rewards. Prior work often attributes long-horizon failure to task difficulty or reward sparsity; SCA formalizes it as feasible support diluted by high-volume unproductive branches and as local deviations accumulating with depth under terminal-only rewards. The paper provides Definition 3.1, Remarks 3.2 and 3.3, the variance decomposition in Proposition 3.4, and the total-variation bound in Theorem 3.5 on reference anchoring under rare terminal rewards, with proofs in Appendix B.
SAGE translates the SCA diagnosis into two training-time structural guidances: algebraic sparsification projects locally admissible candidates onto operator-indexed subspaces to suppress spurious branching, and hyperbolic structural guidance embeds reasoning states into a negatively curved space to supply dense depth-wise signals. Unlike methods relying on dense process labels or learned verifiers, SAGE's structural potentials require no process labels or ground-truth solution paths and add no inference-time search or filtering. The paper gives Proposition 4.1 on non-vanishing structural advantage under sparse rewards and Proposition 4.2 on guidance-induced feasible-support concentration, with a greedy sparse locator recovery theorem under coherence in Appendix C and a soft concentration bound in Appendix D.
Across 12 benchmarks and 7 model families, SAGE consistently outperforms SFT, GRPO, EMPO, and GRPO-PRM; the 35B SAGE variant reaches 64.86 average accuracy, exceeding Llama-3.3-70B-Instruct at 38.48. Gains span closed-form mathematical reasoning, free-form natural reasoning, and open long-horizon symbolic reasoning, surpassing a larger flagship model at roughly half the parameters. Tables 1 and 2 report averages at 2B, 9B, 27B, and 35B scales; Appendix H provides five-seed mean-standard deviations; Appendix E states all compared methods use the same rollout budgets, decoding constraints, and KL coefficient.
On the open Andrews-Curtis long-horizon task, SAGE reaches AC Validity 59.83, AC Path Solving 31.76, and Lean-Verified Proofs 23.69, with Qwen3 showing nearly an 8-fold increase over base. Ablations show that removing either algebraic sparsification or hyperbolic guidance reduces AC Validity and Lean-Verified success, and replacing hyperbolic with Euclidean distance or shuffling target anchors also weakens performance. Tables 3 and 4 present component ablations and controls; the AC task uses 1190 constructed group presentations, with Lean-verified proofs as the gold-standard end-to-end rigor metric.
Perspective
The results target post-training for long-horizon reasoning under sparse rewards, applying to symbolic tasks with a local admissibility interface and, in mathematical and free-form reasoning, to settings where residuals, anchors, and operator subspaces are approximated by learned proxies. For teams seeking to reduce process-annotation dependence while requiring end-to-end rigor verification, SAGE offers a path that injects structural priors at training time with zero extra inference cost; Appendix E states all structural modules are used only during post-training, with inference using the trained policy directly.
SCA's theoretical concentration results apply directly to symbolic settings, while in mathematical and free-form reasoning they depend on whether learned proxies separate productive from unproductive prefixes, a fidelity that is empirical. Structural prior quality depends on the task interface, and Appendix J notes more automatic prior construction and tighter non-symbolic guarantees remain open. SAGE also adds training-time overhead from candidate-step scoring, residual probing, and hyperbolic distance computation, though inference adds no cost. The paper reports five-seed mean-standard deviations, but variance sources and stability across benchmarks and model scales merit reader scrutiny alongside Appendix H.
