PaperlayerView exact revision on arXiv

Source-linked AI summary

Rewarding Novel Deductions: Solver-guided Process Supervision for Logical Reasoning

Muhammad Asif Ali, Wenqing Wang, Huan Wang, Mohammad Raza

arXiv:2609.34660v2cs.CL

TL;DR

LLMs can struggle to keep multi-step logical deductions consistent, while many approaches emphasize final-answer correctness over intermediate reasoning. SPRING uses solver feedback during training to reward novel, logically useful deductions and penalize contradictory or uninformative steps. Across three benchmarks and four LLMs, it consistently outperforms base models, outcome-only reward baselines, and Logic-LM.

  • Problem

    LLMs struggle with structured logical reasoning that requires precise constraint tracking and consistent multi-step deduction, while many existing approaches provide limited supervision of intermediate reasoning.

    Source: §1 · pp. 1–2

  • Method

    SPRING uses a symbolic solver during reinforcement learning to assess intermediate steps for novelty and logical consistency, then uses that feedback to reward useful deductions and penalize contradictory or uninformative ones.

    Source: §1 · p. 2

  • Results

    Across three benchmarks and four LLMs, SPRING consistently outperforms base LLMs, outcome-only reward baselines, and Logic-LM; ZebraLogic puzzle-accuracy gains reach 49.71 points over the base LLM and 15.43 over the strongest outcome-only baseline.

    Source: §1 · p. 2

  • Takeaways & Limitations

    Analyses report shorter and cleaner successful reasoning traces, fewer contradictions, and greater consistency with underlying logical constraints.

    Source: §6 · p. 10

    If parsed premises are incomplete, incorrect, or solver-incompatible, rewards become less informative because verification assesses reasoning against the constructed solver state rather than the original problem.

    Source: D Limitations · p. 21

Abstract

from arXiv · show

Logical reasoning remains a major challenge for large language models (LLMs), particularly on structured problems that require precise constraint tracking, consistency preservation, and multi-step deduction. This challenge is especially acute for small-scale LLMs, which are more prone to producing inconsistent, redundant, or brittle reasoning trajectories. Existing approaches for improving logical reasoning largely optimize for final-answer correctness, providing only weak supervision over the intermediate reasoning process. In this work, we propose SPRING: (Solver-guided Process Rewards for Novel LogIcal ReasoNing Step Generation). SPRING uses SMT solver as a training-time verifier of intermediate reasoning steps to provide process-level supervision. It introduces the notion of a novel reasoning step, namely, a step that is logically valid, consistent with the evolving reasoning state, and not already implied by previously accepted non-contradictory deductions. Based on this solver-based assessment, it designs process rewards that encourage novel inferential progress while penalizing contradictory and uninformative reasoning steps. Evaluation across three logical reasoning benchmarks, ZebraLogic, AR-LSAT, and Knights and Knaves, and four LLMs shows that SPRING consistently outperforms base LLMs, outcome-only reward baselines, and Logic-LM. On ZebraLogic, SPRING improves puzzle accuracy by up to 49.71 and 15.43 points over the base LLM and strongest outcome-only baseline, respectively. On AR-LSAT, it improves overall accuracy by up to 64.93 and 12.14 points, respectively. On Knights and Knaves, SPRING achieves up to 93.14 puzzle accuracy and 96.05 person accuracy.

1 Introduction

The introduction identifies weak supervision of intermediate deductions as a gap in logical reasoning training and presents SPRING, which uses solver feedback to reward novel, useful steps. It reports improved results across three benchmarks and four LLMs.

1 Introduction

  • LLMs, especially small-scale models, struggle to maintain sound, consistent, and informative multi-step deductions, with traces often redundant, unsupported, or contradictory.The introduction notes that models in the 4B-and-below regime often need stronger or more structured supervision to maintain coherent reasoning trajectories.Source: §1 · pp. 1–2
  • Prior solver-augmented methods mainly use solvers after formalization, while many training approaches optimize final-answer correctness rather than intermediate reasoning quality.The introduction argues that identical answers can arise from trajectories that differ in validity, informativeness, contradiction, or redundancy.Source: §1 · p. 2
  • SPRING uses a solver during reinforcement learning to identify novel, valid, state-consistent deductions and reward useful progress while penalizing contradictions and uninformative steps.A novel step is not already implied by previously accepted non-contradictory deductions.Source: §1 · p. 2
  • SPRING improves ZebraLogic puzzle accuracy by up to 49.71 points over the base LLM and 15.43 over the strongest outcome-only baseline, and outperforms baselines across three benchmarks.The evaluation uses four LLMs and also reports up to 64.93- and 12.14-point gains on AR-LSAT over the base and strongest outcome-only baseline, respectively.Source: §1 · p. 2

2 Related Work

Related work uses symbolic solvers to support structured reasoning, often through formalization followed by inference or consistency checking. SPRING differs by using solver feedback to supervise intermediate reasoning during learning.

2 Related Work

  • Solver-augmented methods pair LLM formalization with symbolic deduction or consistency checks, a design suited to structured tasks with global constraints and combinatorial dependencies.AR-LSAT and ZebraLogic exemplify the challenge of structured deduction and increasing deductive complexity [Zhong et al., 2022, Lin et al., 2025].Source: §2 · pp. 2–3
  • SatLM, Logic-LM, LINC, and LTRAG use formal representations with solver inference, refinement, theorem proving, or retrieval-augmented exemplars [Ye et al., 2023; Pan et al., 2023a; Olausson et al., 2023; Hu et al., 2025].The passage reports gains for Logic-LM, LINC, and LTRAG on logical reasoning benchmarks, including AR-LSAT, FOLIO, and comparisons with prior methods.Source: §2 · p. 3
  • Formalization quality can bottleneck solver-augmented reasoning: inaccurate executable translations limit downstream accuracy and prevent the solver from recovering the intended reasoning process.Lam et al. [2024] report that translation quality varies across symbolic tools and is tied to downstream reasoning accuracy.Source: §2 · p. 3
  • SPRING uses the solver during reinforcement learning to evaluate intermediate steps for novelty, validity, and consistency, then converts feedback into process rewards.This contrasts with prior methods that primarily use solvers for downstream inference or final-answer verification.Source: §2 · p. 3

3 Problem Formulation

The problem formulation represents a logical task as premises and domain constraints, then trains a policy to generate a solution alongside natural-language and formal reasoning steps. It defines step properties used to assess validity, novelty, contradiction, and consistency with the final solution.

3 Problem Formulation

  • A problem instance combines natural-language premises or clues with domain constraints, and the model generates a reasoning trajectory followed by a final solution.Each step pairs a natural-language rationale with an optional formal statement executable in Z3.Source: §3 · p. 3
  • The base theory Γbase combines domain constraints Γdom with premises C, and the training objective seeks intermediate formal steps that are both valid and novel.The model policy generates interleaved natural-language and formal reasoning steps.Source: §3 · p. 3, §3.1 · p. 4

3.1 Core Definitions

  • Strong implication excludes vacuous implication under inconsistency, while a valid step is entailed by the base theory and remains consistent with it.The definitions test satisfiability with the step and unsatisfiability with its negation.Source: §3.1 · p. 4
  • A novel step is valid but neither tautological nor already implied by accepted non-contradictory steps, and it is not equivalent to an original premise.Tautological steps follow from domain constraints alone and provide no problem-specific progress.Source: §3.1 · p. 4
  • A contradictory step makes the current reasoning state unsatisfiable, meaning it conflicts with premises, domain constraints, or previously accepted non-contradictory deductions.The contradiction test adds the generated step to the current context.Source: §3.1 · p. 4
  • A trajectory is consistent with the final solution when the domain constraints, formal reasoning steps, and predicted solution remain jointly satisfiable.Source: §3.1 · p. 4

4 SPRING

SPRING uses symbolic verification during training to supervise intermediate logical deductions, rewarding inferential progress while discouraging inconsistent or uninformative steps. Its workflow structures model outputs for solver checking and incorporates those checks into reinforcement-learning rewards.

4.1 LLM Prompting and Output Structure

  • Parsed premises, interleaved natural-language and formal reasoning, and a final solution form the model output, with formal steps enabling precise symbolic verification.The parsed premises initialize the solver state before it evaluates the formal deductions.Source: §4.1 · p. 5, §4.2 · p. 5

4.2 Solver Construction and Step Verification

  • The solver checks premise satisfiability and uniqueness, then evaluates steps for validity, tautology, novelty, contradiction, and consistency with the final solution.Novelty measures new inferential content beyond previously accepted reasoning; final-solution consistency checks whether deductions and the prediction can coexist in a satisfiable theory.Source: §4.2 · pp. 5–6

4.3 Process-Level Reward

  • The reward combines solver-derived novelty, contradiction, and final-solution consistency signals with formatting, parseability, and final-answer accuracy.Process-level rewards apply when the parsed-premise system is satisfiable; otherwise, reward is limited to auxiliary and final-answer quality signals.Source: §4.3 · p. 6

4.4 RL Training

  • SPRING trains with group-based reinforcement learning using GRPO, while a DAPO-style runtime supports sampling and optimization and a frozen reference policy regularizes training.Candidates receive solver-guided scalar rewards, and the policy is encouraged to prefer candidates with better reasoning quality relative to others in the sampled group.Source: §4.4 · pp. 6–7

5 Experimentation

SPRING is evaluated across three logical-reasoning benchmarks and four LLMs, with experiments comparing its results and reasoning traces against baselines and reward ablations. The reported results cover both end-task accuracy and process quality.

5.1 Experimental Settings

  • The evaluation uses ZebraLogic, AR-LSAT, and Knights and Knaves, with four LLMs, outcome-only reward baselines, and Logic-LM as a comparison.ZebraLogic uses a 250/50/700 train/validation/test split; AR-LSAT uses its official 230-instance test set, and KnK uses all 700 test puzzles.Source: §5.1 · p. 7

5.2 Main Results

  • SPRING consistently improves logical reasoning across four LLMs and three benchmarks, outperforming outcome-only reward learning and Logic-LM.Table 1 presents the performance comparison across ZebraLogic, AR-LSAT, and Knights and Knaves.Source: §5.2 · p. 8, Table 1 · p. 8
  • On ZebraLogic, SPRING reaches Puzzle Acc. scores of 54.00, 73.71, 55.71, and 77.85 across the four evaluated LLMs.For Qwen3-1.7B, its 54.00 Puzzle Acc. exceeds OR-NL's 38.57.Source: §5.2 · p. 8
  • Removing the novel-step reward lowers ZebraLogic Puzzle Acc. and AR-LSAT overall accuracy, with the size of the reported reduction varying across models.On ZebraLogic, the reduction ranges from 2.00 to 34.72 points across the four models.Source: §5.2 · pp. 8–9
  • On AR-LSAT, SPRING achieves overall accuracies of 49.26, 73.61, 37.52, and 75.56 across the four LLMs.Removing the novelty reward reduces overall accuracy for all four LLMs.Source: §5.2 · pp. 8–9
  • On Knights and Knaves, SPRING reaches up to 93.14 Puzzle Acc. and 96.05 Person Acc., and removing novelty lowers Puzzle Acc. for all four LLMs.The reported Puzzle Acc. gains over the strongest outcome-only baseline range from 7.86 to 16.00 points across the four LLMs.Source: §5.2 · p. 9

5.3 Ablation Analyses

  • On ZebraLogic, removing novelty reduces Puzzle Acc. and produces longer, less stable traces; removing both novelty and contradiction leaves lower solver consistency and structural reliability than SPRING.SPRING has the highest Puzzle Acc. (73.71), solved-case SAT-rate (0.965), and a contradiction rate of 0.46 per 100 steps; its failed traces average 9.39 steps.Source: §5.3 · pp. 9–10

5.4 Further Analyses

  • Further ZebraLogic analyses examine scaling across puzzle sizes, solver SAT rate across epochs, errors, and qualitative cases; their results are reported in Appendix C.The analyses address behavior under increasing difficulty, solver consistency during training, and reasoning-trace quality.Source: §5.4 · p. 10

6 Conclusion

SPRING uses symbolic verification to supervise intermediate reasoning, and experiments across three benchmarks and four LLMs show it outperforms base LLMs, outcome-only reward baselines, and Logic-LM. Its analyses also report shorter, cleaner successful traces, fewer contradictions, and greater consistency with logical constraints.

6 Conclusion

  • Across three benchmarks and four LLMs, SPRING outperforms base LLMs, outcome-only reward baselines, and Logic-LM.The conclusion also reports shorter, cleaner successful traces, fewer contradictions, and greater consistency with logical constraints.Source: §6 · p. 10
  • SPRING rewards novel, logically consistent deductions and penalizes contradictory and uninformative steps, supervising reasoning trajectories rather than only final-answer correctness.The framework uses symbolic verification to provide process-level supervision.Source: §6 · p. 10

A Background

  • The benchmarks cover complementary tasks: globally constrained assignments, text-centric ordering, grouping and assignment, and truth-conditional reasoning about characters.ZebraPuzzles require complete assignments, AR-LSAT asks questions over textual rule systems, and Knights and Knaves assigns truth-telling identities.Source: A Background · p. 13, §A.2 · p. 14, §A.3 · p. 15

A.1 ZebraPuzzles

  • ZebraPuzzles require unique assignments satisfying clue-derived and global one-to-one constraints, making intermediate deductions amenable to symbolic validity and consistency checks.The example distinguishes a valid deduction, a contradiction, and a novel deduction not already implied by accepted steps.Source: §A.1 · pp. 13–14

A.2 AR-LSAT

  • In the AR-LSAT example, “A must be first” is valid, while “B must be second” is a novel deduction from combining Rules 1 and 3.The benchmark includes ordering, grouping, and assignment problems that require reasoning over textual rules.Source: §A.2 · pp. 14–15

A.3 Knights and Knaves

  • Knights and Knaves can be encoded with Boolean identity variables and constraints; in the example, assuming A is a knight leads to a contradiction detected through C’s statement.Each knight’s statement must be true, while each knave’s statement must be false.Source: §A.3 · pp. 15–16

B.1 Evaluation Benchmarks

The evaluation uses three benchmarks with complementary training and test splits, and reports task-specific accuracy measures. ZebraLogic distinguishes complete-puzzle accuracy from cell-level accuracy, while Knights and Knaves also reports person-level accuracy.

B.1 Evaluation Benchmarks

  • The evaluation covers 1,000 ZebraLogic puzzles with 250/50/700 train/validation/test instances, balanced AR-LSAT training and validation sets, and the official 230-instance AR-LSAT test split.Knights and Knaves uses 300 sampled training puzzles for reinforcement learning and the complete 700-puzzle test set.Source: §B.1 · p. 16

B.2 Evaluation Metrics

  • ZebraLogic reports Puzzle Acc. for fully correct assignments and Cell Acc. for individual assignments, which gives partial credit for some correct cells.A puzzle counts as correct under Puzzle Acc. only when all predicted cells match the ground truth.Source: §B.2 · pp. 16–17
  • AR-LSAT reports accuracy separately for Ordering, Grouping, and Assignment problems, as well as overall accuracy across its test instances.Source: §B.2 · p. 17
  • Knights and Knaves reports Puzzle Acc., requiring all identities in a puzzle to be correct, and Person Acc. for individual character identities.Person Acc. gives credit at the individual-character level.Source: §B.2 · p. 17

C Additional Experimental Results

The additional analyses examine scaling across puzzle sizes, solver SAT-rate across training epochs, errors, and qualitative cases.

C Additional Experimental Results

C.1 Scaling Behavior of SPRING Across Puzzle Sizes

For Qwen3-4B-Thinking, ZebraLogic performance declines as puzzle size grows, with the sharpest drop on X-Large puzzles. The appendix also tracks Z3 solver SAT-rate across training epochs.

C.1 Scaling Behavior of SPRING Across Puzzle Sizes

  • Small puzzles yield 0.941 Cell Acc., 0.924 SAT-rate, and 0.915 Puzzle Acc.; on Medium puzzles, novel reasoning steps average 4.66, up from 2.81 on Small puzzles.On Large puzzles, Puzzle Acc. falls to 0.783 while Cell Acc. and SAT-rate remain relatively stable.Source: Table 4 · p. 17, §C.1 · p. 17
  • On X-Large puzzles, Qwen3-4B-Thinking reaches 0.405 Cell Acc. and 0.204 Puzzle Acc., while SAT-rate remains 0.641.The SAT-rate exceeds Puzzle Acc., indicating partially solver-consistent structures without fully correct solutions.Source: Table 5 · p. 18, §C.1 · p. 18

C.2 Z3-Solve SAT rate across epochs

C.3 Error Analyses

Error rates rise sharply with puzzle size, while incorrect outputs are most often globally satisfiable but differ from the gold solution. Harder puzzles also expose more inconsistency and output-structure failures.

C.3 Error Analyses

  • Only 29 of 142 X-Large puzzles are solved correctly, as the error rate rises from 0.085 on Small and 0.112 on Medium to 0.217 on Large and 0.796 on X-Large puzzles.An error is an instance with Puzzle Acc. = 0.Source: §C.3 · p. 19
  • Solver-Consistent prediction is the dominant error type, with Missing output and Header Mismatch the next major sources of incorrect cases.Table 8 illustrates the different error types.Source: §C.3 · p. 19, Table 8 · p. 19
  • Solver-Inconsistent and Format Failure cases are less frequent overall but become more visible on harder puzzles, alongside the rise in output failures.Source: §C.3 · p. 19

C.4 Qualitative Case study

On shared puzzles, SPRING produces shorter, contradiction-free traces where the ablated variants fail. The case study contrasts its compact deduction chains with repeated consistency violations in those variants.

C.4 Qualitative Case study

  • On shared validation puzzles, SPRING solves instances with fewer steps and zero contradictions, while (–N) and (–NC) fail despite often generating longer traces.Table 9 compares the variants on shared puzzles.Source: §C.4 · p. 19, Table 9 · p. 20
  • SPRING maintains a compact, monotonic deduction chain, whereas (–N) and (–NC) repeatedly violate global consistency through contradictory reassignment or duplicate attribute placement.Table 10 compares parsed-only traces on the same puzzle using Qwen3-4B-Thinking.Source: §C.4 · p. 20, Table 10 · p. 20
  • Baseline traces also show unstable clue propagation, such as assigning the same person or attribute incompatibly across houses.Examples include assigning colonial to both Eric and Arnold or placing lilies in multiple houses; the case study reports improvements in reasoning efficiency and trajectory consistency with SPRING.Source: §C.4 · p. 20

D Limitations

The limitations concern SPRING’s applicability beyond structured logical tasks and the constraints on its AR-LSAT grouping prompts. They include dependence on solver-compatible representations and accurately parsed premises, as well as requirements for interleaved explanations and solver-verifiable steps limited to supported, noncontradictory deductions.

D Limitations

  • SPRING requires premises and deductions that can be reliably translated into solver-compatible symbolic constraints, limiting direct use in open-ended domains.Defining the symbolic interface for such domains may be difficult or introduce parsing errors.Source: D Limitations · pp. 20–21
  • Incomplete, incorrect, or solver-incompatible parsed premises can make the solver state unsatisfiable or semantically inaccurate, weakening downstream process rewards.The verifier assesses reasoning relative to the constructed solver state, not the original natural-language problem.Source: D Limitations · p. 21
  • Solver-verifiable process signals assess validity, novelty, contradiction, and consistency, but omit qualities such as abstraction, explanation quality, and human interpretability.Consequently, the framework may favor solver-compatible reasoning over reasoning that is more concise or natural to people.Source: D Limitations · p. 21

E.2 Prompt Template for AR-LSAT (Grouping Problems)

  • The template alternates natural-language explanations with formal deductions, numbering formal steps sequentially as S<k>.Each reasoning entry must be exactly one sentence; explanations justify the next formal step from rules, facts, earlier steps, or option testing.Source: §E.2 · p. 27
  • Formal steps use a restricted vocabulary for group membership, Boolean relations, counting constraints, and Sat/Unsat option checks.The permitted operators include membership assignments and their negations, logical connectives, counting operators, and option-feasibility checks.Source: §E.2 · pp. 27–28
  • Allowed deductions include forced or excluded group membership, same- or different-group relations, and conditional consequences.The template also permits direct question facts as formal steps.Source: §E.2 · p. 28
  • The template also allows exclusive-choice and counting deductions, plus option feasibility or impossibility checks.Sat means the option can extend to a valid grouping; Unsat means it cannot.Source: §E.2 · p. 28
  • Formal steps must follow from rules, facts, and accepted earlier steps unless they test option feasibility; unsupported, contradictory, tautological, or redundant steps are prohibited.Ordering operators are barred unless the problem specifies ordered groups, and final-answer text cannot serve as a reasoning step.Source: §E.2 · p. 28

Related papers

Loading 2609.34660v2…