SATURN框架：基于SAT问题的大语言模型推理训练方法

1. 项目概述：SATURN框架的设计动机

在当前的AI研究领域，大语言模型（LLMs）的推理能力训练面临三个关键瓶颈。首先是数据生成成本问题——现有的数学证明或编程题生成要么依赖专家标注（如MATH数据集），要么需要调用LLM本身进行合成（如LeanDojo），每道题的平均生成成本高达3-7美元。其次是验证可靠性问题——当模型输出一个数学证明步骤时，即便是专门的验证器也可能出现误判（如Metamath验证器对某些构造性证明的误拒率可达12%）。最后是难度控制问题——GSM8K数据集中"简单"与"困难"题目的区分度不足，导致模型训练过程容易出现震荡。

SATURN框架的创新在于选择布尔可满足性问题（SAT）作为训练载体。一个典型的SAT问题形如：(x₁∨¬x₂)∧(x₂∨x₃)∧(¬x₁∨¬x₃)，其优势体现在：

• 生成成本：随机生成含n个变量、k个子句的3-SAT问题仅需O(nk)时间复杂度
• 验证效率：验证候选解只需线性扫描子句，百万级规模的问题可在毫秒级完成
• 难度调控：通过调节变量数n与子句数k的比例，可精确控制问题难度（当k/n≈4.26时达到相变点）

2. 核心架构解析

2.1 双循环训练机制

SATURN采用课程评估循环（外循环）与模型训练循环（内循环）的协同架构。外循环每完成1000个训练step就会启动，其工作流程如下：

1. 从当前难度池采样100个SAT问题作为测试集
2. 计算模型在这些问题上的平均解决率P
3. 根据P值动态调整难度参数：
   • P>0.8：将变量数n增加10%，子句数k调整为⌈4.26n⌉
   • 0.5<P≤0.8：保持当前参数
   • P≤0.5：将n减少5%，k调整为⌈3.8n⌉

内循环采用标准的PPO强化学习算法，但创新性地将SAT问题的解决过程建模为马尔可夫决策过程。每个时间步t，模型需要：

• 观察当前部分赋值状态s_t（如x₁=True, x₂=Unassigned）
• 选择动作a_t∈
• 获得即时奖励r_t：每正确赋值一个变量得+0.1，完整解出问题得+5，错误赋值导致矛盾得-1

2.2 难度量化公式

传统SAT难度指标（如树形分解宽度）不适用于LLM场景。我们提出的新