arXiv：cs.AI· Jialiang Sun, Kuldeep Meel·· 10 小时前
SAT-RL：用符号求解器训练语言模型做逻辑推理
SAT-RL: Training Language Models for Logical Reasoning with Symbolic Solvers
AI 导读
SAT-RL 是一个强化学习框架，让 LLM 通过多轮工具调用与 Z3 等可满足性求解器交互，结合可验证合成数据、求解器增强轨迹的监督预热和工具感知奖励的强化学习。实验显示，该方法在域内与域外逻辑任务上均显著提升了模型的符号推理能力，代码已开源。
正文
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 this https URL.
| Subjects: | Artificial Intelligence (cs.AI); Symbolic Computation (cs.SC) |
| Cite as: | arXiv:2610.14402 [cs.AI] |
| (or arXiv:2610.14402v1 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2610.14402 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Jialiang Sun [view email]
[v1]
Fri, 9 Oct 2026 23:46:15 UTC (2,106 KB)
来源：arXiv：cs.AI · arxiv.org