SATURN: SAT-based Reinforcement Learning to Unleash Language Model Reasoning

SATURN提出一个基于SAT问题的强化学习框架，通过课程学习和可控难度的SAT任务显著提升大型语言模型在SAT、数学和编程任务上的推理能力。

Reinforcement Learning, Large Language Model, Reasoning, Curriculum Learning

Huanyu Liu, Jia Li, Hao Zhu, Kechi Zhang, Yihong Dong, Ge Li

Peking University

Generated by grok-3

Background Problem

大型语言模型（LLMs）的推理能力在数学、编程和逻辑推理任务中表现出潜力，但如何设计有效的强化学习（RL）任务以持续提升其推理能力仍是一个开放问题。现有RL任务面临三大限制：1）可扩展性不足，依赖人工标注或昂贵的LLM合成数据；2）可验证性差，LLM输出难以自动可靠验证；3）难度控制不足，难以通过从易到难的课程学习逐步培养推理能力。为解决这些问题，SATURN提出基于布尔可满足性问题（SAT）的RL框架，利用SAT问题的可扩展性、可验证性和可控难度，旨在设计一个支持课程学习并提升LLM推理能力的任务。

Method

SATURN是一个基于SAT问题的多阶段强化学习框架，核心思想是通过课程学习逐步提升LLM的推理能力。其主要步骤如下：

课程估计循环（Curriculum Estimation Loop）：动态构建具有可调难度的SAT实例，并根据LLM在验证集上的pass@1表现决定是否进入更高难度阶段。
LLM训练循环（LLMs Training Loop）：在当前难度下，使用生成的SAT训练实例通过GRPO（一种带KL散度惩罚的策略梯度优化方法）训练LLM，奖励函数结合格式正确性和答案准确性。
SAT实例构建：通过SAT_Construction工具生成(n, k, l)-SAT实例，其中n为每个子句的变量数，k为总变量数，l为子句数，通过调整参数实现可扩展性和难度控制。
难度估计：提出一个基于解决方案空间大小的难度估计公式 $D(n,k,l) = \log_2(k) + 2\log_2(l) - n + \frac{k}{n}$ ，用于课程学习的难度分级。

批判性思考：难度估计公式虽然提供了理论依据，但其与LLM实际推理难度的相关性仅通过简单的线性回归（R²值约为0.7）验证，缺乏更广泛的实证支持，可能无法准确反映LLM在不同难度任务上的表现。此外，课程学习中难度过渡的具体机制未详细说明，如何确保训练稳定性仍是一个潜在问题。

Experiment

SATURN在DeepSeek-R1-Distill-Qwen-1.5B和7B模型上进行测试，得到SATURN-1.5B和SATURN-7B，实验设计围绕四个研究问题（RQ1-RQ4）：

数据集与基准：发布SATURN-2.6k数据集，包含1500个训练实例、160个同难度测试实例和1000个更高难度的未见测试实例；同时在数学和编程任务上使用AIME、AMC、MATH-500、GPQA Diamond和LiveCodeBench等基准。
实验设置：课程学习初始难度分别为(3,5,5)和(3,5,13)，通过pass@1阈值（1.5B为0.5，7B为0.75）控制难度提升，评估指标为pass@k。
结果：1）在SAT任务上，SATURN-1.5B和SATURN-7B在未见更高难度测试集上的pass@3分别提升+14.0和+28.1；2）在数学和编程任务上，平均得分分别提升+4.9和+1.8；3）相比Logic-RL等现有RL任务方法，SATURN在Qwen2.5-7B-Instruct-1M上的平均得分提升+8.8%。
分析与批判：实验设置较为全面，涵盖了SAT任务和泛化任务的表现，但改进幅度在数学和编程任务上（尤其是SATURN-7B的+1.8）相对有限，可能受到基准选择或模型规模的限制。此外，难度估计的有效性未在不同模型间充分验证，课程学习的两次迭代是否足够也值得商榷。SATURN-2.6k数据集的难度分布是否具有代表性未明确说明，可能影响结果的普适性。

Further Thoughts

SATURN的课程学习方法为提升LLM推理能力提供了一个新颖视角，但其局限性也启发了一些更广泛的思考。首先，SAT问题的指数级复杂性可能限制其在更大规模模型或更复杂任务上的应用，未来是否可以结合其他NP问题（如图着色问题）设计更多样化的RL任务？其次，SATURN在数学和编程任务上的泛化改进有限，这提示我们推理能力的提升可能需要结合领域知识的监督信号，而不仅仅依赖形式逻辑训练。进一步研究可以探索如何将SATURN与领域特定任务（如数学定理证明）结合，以实现更强的泛化能力。此外，SATURN的难度估计方法是否适用于其他类型的推理任务？如果能将其推广到多模态推理或多智能体协作推理场景，可能为AI系统的综合推理能力带来新的突破。最后，考虑到上下文窗口瓶颈，是否可以通过分层推理或外部工具辅助（如SAT求解器）来缓解复杂SAT问题的计算负担？这可能是一个值得探索的方向。