Rewarding Novel Deductions: Solver-guided Process Supervision for Logical Reasoning
Authors: Muhammad Asif Ali, Wenqing Wang, Huan Wang, Mohammad Raza
Organizations: FORTE Lab, Faculty of Science, Information Technology University, Lahore, Pakistan · College of Informatics, Huazhong Agricultural University, Wuhan, China · Qatar Computing Research Institute, Hamad Bin Khalifa University, Doha, Qatar
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.
Figures & tables
Figure 1: Illustration of Spring using a ZebraPuzzle example. Natural-language clues are converted into solver-checkable syntactic clues, interleaved reasoning steps are classified by the solver, and the resulting signals are mapped to process rewards for training.
LLM
System
ZebraLogic
AR-LSAT (Acc.)
Knights and Knaves
Puzzle Acc. ↑
Cell Acc. ↑
Ordering ↑
Grouping ↑
Assignment ↑
Overall ↑
Puzzle Acc. ↑
Person Acc. ↑
Qwen3-1.7B
Base-NL
11.14
35.04
16.07
24.48
0.00
13.52
53.28
64.43
OR-NL
38.57
49.87
19.64
40.81
1.44
20.63
68.57
79.64
Base-INT
31.85
41.45
23.21
24.48
14.49
20.73
18.71
55.61
OR-INT
36.00
46.09
35.71
51.02
24.63
37.12
73.57
80.54
Logic-LM
12.85
33.16
-.-
-.-
-.-
15.58
3.57
22.51
Table 1: Spring performance comparison across different LLMs on ZebraLogic, AR-LSAT, and Knights and Knaves.
System
Puzzle Acc. ↑
Solved traces
Failed traces
SAT-rate ↑
Steps ↓
Parsed / Total ↑
Valid / Parsed ↑
Steps ↓
Parsed / Total ↑
Valid / Parsed ↑
Contradictions / 100 Steps ↓
--N
61.42
0.941
35.20
0.460
0.988
49.10
0.384
0.824
6.77
--NC
66.14
0.814
34.82
0.347
0.953
11.23
0.305
0.912
2.52
Spring
73.71
0.965
22.37
0.492
0.996
9.39
0.495
0.991
0.46
Table 2: Reasoning-trace quality across three reward settings for Qwen3-4B-Thinking. Solved traces are averaged over correctly solved cases, while Failed traces are averaged over incorrect cases.
Appendix figures & tables10 assets
Supplementary material from the paper’s appendix.
Appendix
House
Person
Pet
Drink
1
Alice
Dog
Coffee
2
Bob
Cat
Tea
3
Carol
Fish
Juice
Appendix
Table 4
Dataset
Category / Split
Train
Validation
Test
Notes
ZebraLogic
Small
80
12
224
1000 total puzzles
Medium
67
12
196
Large
52
13
138
Extra-Large
51
13
142
Total
250
50
700
AR-LSAT
Ordering
300
50
112
Official test split
Appendix
Table 3: Data statistics for ZebraLogic, AR-LSAT, and Knights and Knaves.
Category
#Samples
Cell-Acc.
SAT-rate
#Novel-steps
Puzzle Acc.
Small
224
0.941
0.924
2.81
0.915
Medium
196
0.922
0.908
4.66
0.888
Large
138
0.882
0.884
4.92
0.783
Extra-Large
142
0.405
0.641
2.08
0.204
Appendix
Table 4: Spring performance aggregated by puzzle category using the predefined size groups. These results are reported using Qwen3-4B-Thinking.
Category
Size
#Samples
Cell Acc.
SAT-rate
#Novel-steps
Puzzle Acc.
Small
2x2
23
1.000
0.957
0.96
1.000
2x3
27
1.000
1.000
2.15
1.000
2x4
31
0.935
0.871
2.84
0.935
2x5
26
0.904
0.923
2.96
0.846
2x6
29
0.877
0.828
2.83
0.793
3x2
33
0.970
0.939
3.24
0.970
Appendix
Table 5: Test metrics by inferred puzzle size. The puzzle size is extracted from pid as A×B, and each size is mapped to a predefined difficulty category. All results are obtained using Qwen3-4B-Thinking.
Figure 2: Z3 Solver SAT-rate across training epochs.
Category
#Total
#Correct
#Incorrect
Error Rate
Small
224
205
19
0.085
Medium
196
174
22
0.112
Large
138
108
30
0.217
X-Large
142
29
113
0.796
Appendix
Table 6: Error analysis with respect to puzzle size for ZebraLogic benchmark. Error count refers to instances with Puzzle Acc.=0 .
Reason
#Total
Small
Medium
Large
X-Large
Solver-Consistent
84
6
6
16
56
Missing output
40
11
11
1
17
Header Mismatch
34
1
4
8
22
Solver-Inconsistent
25
1
1
5
18
Format Failure
9
0
0
0
9
Appendix
Table 7: Statistics of incorrect cases for ZebraLogic benchmark. Counts are computed over instances with Puzzle Acc.=0 .
Reason
Key signals
1-line prediction snippet
Observation
Missing output
Cell Acc. =0 , SAT =0 , Puzzle Acc. =0
WRONG OUTPUT FORMAT
The model returns no usable prediction at all, so the failure is caused by blank or unextractable output rather than reasoning.
The output remains solver-consistent, but duplicated attribute assignments across houses make it non-exact.
Solver-Inconsistent
SAT =0 , Puzzle Acc. =0
houses 1–2 both use Mother=Holly, Child=Alice, Animal=cat
SAT=0 . Many local assignments are plausible, but repeated values violate the global one-to-one puzzle constraints.
Format Failure
Format_Check=False
Header has 7 fields, but each predicted row contains only 6 values
The output has the shape of a table, but every row is missing one attribute column, so evaluation collapses to zero matched cells.
Appendix
Table 8: Different types of Error Cases for ZebraLogic Benchmark.
Puzzle ID
System
Puzzle Acc.
SAT
#Steps
#Parsed
#Valid
#Contradictions
4x5-16
Spring
1.0
1.0
22
11
11
0
--N
0.0
1.0
85
40
22
18
--NC
0.0
1.0
144
34
31
3
4x6-0
Spring
1.0
1.0
20
10
10
0
--N
0.0
1.0
88
42
26
16
--NC
0.0
0.0
0
0
0
0
Appendix
Table 9: Case study on shared puzzles with Spring compared against ( --N ) and ( --NC ) variants. We used Qwen3-4B-Thinking for this analysis.
System
Parsed-only reasoning trace
Outcome
Spring
(1) House 2 = Eric; (2) Eric → colonial; (3) House 3 = lilies; (4) House 1 = Arnold; (5) Arnold → roses; (6) Therefore House 4 = lilies; (7) …
Exact solution; short, contradiction-free trace.
--N
(1) House 2 = Eric; (2) Eric → colonial; (3) House 2 = Arnold; (4) Arnold → lilies; (5) House 4 = lilies; (6) House 1 = Eric; (7) …
Solver-consistent but duplicated assignments.
--NC
(1) House 2 = Eric; (2) Eric → colonial; (3) House 1 = Arnold; (4) Arnold → colonial; (5) House 3 = lilies; (6) House 4 = lilies; (7) …
Long, noisy trace with repeated attributes.
Appendix
Table 10: Case study on a matched puzzle. We compare the parsed-only reasoning traces produced by Spring , --N , and --NC on the same puzzle. We used Qwen3-4B-Thinking for this analysis.
Chain-of-thought (CoT) prompting can fail severely on constraint-dense logical reasoning tasks, where unverified errors accumulate silently across steps. We introduce SymStep: an LLM makes one atomic claim at a time (DEDUCE: Alice, pet, Cat), then a lightweight constraint propagator checks the claim for consistency with prior accepted deductions, rejects contradictions, and cascades implied facts automatically. SymStep+G additionally provides MRV guidance after each accepted step, directing the LLM toward the most constrained unresolved variable. On a 35-puzzle retained subset of ZebraLogicBench, a benchmark of 1,000 Einstein-style logic puzzles, Direct and CoT both achieve 0%, while SymStep+G reaches 97%. On AR-LSAT analytical reasoning problems, SymStep achieves 100% vs. CoT's 87%. On LGP-14, SymStep+G achieves 100% vs. 0% for CoT and Logic-LM, the strongest prior symbolic+LLM baseline we compare against. Ablation studies reveal that MRV guidance is a key mechanism for reducing directionless cycling, while consistency checking provides a safety net against explicit contradictions. Across six benchmarks spanning five task domains, SymStep variants match or exceed every baseline on constraint-dense and arithmetic tasks. Experiments on AQUA-RAT algebra confirm the advantage is constraint-density-specific.
Aida Usmanova, Rui Gao, Dilshod Azizov +2
Leuphana University of Lüneburg · Mohamed bin Zayed University of Artificial Intelligence
While LLMs demonstrate impressive reasoning capabilities, they remain fragile in multi-step logical deduction, where a single transition error can propagate through the entire reasoning chain, leading to unstable performance. In this work, we identify logical connectives as primary points of this structural fragility. Through empirical analysis, we show that connective tokens function as high entropy forking points, at which models frequently struggle to determine the correct logical direction. Motivated by this observation, we hypothesize that intervening in logical connective selection can guide LLMs toward more correct logical direction, thereby improving the overall reasoning chain. To validate this hypothesis, we propose a multi-layered framework that intervenes specifically at these logic-critical junctions in the reasoning process. Our framework includes (1) Gradient-based Logical Steering to guide LLMs internal representations towards valid reasoning subspaces, (2) Localized Branching to resolve ambiguity via targeted look-ahead search, and (3) Targeted Transition Preference Optimization, a surgical reinforcement learning objective that selectively optimizes single-token preferences at logical pivots. Crucially, by concentrating intervention solely on logic-critical transitions, our framework achieves a favorable accuracy--efficiency trade-off compared to global inference time scaling methods like beam search and self-consistency.
Seunghyun Park, Yuanyuan Lei
Independent Researcher · University of Florida Gainesville, FL, United States
Large Language Models (LLMs) still struggle with multi-step logical reasoning. Existing approaches either purely refine the reasoning chain in natural language form or attach a symbolic solver as an external module. In this work, we instead ask whether LLMs contain a shared internal logical subspace that simultaneously aligns natural-language and symbolic-language views of the reasoning process. Our hypothesis is that this logical subspace captures logical reasoning capabilities in LLMs that are shared across views while remaining independent of surface forms. To verify this, we employ Canonical Correlation Analysis on the paired residual activations from natural-language and symbolic-language reasoning chains, learning a low-dimensional subspace with maximum cross-view correlation. Furthermore, we design a training-free approach that steers LLMs reasoning chain along this logical subspace, thereby leveraging the complementary reasoning signals from both views. Experiments on four logical reasoning benchmarks demonstrate the effectiveness of our approach, improving accuracy by up to 11 percentage points and generalizing well on out-of-domain problems.
Feihao Fang, My T. Thai, Yuanyuan Lei
University of Illinois Urbana-Champaign, Champaign, IL · Computer & Information Science and Engineering, University of Florida, Gainesville, FL