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 在域内和域外逻辑任务上均大幅提升了带工具符号推理能力，代码已开源。
正文 · AI 翻译
摘要：大型语言模型（LLM）在数学和逻辑推理方面已取得强劲表现，但随着问题难度因约束交互数量和搜索空间规模而增加，它们仍受复杂性之困，举步维艰。相比之下，Z3 等可满足性求解器通过形式理论下的约束求解，提供可扩展且可验证的推理，但缺乏解读自然语言问题描述的灵活性。在本工作中，我们提出 SAT-RL，一个强化学习（RL）框架，训练 LLM 通过多轮工具执行与符号求解器交互。SAT-RL 利用具有可验证解的合成数据生成、在求解器增强轨迹上的监督式预热，以及带有工具感知奖励的、以求解器为依据的强化学习。实验表明，SAT-RL 在域内和域外逻辑任务上均显著提升了使用工具进行符号推理的能力。我们的代码可在 此 https URL 获取。
| 学科： | 人工智能（cs.AI）；符号计算（cs.SC） |
| 引用为： | arXiv:2610.14402 [cs.AI] |
| （或 arXiv:2610.14402v1 [cs.AI] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.14402 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Jialiang Sun [查看电子邮件]
[v1]
2026年10月9日星期五 23:46:15 UTC（2,106 KB）
来源：arXiv cs.AI · arxiv.org