PaperlayerView exact revision on arXiv

Source-linked AI summary

SAT-RL: Training Language Models for Logical Reasoning with Symbolic Solvers

Jialiang Sun, Kuldeep Meel

arXiv:2610.14402v1cs.AIcs.SC

TL;DR

LLMs struggle with logical problems as constraints and search spaces grow, while solver-coupled approaches motivate training that coordinates language models with symbolic tools. SAT-RL trains LLMs to plan and refine solver calls using synthetic data and solver-grounded rewards. It improves in-domain logical reasoning and generalizes to unseen out-of-domain benchmarks, outperforming base LLMs and ReTool baselines.

  • Problem

    LLM accuracy degrades as constraint counts and search spaces grow, and symbolic checking reveals constraint violations and gaps between reasoning rationales and verifiable correctness.

    Source: §1 · p. 1

  • Method

    SAT-RL trains LLMs to plan and iteratively refine symbolic-solver calls, integrating synthetic data with solver interactions and verifiable rewards for answer correctness and formula quality.

    Source: §1 · p. 1, §3.4 · p. 5, §5 · p. 8

  • Results

    SAT-RL improves in-domain logical reasoning and generalizes to unseen out-of-domain benchmarks, outperforming base LLMs and ReTool baselines.

    Source: §5 · p. 8

  • Takeaways & Limitations

    SAT-RL combines accurate logical reasoning with faithful solver use within the evaluated in-domain and unseen out-of-domain benchmarks.

    Source: §5 · p. 8

    The study focuses on logical reasoning and a fixed set of widely used symbolic solvers; broader program synthesis and open-ended natural-language reasoning remain unexplored.

    Source: Limitations · p. 9

Abstract

from arXiv · show

Large language models (LLMs) have achieved strong performance in mathematical and logical reasoning, yet they still suffer from the curse of complexity and struggle as problem difficulty increases with the number of constraint interactions and the size of the search space. In contrast, satisfiability solvers such as Z3 provide scalable and verifiable reasoning through constraint solving under formal theories, but lack the flexibility to interpret natural-language problem descriptions. In this work, we propose SAT-RL, a reinforcement-learning (RL) framework that trains LLMs to interact with symbolic solvers through multi-turn tool execution. SAT-RL leverages synthetic data generation with verifiable solutions, supervised warm-up on solver-augmented traces, and solver-grounded reinforcement learning with tool-aware rewards. Experiments show that SAT-RL substantially improves symbolic reasoning with tools on both in-domain and out-of-domain logic tasks. Our code is available on https://github.com/sunjia72/SAT-RL.

1 Introduction

LLMs struggle as logical problems grow in constraints and search space, while symbolic solvers offer scalable, verifiable deductions but cannot flexibly interpret natural language. SAT-RL trains LLMs to plan and refine solver calls through synthetic-data warm-up and solver-grounded reinforcement learning.

  • LLM accuracy drops as constraint counts and search spaces grow, with symbolic checking linking degradation to constraint violations and gaps between rationales and verifiable correctness.Source: §1 · p. 1
  • Symbolic solvers scale to large combinatorial spaces and provide reliable deductions, but existing solver-coupled systems operate only at inference time and remain vulnerable to program errors and encoding misalignment.Prior systems also offer limited means of aligning solver encodings with original problem constraints.Source: §1 · p. 1
  • SAT-RL trains LLMs to plan and iteratively refine symbolic-solver calls through synthetic-data warm-up and reinforcement learning with verifiable rewards and instance-conditioned tool sampling.The warm-up uses synthetic logic data with ground-truth solvers and verifiers for supervised fine-tuning.Source: §1 · pp. 1–2

2 Related Work

Prior work spans natural-language inference, formal validity, and generated constraint puzzles, alongside prompting, solver-coupling, and reinforcement-learning approaches to logical reasoning.

2.1 Benchmarks for Logical Reasoning

  • Logical-reasoning benchmarks cover passage-based inference, relational induction, formal validity and entailment, generated constraint puzzles, and multi-step test suites.Examples include LogiQA and ReClor, FOLIO and Rule-Taker, SAT-Bench and Enigmata, and LogicBench and Multi-LogiEval.Source: §2.1 · p. 2

2.2 Logical Reasoning with LLMs

  • LLM approaches include CoT, ToT, and self-consistency prompting, plus solver systems ranging from one-shot SATLM queries to MCP-Solver's iterative constraint construction and validation (Ye et al., 2023; Szeider, 2024).Source: §2.2 · p. 2
  • RL methods for reasoning include PPO, DPO, GRPO, policy-gradient variants, self-play preference training, and DAPO's long-horizon training refinements.Source: §2.2 · p. 2

3 Methods

SAT-RL combines solver-grounded data generation, supervised warm-up, and reinforcement learning with multi-turn tool execution. Its methods formalize logical queries, construct verifiable training data, and reward both answer correctness and solver-call quality.

3.1 Preliminaries

  • SAT-RL formalizes each natural-language reasoning instance as a theory, variables, constraint formula, and query, supporting decision, solving, and counting tasks.The theory specifies the semantics of the symbols and predicates, while satisfying models assign values to the variables that meet the constraints.Source: §3.1 · p. 3

3.2 Data Generation and Processing

  • Synthetic-Logic covers 16 task families with solver-grounded traces; SAT-Bench supplies controlled-difficulty RL puzzles, and Enigmata provides out-of-distribution evaluation.The synthetic set contains 1,399 verifiable instances after timeout removal, split into 1,260 training and 139 test instances.Source: §3.2 · p. 4

3.3 Supervised Fine-tuning

  • Supervised fine-tuning warms up the policy on prompts paired with target responses containing valid solver programs, teaching tool use and reducing early invalid executions.The stated warm-start skills include solver-tool API usage, planning, and coding.Source: §3.3 · p. 4

3.4 Reinforcement Learning

  • Reinforcement-learning rewards combine response format, answer correctness, tool compilability, and equivalence between proposed and ground-truth formulas.The policy is encouraged to abstain under uncertainty, while incorrect answers are penalized; on SAT-Bench's yes/no tasks, uniform random guessing is strictly suboptimal in expectation.Source: §3.4 · pp. 5–6
  • DAPO trains the SFT-initialized policy from sampled completion groups while rollouts interleave model reasoning, executable solver calls, and returned tool feedback.The tool interface places reasoning, tool calls, and responses in sequence before the final answer.Source: §3.4 · pp. 5–6

4 Evaluation

The evaluation tests SAT-RL on in-domain SAT-Bench, out-of-domain Enigmata and AIME 2025, and ablations of its training components. SAT-RL improves SAT-Bench and Enigmata accuracy, with more limited gains on AIME 2025.

4 Evaluation

  • The evaluation uses proprietary models and 4B- and 9B-parameter Qwen3.5 variants, comparing SAT-RL with ReTool across three runs.The in-domain test uses SAT-Bench; Enigmata and AIME 2025 assess out-of-domain generalization.Source: §4 · pp. 6–7

4.1 RQ 1: In-Domain Performance

  • SAT-Bench accuracy reaches 97.2% for SAT-RL Qwen3.5-9B, above Claude Sonnet 5 (93.0%) and ReTool-trained Qwen3.5-9B (83.5%).SAT-RL Qwen3.5-4B reaches 85.4%, up from 19.8%, outperforming the larger ReTool-trained Qwen3.5-9B model.Source: §4.1 · p. 7, Table 4 · p. 7

4.2 RQ 2: Out-of-Domain Generalization

  • Enigmata overall accuracy rises from 33.9% to 59.9%, with gains across all seven categories and the easy, medium, and hard subsets.SAT-RL accuracy reaches 100.0% on Crypto and 82.8% on Logic.Source: §4.2 · p. 7, Table 5 · p. 8
  • On AIME 2025, Avg@8 accuracy rises from 86.7% (208/240) to 88.3% (212/240), while both models solve 28/30 problems.The authors characterize the mathematical-reasoning gains as limited but non-negative under this configuration.Source: §4.2 · p. 7

4.3 RQ 3: Ablation Studies

  • Removing SFT drops SAT-Bench accuracy from 97.2% to 54.9%; removing equivalence checking lowers it to 91.2%, while removing tool sampling routes over 99% of calls to Z3.Without equivalence checking, only 80.6% of solver calls have formula encodings equivalent to ground truth, and rollouts show reward-hacking behavior; without tool sampling, Enigmata accuracy is 52.7%.Source: §4.3 · p. 8

5 Conclusion

SAT-RL integrates synthetic data and symbolic solver interaction into LLM training. Experiments report improved in-domain reasoning and generalization to unseen out-of-domain benchmarks, outperforming base LLMs and ReTool baselines.

5 Conclusion

  • SAT-RL integrates synthetic data and symbolic solver interaction into LLM training for accurate logical reasoning and faithful solver use.Source: §5 · p. 8
  • Experiments report improved in-domain reasoning and generalization to unseen out-of-domain benchmarks, outperforming base LLMs and ReTool baselines.Source: §5 · p. 8
  • Table 6 reports in-domain final-answer accuracy and encoded-formula logic-equivalence rates for Qwen3.5-9B ablations; TS denotes Tool Sampling.Source: Table 6 · p. 8
  • Figure 3 tracks logic-equivalence on SAT-Bench; in its “w/o Logic Equivalence” ablation, requiv is computed but excluded from the training reward.Source: Figure 3 · p. 8
  • Figure 4 compares symbolic solver usage distributions with tool sampling enabled versus disabled.Source: Figure 4 · p. 8

Limitations

The study is limited to logical reasoning and a fixed set of widely used symbolic solvers; broader domains remain to be explored.

Limitations

A Components of the Enigmata Test Set

The appendix reports Enigmata test-set instance counts grouped by difficulty, puzzle category, and puzzle name.

A Components of the Enigmata Test Set

B Hyperparameter Settings

The appendix provides the SFT and RL training configurations and reports that Qwen3.5-9B training on SAT-Bench takes around 24 hours.

B Hyperparameter Settings

B.1 Description of Synthetic Puzzles

The appendix describes synthetic puzzles spanning graph, numeric, automata, neural-network, and grid constraints, then gives prompt templates for SAT-Bench and other settings.

B.1 Description of Synthetic Puzzles

  • Graph puzzles include clique selection, feedback-vertex removal, K-coloring, thresholded Max Cut and TSP, and set covering.The tasks respectively seek a target-size clique, an acyclic remainder, a valid coloring or cut, a threshold-feasible tour, or a small covering family.Source: §B.1 · pp. 12–13
  • Set packing and integer puzzles ask for disjoint subsets, an equal-sum partition, or a subset matching a target sum.Their parameters include the prescribed packing size, item array, and target or implied half-total.Source: §B.1 · p. 13
  • Other synthetic tasks include fixed-length accepting paths in NFAs and inputs that flip a threshold-gate BNN within a Hamming ball.The NFA instance specifies states, alphabet, transitions, start and accepting states; the BNN instance specifies a seed and radius.Source: §B.1 · p. 13
  • Grid puzzles cover partial N-Queens, generalized Sudoku, magic squares, Latin squares, and Futoshiki with neighboring-cell inequalities.These tasks combine pre-filled cells or clues with row, column, sub-block, diagonal, or nonattacking constraints as applicable.Source: §B.1 · p. 13

C Prompt Templates

  • The SAT-Bench prompt template supplies a problem statement, variable mapping, and sampled solver for the model to use.It asks for step-by-step solving and a final answer in the specified format.Source: C Prompt Templates · pp. 13–14
  • The other-settings template is used in training and evaluation, requests a formatted final answer, and permits “idk” when tool-supported evidence is insufficient.It includes the problem statement and asks the model to solve step by step.Source: C Prompt Templates · p. 14

D OR-Tools Example

The appendix provides an OR-Tools example that models an integer constraint and searches for all solutions, then notes that solved examples appear later.

D OR-Tools Example

  • A solution callback counts each solution, and the solver searches for all solutions before printing the count.The callback can also print solutions when configured to do so.Source: D OR-Tools Example · p. 14
  • The example defines nonnegative integer variables x and y, each bounded from 0 to 50, and imposes 4x + 6y = 50.The bounds are described as potentially loose.Source: D OR-Tools Example · p. 14

E Solved Examples

E.1 Solved SAT-Bench Example

The examples show solver-assisted reasoning across SAT-Bench and Enigmata, including an equivalent SAT-Bench formula and correction of an initial UNSAT formulation to produce a verified Enigmata board satisfying the stated constraints.

E.1 Solved SAT-Bench Example

  • Z3 returned sat, establishing that all four experimental conditions can be simultaneously satisfied and the answer is yes.Source: §E.1 · p. 15
  • The reward scores were format 0.1, correctness 1.0, tool_success 0.1, and equivalence 1.0.Source: §E.1 · p. 15
  • The extracted formula omits one ground-truth clause but is reported logically equivalent, and the response contains a correctly parsed answer and compilable Z3 call.Source: §E.1 · p. 15

E.2 Solved Enigmata Example

  • The initial PySAT attempt returned “Unsolvable,” leading the model to suspect an adjacency-constraint modeling error and retry.Source: §E.2 · p. 17
  • The final answer presents the verified board between the required <begin_board> and <end_board> tags.The board is `.XX.X*.` / `.XX*.X.` / `*XX.XXX` / `..*....` / `....XX*` / `.*X.XXX` / `....*..`.Source: §E.2 · p. 18
  • The solver’s final board places stars in columns (5, 3, 0, 2, 6, 1, 4) by row and is verified as satisfying the puzzle constraints.The solution has exactly one star per row and column, uses empty cells, and separates stars in adjacent rows by more than one column.Source: §E.2 · pp. 17–18
  • The first PySAT formulation returned UNSAT despite the task’s unique-solution premise, so the model corrected the formula and obtained a satisfying solution.The initial encoding added at-least-one clauses for each row; the corrected result was confirmed by the verifier.Source: §E.2 · p. 18

F Additional Training Trajectories

Figure 5 presents additional SAT-Bench training trajectories for two Qwen3.5 model sizes, covering reward components, test correctness, and entropy.

F Additional Training Trajectories

Loading 2610.14402v1…