Language models trained to solve logic problems using symbolic tools
SAT-RL: Training Language Models for Logical Reasoning with Symbolic Solvers
Artificial IntelligenceSymbolic Computation
Summary
Large language models can solve many math and logic puzzles but struggle with very complex ones. Symbolic solvers can handle complex reasoning but don’t understand natural language. The authors created SAT-RL, a way to train language models to work together with symbolic solvers by practicing multi-step problem solving. This method helps the models solve more difficult logic problems both similar to and different from their training. Their work shows how combining smart language understanding with precise symbolic tools improves reasoning.
What this means in practice
- •For software engineers: Integrate trained language models with symbolic solvers to automate complex logic verification tasks in software development.
- •For system architects: Design hybrid AI systems combining language models and symbolic solvers for scalable reasoning in formal verification and constraint solving.
Authors
Jialiang Sun, Kuldeep Meel
Abstract
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.