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

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

cs.CLSep 28, 2026

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

Abstract

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
LLM	System	Puzzle Acc. $\uparrow$	Cell Acc. $\uparrow$	Ordering $\uparrow$	Grouping $\uparrow$	Assignment $\uparrow$	Overall $\uparrow$	Puzzle Acc. $\uparrow$	Person Acc. $\uparrow$
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. $\uparrow$	Solved traces				Failed traces
System	Puzzle Acc. $\uparrow$	SAT-rate $\uparrow$	Steps $\downarrow$	Parsed / Total $\uparrow$	Valid / Parsed $\uparrow$	Steps $\downarrow$	Parsed / Total $\uparrow$	Valid / Parsed $\uparrow$	Contradictions / 100 Steps $\downarrow$
--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

\texttt{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

\texttt{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.
Header Mismatch	$\texttt{Format\_Check}=\texttt{False}$	header: [House, Name, FavoriteSport] $\rightarrow$ [House, Name, Sport]	Mis-match in header schema output fields.
Solver-Consistent	SAT $=1$ , Puzzle Acc. $=0$	rows: [1, Eric, colonial, lilies], [2, Arnold, colonial, lilies], …	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	$\texttt{Format\_Check}=\texttt{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 $\rightarrow$ colonial; (3) House 3 $\neq$ lilies; (4) House 1 = Arnold; (5) Arnold $\rightarrow$ roses; (6) Therefore House 4 = lilies; (7) …	Exact solution; short, contradiction-free trace.
--N	(1) House 2 = Eric; (2) Eric $\rightarrow$ colonial; (3) House 2 = Arnold; (4) Arnold $\rightarrow$ lilies; (5) House 4 = lilies; (6) House 1 = Eric; (7) …	Solver-consistent but duplicated assignments.
--NC	(1) House 2 = Eric; (2) Eric $\rightarrow$ colonial; (3) House 1 = Arnold; (4) Arnold $\rightarrow$ 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.

Explore similar work

SymStep: Symbolic Step Verification for Logical Reasoning
Jul 25, 2026Aida Usmanova, Rui Gao, Dilshod Azizov +2Constraint Satisfaction Symbol-
Leuphana University of Lüneburg · Mohamed bin Zayed University of Artificial Intelligence
Where Reasoning Breaks: Logic-Aware Path Selection by Controlling Logical Connectives in LLMs Reasoning Chains
Apr 22, 2026Seunghyun Park, Yuanyuan LeiReasoning Chain Reasoning Skills
Independent Researcher · University of Florida Gainesville, FL, United States
Discovering a Shared Logical Subspace: Steering LLM Logical Reasoning via Alignment of Natural-Language and Symbolic Views
Apr 21, 2026Feihao Fang, My T. Thai, Yuanyuan LeiLLM Reasoning Strategies Reasoning Chain
University of Illinois Urbana-Champaign, Champaign, IL · Computer & Information Science and Engineering, University of Florida, Gainesville, FL

Jul 25, 2026, cs.AIJ/K move · Enter open · S save

SymStep: Symbolic Step Verification for Logical Reasoning

Aida Usmanova, Rui Gao, Dilshod Azizov, Ricardo Usbeck+1

Leuphana University of Lüneburg · Mohamed bin Zayed University of Artificial Intelligence

Constraint Satisfaction Symbol-Puzzle Synagent

Open paper AskPDF arXiv

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.

Abstract

Explore similar work

SymStep: Symbolic Step Verification for Logical Reasoning

Where Reasoning Breaks: Logic-Aware Path Selection by Controlling Logical Connectives in LLMs Reasoning Chains

Discovering a Shared Logical Subspace: Steering LLM Logical Reasoning via Alignment of Natural-Language and Symbolic Views