Diverse Reasoning Paths Matter: Symbolic Equivalence Augmentation for Enhancing RL Exploration

1 Introduction

• The paper investigates an underexplored question: whether reasoning-path diversity during SFT supports downstream RLVR, beyond problem-level factors such as task diversity.Prior work found that high SFT accuracy does not reliably yield high RL performance, while exploration is more important.Source: §1 · p. 1
• Existing paraphrasing and rejection-sampling methods mainly vary wording or phrasing, not the underlying reasoning strategy needed to test the paper’s hypothesis.The authors distinguish step-level reasoning diversity from surface-level lexical variation.Source: §1 · p. 1
• EquivAug uses equivalence transformations to generate diverse, verifiable reasoning paths, with structurally distinct intermediate steps that preserve the same conclusion.For example, distributivity can transform a(b+c) into ab + ac.Source: §1 · pp. 1–2
• The study examines CoT diversity at SFT and downstream RLVR performance, finding diverse and correct SFT data significantly improve RL outcomes; to the authors’ knowledge, this is the first empirical establishment of the connection.Source: §1 · p. 2
• EquivAug with GRPO outperforms all baseline methods across benchmarks and model scales from 1.5B to 8B; diverse CoT improves RLVR, while surface-level diversity does not.The experiments use GSM8K and FOLIO with an identical post-training process.Source: §1 · p. 2

2.1 The Interplay between SFT and Reinforcement Learning

• Earlier work examines how SFT shapes exploration and RL performance, but primarily studies problem-level factors rather than reasoning-path diversity for a fixed problem set.The cited work includes findings that SFT can broaden exploration and that task diversity or difficulty can matter more than SFT accuracy.Source: §2.1 · p. 2

2.2 Data Augmentation for Reasoning

• Solution augmentation includes paraphrasing, which preserves the underlying strategy, and sampling, whose correct final answers do not guarantee valid intermediate reasoning.Question-focused approaches instead increase problem complexity or rewrite questions from multiple perspectives.Source: §2.2 · p. 2
• EquivAug combines equivalence-preserving symbolic transformations with solver-based verification to produce reasoning paths that are structurally diverse and provably correct at every intermediate step.The work builds on neuro-symbolic augmentation approaches.Source: §2.2 · p. 3

3 Motivation and Problem Definition

• When all sampled responses to a prompt are correct or all are incorrect, their normalized advantages vanish, leaving GRPO without a gradient for that prompt.GRPO derives advantages by normalizing rewards within a group of sampled responses.Source: §3 · p. 3
• A narrow SFT policy can produce homogeneous responses or no correct response on hard problems, while multiple reasoning strategies make mixed-reward groups more likely.Such groups help keep informative advantage signals available during training.Source: §3 · p. 3
• The hypothesis is that diverse SFT reasoning paths broaden initial policy coverage, supporting more effective exploration and stronger downstream RLVR performance.The problem is to generate paths that differ in reasoning steps while preserving correctness.Source: §3 · p. 3
• Equivalent Solution Augmentation seeks multiple reasoning paths per question that retain the original answer and differ from one another in reasoning structure.The dataset represents each example with a question, reasoning path, and final answer.Source: §3 · p. 3

4.1 Overview

• EquivAug converts CoT to symbolic forms, derives equivalent variants, verifies them with a symbolic solver, and reconstructs them as natural-language training data.The resulting augmented data is used for SFT before GRPO.Source: §4.1 · pp. 3–4, Figure 1 · p. 4

4.2 Symbolic Representation

• For math problems, step-level algebraic expressions form an AST with numbers and variables at leaves and arithmetic operators at internal nodes.The expressions can be executed and checked against the gold answer; the tree supports transformations on subtrees.Source: §4.2 · p. 4
• For FOLIO, premises and conclusions are converted into theorem-prover inputs, with Prover9 or Mace4 used to verify labels and obtain proof traces.Prover9’s search can produce different valid traces for semantically equivalent formula forms.Source: §4.2 · pp. 4–5

4.3 Equivalence Transformation

• Math rewrites alter expression structure while preserving value; logical rewrites and premise reordering preserve entailment while prompting distinct derivations.The libraries include algebraic rules and logical equivalences, while varied Prover9 resolution settings and clause-selection heuristics change its search.Source: §4.3 · p. 5, Table 1 · p. 5, Table 2 · p. 5

4.4 Natural Language Reconstruction

• A language model translates each transformed symbolic path into fluent natural-language CoT, with prompting designed to keep the text aligned to symbolic steps.The complete prompt template is in Appendix C.3.Source: §4.4 · pp. 5–6

5.1 Experiment Settings

• Experiments use GSM8K and FOLIO, three backbone models, mean accuracy over five runs, and RPD from five sampled SFT solutions per test instance.GRPO uses exact-match final-answer reward, and the compared augmentation methods share post-training configurations.Source: §5.1 · p. 6

5.2 Diversity of Generated Paths (RQ1)

• EquivAug yields higher RPD than corresponding baselines in nearly all settings, whereas paraphrasing largely changes wording and RFT paths tend to cluster around learned patterns.An RFT exception on Qwen2.5-1.5B for FOLIO scores 0.4998, which the authors attribute mainly to unstable output styles rather than genuine reasoning diversity.Source: §5.2 · p. 7

5.3 Post-training RL with Diverse SFT (RQ2)

• EquivAug achieves the highest ACCGRPO across model scales and datasets, while Table 3 reports RPD, ACCSFT, and ACCGRPO for each augmentation method.The experiments compare augmentation strategies under the same post-training configurations.Source: §5.3 · p. 7, Table 3 · p. 8
• ρ = 0.87 on GSM8K, ρ = 0.67 on FOLIO, and ρ = 0.77 overall describe positive rank correlations between SFT RPD and post-GRPO accuracy.EquivAug is not consistently the strongest method by SFT accuracy, but surpasses baselines after GRPO; the authors connect this to higher output entropy preserving a broader policy distribution for exploration.Source: §5.3 · p. 7

5.4 Ablation and OOD Generalization (RQ3)

• On GSM8K with Qwen2.5-1.5B, both RPD and downstream accuracy peak at K = 5 augmented solutions, while transformation complexity 1 performs best.More solutions reduce RPD without improving performance, and too many sequential transformations degrade accuracy, possibly because paths become unnatural or structurally strange.Source: §5.4 · p. 8, Figure 2 · p. 8
• On SVAMP and MATH500 after training Qwen2.5-1.5B on GSM8K, EquivAug achieves the best post-RL accuracy: 76.13 on SVAMP and 36.68 on MATH500.The authors report transfer to a distribution-shifted arithmetic benchmark and a more challenging mathematical benchmark.Source: §5.4 · p. 8, Figure 3 · p. 8

• Across GSM8K and FOLIO and multiple model scales, EquivAug produces more diverse reasoning paths after SFT and stronger performance after GRPO.Source: §6 · p. 9
• EquivAug generates structurally diverse, provably correct paths through equivalence-preserving transformations and solver-based verification.Source: §6 · p. 9
• The paper concludes that reasoning-step diversity, rather than surface-level lexical variation, is key to preparing an effective policy foundation for RLVR.Source: §6 · p. 9

• EquivAug’s equivalence-rule libraries are manually designed from established mathematical and logical identities.The rules suffice for meaningful diversity in the current evaluation domains; automatic discovery, learning, or expansion remains future work.Source: Limitations · p. 9
• Experiments cover models from 1.5B to 8B parameters, leaving the persistence of gains at larger scales open.Source: Limitations · p. 9
• The authors identify studying the interplay between reasoning diversity and model capacity at larger scales as future work.Source: Limitations · p. 9

A Theorem Prover: Prover9

• For TRUE instances, a refutation of C establishes Premises |= C; for FALSE instances, a refutation of ¬C establishes Premises |= ¬C.Source: A Theorem Prover: Prover9 · p. 11
• For UNCERTAIN instances, Mace4 constructs models satisfying Premises ∪ {C} and Premises ∪ {¬C}, confirming that the premises do not determine C’s truth value.Source: A Theorem Prover: Prover9 · p. 11

B Algorithm

• Algorithm 1 presents pseudocode for EquivAug.Source: B Algorithm · p. 11

C.1 Configurations

• SFT trains for 3 epochs, using full-parameter fine-tuning for Qwen2.5-1.5B and Qwen2.5-3B and LoRA for Llama-3.1-8B.Learning rates are 2e-5 for full fine-tuning and 2e-4 for LoRA; the other shared settings include AdamW, weight decay 0.01, cosine scheduling, batch size 16, and BF16.Source: §C.1 · p. 11
• GRPO uses binary exact-match correctness rewards, 8 rollouts per prompt, and 3 epochs for GSM8K or 10 for Folio.The setup uses a 1e-6 learning rate, KL penalty coefficient β = 0.0005, sampling temperature 0.7, and the original training sets.Source: §C.1 · p. 11
• Both SFT and RL use a Metamath-adopted prompt template with instruction and response placeholders.Source: §C.1 · p. 11

C.2 Metric: RPD

• RPD averages each step’s minimum cosine distance to the steps in the longer solution, matching from the shorter solution to the longer one.A higher score indicates greater strategic divergence; the paper uses Qwen-3-embedding-8B for step embeddings.Source: §C.2 · pp. 11–12

C.3 Prompt Template

• For GSM8K, the templates convert a natural-language solution into one arithmetic expression and then write a solution following a new equivalent expression.The expression-reconstruction prompt expands intermediate results into their original subexpressions while preserving operations and order.Source: §C.3 · p. 12
• For FOLIO, templates turn formal proofs into natural-language explanations that trace why a conclusion is true, false, or uncertain.The prompts request explanations in natural prose and specify the corresponding verdict line.Source: §C.3 · pp. 12–13

D.1 Accuracy Trends

• EquivAug starts with lower accuracy but learns more effectively during GRPO and soon outperforms the other methods.Figure 4 reports test accuracy trends for Llama3.1-8B on GSM8K.Source: Figure 4 · p. 13, §D.1 · p. 13

D.2 Entropy

• EquivAug has the highest entropy among methods, which the authors interpret as evidence of better exploration.Figure 5 shows entropy during GRPO training.Source: §D.2 · p. 13, Figure 5 · p. 13
• Entropy decreases during GRPO training; the authors suggest this may explain RFT’s lowest entropy, describing RFT as a weak version of RL without advantages and negative samples.The RFT explanation is presented as a possible reason, not a demonstrated cause.Source: §D.2 · p. 13