SAT-RL：用符号求解器训练语言模型做逻辑推理

SAT-RL 是一个强化学习框架，训练 LLM 通过多轮工具调用与 Z3 等可满足性求解器交互，以缓解问题难度随约束交互数量和搜索空间增长而上升的困境。该框架结合可验证解的合成数据生成、求解器增强轨迹的监督预热，以及带工具感知奖励的求解器接地强化学习。实验显示其在域内和域外逻辑任务上均显著提升了带工具符号推理能力，代码已开源。