SFT-GRPO 数据重叠作为自动形式化的 后训练 超参数

受监督的 微调 (SFT) 和组相对策略优化 (GRPO) 是常见的 后训练 配方。我们对 SFT-GRPO 数据重叠进行了受控消融，在仅训练配方不同的六种条件下评估了针对 Lean 4 自动形式化进行后训练的 Qwen3-8B（思考禁用）：基本模型、仅 SFT、仅 GRPO 以及三种 SFT+GRPO 配置，其中 0%、30% 或 100% 的 GRPO 提示与 SFT 语料库一致。在零额外计算成本的情况下，保持 SFT 和 GRPO 数据不相交始终优于完全重叠。在 LLM 法官评估的 k 处编译通过和 k 处语义通过下对 Gaukao-Formal 和 PutnamBench 进行评估，我们发现较低的重叠与较高的编译和语义准确性单调相关。在 0% 重叠度下，GRPO 在高考上比单独的 SFT 产生了 10.4 个百分点的语义增益，而在 100% 重叠度下，两个指标保持平稳，使得 GRPO 阶段实际上是多余的。我们进一步表明，双度量评估揭示了最高编译模型的编译语义差距超过 30 个百分点，这种差异在仅编译基准测试下是不可见的。据我们所知，这是首次将 SFT-GRPO 数据重叠作为 后训练 超参数进行受控调查，展示了模型行为如何根据训练阶段之间的数据共享程度而变化。