SFT-GRPO Data Overlap as a Post-Training Hyperparameter for Autoformalization

TL;DR

This paper investigates how varying the overlap of data between supervised fine-tuning and group relative policy optimization affects autoformalization performance, revealing that less overlap improves accuracy.

Contribution

It provides the first controlled study on SFT-GRPO data overlap, showing that disjoint data enhances model performance and exposes semantic gaps.

Findings

Disjoint SFT and GRPO data outperform overlapping data at no extra cost.

Lower data overlap correlates with higher compilation and semantic accuracy.

Dual-metric evaluation uncovers significant compile-semantic gaps in models.

Abstract

Supervised fine-tuning (SFT) followed by Group Relative Policy Optimization (GRPO) is a common post-training recipe. We conduct a controlled ablation over SFT-GRPO data overlap, evaluating Qwen3-8B (thinking disabled) post-trained for Lean 4 autoformalization under six conditions that differ solely in training recipe: a base model, SFT-only, GRPO-only, and three SFT+GRPO configurations where 0 percent, 30 percent, or 100 percent of the GRPO prompts coincide with the SFT corpus. Keeping SFT and GRPO data disjoint consistently outperforms full overlap at zero additional compute cost. Evaluating on Gaokao-Formal and PutnamBench under both compile pass at k and semantic pass at k assessed by an LLM judge, we find that lower overlap is monotonically associated with higher compilation and semantic accuracy. At 0 percent overlap, GRPO yields a 10.4 percentage point semantic gain over SFT alone on Gaokao, while at 100 percent overlap both metrics remain flat, rendering the GRPO stage effectively redundant. We further show that dual-metric evaluation reveals compile semantic gaps exceeding 30 percentage points for the highest compiling models, a disparity invisible under compile-only benchmarking. To our knowledge, this is the first controlled investigation of SFT-GRPO data overlap as a post-training hyperparameter, demonstrating how model behavior varies based on the degree of data sharing between training stages.