PaperlayerView exact revision on arXiv

Source-linked AI summary

From Reasoning Strings to Partial Orders: Verifier-Certified Rule Transport through Quotient Policy Optimization

Bang Xie, Hao Liu, Zhiyuan Peng, Xin Yin, Chenhao Ying, Yuan Luo, Senjian Zhang, Wei Chen

arXiv:2609.27833v1cs.LG

TL;DR

Trajectory-level optimization treats successful traces differing only by commuting steps as separate events, although computations can admit multiple valid orders and indiscriminate order augmentation can reward invalid permutations. VCRT replays adjacent operation pairs with native verifiers, using certified legal swaps to form trajectory orbits and anti-diamonds to separate dependency violations. Across the three LOEO folds, VCRT gains 13.06 points (CI [12.58, 13.54]) over the strongest matched baseline; Lean contributes most of the improvement.

  • Problem

    Trajectory-level optimization treats successful traces differing only by commuting steps as separate events, although computations can admit multiple valid orders and indiscriminate order augmentation can reward invalid permutations.

    Source: §1 · p. 1

  • Method

    VCRT replays adjacent operation pairs with native verifiers, using certified legal swaps to form trajectory orbits and anti-diamonds to separate dependency violations.

    Source: §1 · p. 1, Diamonds and Anti-Diamonds · p. 2

  • Results

    Across the three LOEO folds, VCRT gains 13.06 points (CI [12.58, 13.54]) over the strongest matched baseline; Lean contributes most of the improvement.

    Source: §9 · p. 7

  • Takeaways & Limitations

    The evidence favors verifier-certified dependency separation as the transferable component, while leaving the general benefit of exact orbit-mass optimization unresolved.

    Source: §7 · p. 6, §9 · p. 7

    Evidence covers compact backbones, three structured environments, and a shared greedy-evaluation interface; longer traces, larger models, and less formal environments remain outside the reported evidence.

    Source: §8 · p. 7

Abstract

from arXiv · show

Many computations admit several valid execution orders because independent subgoals or disjoint state updates can commute. Reinforcement learning with verifiable rewards usually treats each successful trace as a separate token sequence, so serialization choices can be mistaken for logical dependencies. We introduce Verifier-Certified Rule Transport (VCRT), which replays adjacent operation pairs with native verifiers. Pairs whose two orders are accepted and reach the same canonical state provide commutation certificates; rejected or state-changing reversals provide anti-diamonds. VCRT uses anti-diamonds to preserve genuine prerequisites and assigns policy credit to the total probability mass of each certified orbit. It also constrains post-swap consistency, source retention, and policy drift. We evaluate leave-one-environment-out transfer across ProofWriter, CLRS, and Lean through a shared anonymized relation-graph interface. All training and checkpoint decisions are frozen before held-out evaluation, which uses one greedy trajectory per item without search or verifier feedback. VCRT obtains a 77.60% macro pass rate versus 64.53% for the strongest matched baseline, a paired gain of 13.06 points (95% bootstrap CI [12.58, 13.54]). Lean accounts for most of this gain at 33.49 points, while ProofWriter and CLRS improve by 2.85 points on average. Mechanism tests consistently favor anti-diamond supervision, whereas No-Orbit is statistically indistinguishable from full VCRT. The evidence does not establish a general benefit from exact orbit aggregation.

1 Introduction

Successful reasoning traces can differ in serialization even when their operations are independent, but indiscriminate order invariance can also reward invalid reversals. VCRT uses native verifiers to distinguish certified commutations from prerequisites and transfers policy credit across certified reorderings.

1 Introduction

  • Trajectory-level optimization treats successful traces that differ only by commuting steps as separate events, while indiscriminate order augmentation risks rewarding invalid permutations.The underlying computation may admit several valid orders even though autoregressive generation emits one token order.Source: §1 · p. 1
  • VCRT replays adjacent operation pairs with native verifiers, treating accepted orders with the same canonical terminal state as diamonds and rejected or state-changing reversals as anti-diamonds.ProofWriter, CLRS, and Lean provide the native rule engine, state transitions, and proof kernel, respectively.Source: §1 · p. 1
  • The method forms verifier orbits from successful traces connected by certified swaps and applies a quotient policy objective to orbit probability mass, with constraints on anti-diamond separation, post-swap consistency, source retention, and policy drift.The policy receives an anonymized relation graph while native states, verdicts, versions, and provenance remain in a sealed certificate view.Source: §1 · p. 1
  • The evaluation trains on two reasoning environments and tests once on the third after methods, run configurations, and checkpoints are frozen; unrestricted-text dependency extraction is outside scope.Source: §1 · p. 1
  • 13.06 points: VCRT gains over the strongest matched baseline in frozen leave-one-environment-out evaluation, with positive replication on Granite-4.1-3B and source decline below one point.No-Anti underperforms full VCRT in each held-out fold; the benefit of exact orbit aggregation remains environment-dependent.Source: §1 · p. 2

2 Related Work

Related work spans reasoning traces and search, verifier-based policy optimization, partial-order and policy equivalence, and executable reasoning environments. VCRT distinguishes itself through verifier-certified swaps and matched dependency violations, rather than cross-domain contrastive learning itself.

Reasoning traces, search, and tools

  • Prior trace, self-consistency, self-training, and search methods broaden executable traces, while VCRT defines training-time equivalence only after verifier certification and uses one greedy trace at inference.The passage cites Chain-of-thought and related methods.Source: §2 · p. 2

Reinforcement learning with verifiable rewards

Policy equivalence and partial-order semantics

  • Partial-order reduction and policy quotients offer formal precedents, but VCRT treats reasoning equivalence as instance-dependent and certifies each local swap and terminal state before joining trajectories.The passage cites trace semantics, MDP equivalence (Givan, Dean, and Greig 2003; Li, Walsh, and Littman 2006; van der Pol et al. 2020), and POMO.Source: §2 · p. 2

Cross-domain and contrastive reasoning optimization

  • VCRT’s novelty claim is limited to verifier-grounded equivalence construction and a quotient ratio; its closest policy-optimization precedent is cross-domain contrastive optimization, but the supervision objects differ.VCRT uses verifier-certified swaps as positives and matched dependency violations as negatives.Source: §2 · p. 2

Executable reasoning environments

  • ProofWriter, CLRS, and Lean serve as certifiers of local state transitions, while the learned policy receives a shared anonymous relation interface rather than environment-private states.The passage places these systems among prior executable theorem-proving, logic, algorithmic, and proof-state work, with cited markers including Tafjord, Dalvi, and Clark 2021; Veličković et al. 2022; Yang et al. 2023; and de Moura and Ullrich 2021.Source: §2 · p. 2

3 Problem Formulation

A partial order specifies prerequisite relations among operations, while a generated trajectory is one linear extension. Because the learner is not given the order directly, VCRT uses native execution certificates to identify supported swap relations and verifier-equivalent trajectories.

Partial Orders and Linearizations

  • A complete trajectory is a linear extension when it contains each operation once and respects the partial order; adjacent swaps of incomparable operations preserve legal linearizations.Repeated adjacent swaps connect all linear extensions of the same finite partial order, but VCRT defines only the component supported by native swap certificates.Source: Partial Orders and Linearizations · p. 2

Diamonds and Anti-Diamonds

  • A reasoning diamond requires accepted transitions in both orders, preserved canonical action signatures, and equal canonical terminal states; rejected, precondition-violating, or nonequivalent reversals form anti-diamonds.When exactly one complete order is accepted, the pair certifies precedence.Source: Diamonds and Anti-Diamonds · p. 2
  • Verifier-equivalence connects successful trajectories through adjacent certified swaps, so matching final answers alone is insufficient without replay evidence for every connecting swap.Source: Diamonds and Anti-Diamonds · pp. 2–3
  • In Lean, independent sibling subgoals can form a reasoning diamond, whereas reversing an action that depends on an unproved lemma is rejected and certifies that prerequisite.Source: Diamonds and Anti-Diamonds · p. 3

4 Verifier-Certified Rule Transport

VCRT turns native replay evidence into certified equivalences and prerequisite distinctions, then allocates policy credit over certified orbits under auxiliary constraints.

4 Verifier-Certified Rule Transport

  • The audit view retains native execution and provenance, while the policy receives only anonymized pointers and typed relations without verifier outcomes or environment identifiers.All methods receive the same policy view.Source: Certificate and Policy Views · p. 3
  • A positive certificate requires accepted transitions in both orders, matching adapted operation signatures, and identical frozen canonical terminal hashes; a reversal rejected or reaching a distinct hash forms an anti-diamond.Ambiguous correspondence, nondeterministic replay, missing provenance, and checker-version disagreement are excluded.Source: Certificate Construction · p. 3
  • For verified orbit O, VCRT sums complete class mass, making credit invariant to the sampled representative while rewarding alternatives in proportion to their probability rather than uniformly.Singleton failures retain the ordinary trajectory ratio; a sampled subset would require separate estimator and approximation analysis.Source: Exact Orbit Mass · pp. 3–4
  • The objective combines orbit policy loss and anti-diamond separation with constraints for post-swap commutation, source retention, and action-level KL.These terms shape probability allocation within the checker-fixed orbit partition; the constraints are augmented-Lagrangian penalties.Source: Dependency Separation and Constraints · p. 5, Optimization Semantics · p. 5
  • Native replay constructs training supervision, but held-out inference uses one anonymous-input pointer sequence scored once, without test-time search, repair, or verifier-guided resampling.During training, certificates determine which successes share an orbit and which reversals receive the anti-diamond penalty.Source: Optimization Semantics · p. 5

5 Experimental Design

The experimental design tests transfer by withholding an entire reasoning environment, freezing training and checkpoint decisions, and evaluating once under a shared relation interface.

5 Experimental Design

  • Each LOEO fold trains on two of ProofWriter, CLRS, and Lean and withholds the third; five schemas with 500 episodes each yield 5,000 source episodes and 120,000 replayed trajectories per fold.Held-out tasks, labels, reference traces, and verdicts are unavailable during training and model or checkpoint selection.Source: §5 · p. 5, Table 1 · p. 5
  • The transfer target is reuse of commutation, precedence, and conflict decisions through a shared relation vocabulary, not recovering those relations from raw source language.Action identifiers are renumbered and environment names are absent from the policy record.Source: §5 · p. 5
  • The primary backbone is Qwen3.5-2B, trained with LoRA for 400 updates; update 400 is the paper checkpoint.The specified setup uses rank 64, scale 128, dropout 0.05, and learning rate 5×10−6.Source: §5 · p. 5
  • Outcome-GRPO, Canonical-GRPO, and VCRT share the backbone, episode order, update count, and checkpoint schedule; Canonical-GRPO controls for VCRT’s anonymous relation interface.No-Orbit and Shuffled-Orbit probe orbit credit, while a dedicated No-Anti ablation removes the anti-diamond margin.Source: §5 · p. 5
  • After checkpoints are frozen, each held-out item receives one temperature-zero greedy trajectory, with no search, repair, reranking, retrieval, self-consistency, or verifier feedback.The native checker scores the final trajectory.Source: §5 · p. 5
  • The paired bootstrap resamples item-level score differences, while run means, fold means, and equal-weight environment macro averages are reported separately.The stronger baseline is prespecified by three-fold macro average; source retention is measured against the matched frozen backbone.Source: §5 · p. 6

6 Results

The matched comparison favors VCRT, while the component tests more clearly support anti-diamond supervision than exact orbit aggregation. Replication is positive across backbones, with source-task decline remaining limited.

6 Results

  • VCRT gains 13.06 macro pass-rate points over Canonical-GRPO (95% CI [12.58, 13.54]).Fold gains are 33.49 points on Lean, 2.11 on ProofWriter, and 3.59 on CLRS; ProofWriter and CLRS improve by 2.85 points on average. Lean's held-out score is 100%, but five four-operation sibling-goal schemas may impose a ceiling, and two of nine fold-by-run comparisons are negative.Source: Transfer under the Shared Interface · p. 6
  • No-Anti is worse in every environment, while No-Orbit is statistically indistinguishable from full VCRT on average.Singleton ratios change the macro result by less than one point; shuffled-orbit effects vary across environments, and the evidence favors learning illegal orders more clearly than redistributing credit among legal orders.Source: Mechanism and Ablations · p. 6
  • 17.57 points (95% CI [16.35, 18.83]) is the three-fold paired gain on Granite-4.1-3B.Granite gains are 36.36 points on Lean, 9.96 on ProofWriter, and 6.40 on CLRS; both backbones improve in every held-out direction. Qwen's largest source-task decline is 0.96 points, and training consumes 376.55 aggregate GPU hours.Source: Retention, Robustness, and Compute · p. 6

7 Discussion

The matched gain supports the complete VCRT objective beyond the shared relational interface, but does not identify which bundled component accounts for it. The clearest ablation evidence favors anti-diamond supervision, while exact orbit aggregation has no stable average advantage.

7 Discussion

  • The 13.06-point macro gap over Canonical-GRPO supports the bundled VCRT objective beyond the shared relation interface, not any single isolated component.The comparison does not assign the full gain to orbit credit, anti-diamond separation, commutation consistency, retention, or KL control.Source: §7 · pp. 6–7
  • Removing the anti-diamond margin lowers results in every held-out fold, but does not isolate its effect from commutation and retention terms.The evidence supports dependency separation more consistently than other components of the bundled objective.Source: §7 · p. 6, Table 3 · p. 7
  • No-Orbit is 0.58 points above full VCRT with an interval including zero, while Shuffled-Orbit loses on Lean and CLRS but gains on ProofWriter.The ablations do not show a stable average advantage for exact orbit aggregation.Source: §7 · p. 6, Table 3 · p. 7
  • Held-out scores come from one temperature-zero trajectory without search or verifier feedback, consistent with learning portable dependency relations rather than exploring more orders.Certified commutations expand the supervised success event during optimization, not the inference budget.Source: §7 · p. 6
  • Two of nine fold-by-run comparisons are negative, and the five four-operation Lean schemas may impose a ceiling on that fold.The 100% Lean score therefore cannot distinguish strong transfer from ceiling saturation in this setting.Source: §7 · pp. 6–7
  • The evidence covers transfer through a shared pre-certified relation interface; unrestricted-language dependency extraction and unrelated input modalities remain outside scope.Source: §7 · p. 7

8 Limitations and Broader Impact

The evidence is bounded by deterministic verifiers, supplied certified relation graphs, compact backbones, and three structured environments. Checker errors can propagate across updates, motivating independent validation and certificate-error reporting.

Verifier and representation scope

  • VCRT requires deterministic verifiers and supplied certified relation graphs, so the experiment tests use of verified dependencies rather than their induction from raw text.Dependency extraction from unrestricted text lies outside the experiment.Source: §8 · p. 7

Scale and external validity

  • Evidence covers compact backbones, three structured environments, and four-operation episodes; longer traces, larger models, and less formal environments remain outside the reported scope.The evaluation uses a shared greedy-evaluation interface.Source: §8 · p. 7

Reproducibility essentials

  • Reproduction requires the frozen five-by-500 schema construction, all 24 candidate orders, update-400 checkpoints, matched item pairing, and fixed backbone, verifier, and canonicalizer versions.Source: §8 · p. 7

Broader impact

  • A checker error can be reused across updates and propagate beyond one trajectory, so deployments should validate checkers independently and report certificate error rates.Source: §8 · p. 7

9 Conclusion

Across the three leave-one-environment-out folds, VCRT gains 13.06 points over the strongest matched baseline, with Lean contributing most. The conclusion favors verifier-certified dependency separation as transferable while leaving exact orbit-mass optimization unresolved.

9 Conclusion

  • 13.06 points (95% CI [12.58, 13.54]) is VCRT’s gain over the strongest matched baseline across the three LOEO folds.Source: §9 · p. 7
  • No-Anti is worse in every held-out fold, whereas replacing orbit aggregation with singleton ratios does not reduce the macro score.Source: §9 · p. 7
  • The evidence favors verifier-certified dependency separation as the transferable component but leaves exact orbit-mass optimization unresolved.Source: §9 · p. 7

Related papers

Loading 2609.27833v1…