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

arXiv: https://arxiv.org/abs/2610.14402 · HTML: https://mlsanity.com/paper/2610.14402/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Reinforcement learning for reasoning, one of 17 directions in LLM reasoning.
- Builds on 29 of its 61 references that are in the map.
- First posted on arXiv 9 Oct 2026.

## Placed in

- LLM reasoning / [Reinforcement learning for reasoning](https://mlsanity.com/lr/reinforcement-learning-for-reasoning/)

## Builds on (most cited first, 29 of 29)

- [Proximal Policy Optimization Algorithms](https://mlsanity.com/paper/1707.06347/) (2017)
- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [Direct Preference Optimization: Your Language Model is Secretly a Reward Model](https://mlsanity.com/paper/2305.18290/) (2023)
- [DAPO: An Open-Source LLM Reinforcement Learning System at Scale](https://mlsanity.com/paper/2503.14476/) (2025)
- [HybridFlow: A Flexible and Efficient RLHF Framework](https://mlsanity.com/paper/2409.19256/) (2024)
- [AGIEval: A Human-Centric Benchmark for Evaluating Foundation Models](https://mlsanity.com/paper/2304.06364/) (2023)
- [Self-Play Fine-Tuning Converts Weak Language Models to Strong Language Models](https://mlsanity.com/paper/2401.01335/) (2024)
- [ReTool: Reinforcement Learning for Strategic Tool Use in LLMs](https://mlsanity.com/paper/2504.11536/) (2025)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Transformers as Soft Reasoners over Language](https://mlsanity.com/paper/2002.05867/) (2020)
- [Self-Play Preference Optimization for Language Model Alignment](https://mlsanity.com/paper/2405.00675/) (2024)
- [ReClor: A Reading Comprehension Dataset Requiring Logical Reasoning](https://mlsanity.com/paper/2002.04326/) (2020)
- [ZebraLogic: On the Scaling Limits of LLMs for Logical Reasoning](https://mlsanity.com/paper/2502.01100/) (2025)
- [CLUTRR: A Diagnostic Benchmark for Inductive Reasoning from Text](https://mlsanity.com/paper/1908.06177/) (2019)
- [SatLM: Satisfiability-Aided Language Models Using Declarative Prompting](https://mlsanity.com/paper/2305.09656/) (2023)
- [NPHardEval: Dynamic Benchmark on Reasoning Ability of Large Language Models via Complexity Classes](https://mlsanity.com/paper/2312.14890/) (2023)
- [CFBench: A Comprehensive Constraints-Following Benchmark for LLMs](https://mlsanity.com/paper/2408.01122/) (2024)
- [Enigmata: Scaling Logical Reasoning in Large Language Models with Synthetic Verifiable Puzzles](https://mlsanity.com/paper/2505.19914/) (2025)
- [AR-LSAT: Investigating Analytical Reasoning of Text](https://mlsanity.com/paper/2104.06598/) (2021)
- [BoardgameQA: A Dataset for Natural Language Reasoning with Contradictory Information](https://mlsanity.com/paper/2306.07934/) (2023)
- [The Choice of Divergence: A Neglected Key to Mitigating Diversity Collapse in Reinforcement Learning with Verifiable Reward](https://mlsanity.com/paper/2509.07430/) (2025)
- [On-Policy RL with Optimal Reward Baseline](https://mlsanity.com/paper/2505.23585/) (2025)
- [SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulas](https://mlsanity.com/paper/2505.14615/) (2025)
- [AutoLogi: Automated Generation of Logic Puzzles for Evaluating Reasoning Abilities of Large Language Models](https://mlsanity.com/paper/2502.16906/) (2025)
- [Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation](https://mlsanity.com/paper/2502.06563/) (2025)
- [P-FOLIO: Evaluating and Improving Logical Reasoning with Abundant Human-Written Reasoning Chains](https://mlsanity.com/paper/2410.09207/) (2024)
- [MCP-Solver: Integrating Language Models with Constraint Programming Systems](https://mlsanity.com/paper/2501.00539/) (2024)
- [HardcoreLogic: Challenging Large Reasoning Models with Long-tail Logic Puzzle Games](https://mlsanity.com/paper/2510.12563/) (2025)

## Abstract (arXiv)

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.