arXiv cs.AI· Jialiang Sun, Kuldeep Meel·· 3 天前AI 评分30
SAT-RL：用符号求解器训练语言模型进行逻辑推理
SAT-RL: Training Language Models for Logical Reasoning with Symbolic Solvers
AI 导读
SAT-RL 是一个强化学习框架，通过多轮工具执行训练 LLM 与 Z3 等符号求解器交互，结合可验证合成数据、求解器增强轨迹的监督预热和工具感知奖励的求解器接地 RL。实验显示，SAT-RL 在域内和域外逻辑任务上均大幅提升了带工具符号推理能力，代码已开源。
正文 · 原文
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