SFT-GRPO Data Overlap as a Post-Training Hyperparameter for Autoformalization
Organizations: Osmosis AI
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.
Figures & tables
| Dataset | Pool Size | Pass Rate |
|---|---|---|
| Leanabell-Prover ( stoney0062, 2025 ) | 1.13M | 93.0% |
| Lean Workbook ( He et al., 2024 ) | 13.5K | 92.0% |
| NuminaMath ( Li et al., 2024 ) | 104K | 90.6% |
| HERALD ( Gao et al., 2025 ) | 580K | 86.6% |
| Source | Count | % | Role |
|---|---|---|---|
| NuminaMath | 8,000 | 40% | Topic-balanced competition math |
| Leanabell | 7,000 | 35% | Olympiad + AoPS diversity |
| HERALD | 3,000 | 15% | Broad Mathlib coverage |
| Lean Workbook | 2,000 | 10% | Proved + disproved statements |
| Total | 20,000 | 100% |
| Gaokao-Formal | PutnamBench | ||||||||||
| Model | C@1 | C@8 | S@1 | S@8 | C@1 | C@8 | S@1 | S@8 | |||
| Internal models | |||||||||||
| Base | 19.9 | 40.2 | 10.2 | 19.4 | 9.7 | 11.3 | 29.3 | 3.3 | 7.7 | 8.0 | |
| SFT | 61.8 | 92.3 | 41.0 | 70.9 | 20.8 | 28.5 | 65.6 | 14.3 | 34.2 | 14.2 | |
| GRPO-only | 50.9 | 69.3 | 28.1 | 40.2 | 22.8 | 36.1 | 60.1 | 11.9 | 19.2 | 24.2 | |
| SFT+GRPO-0% | 77.6 | 93.9 | 51.4 | 72.7 | 26.2 | 47.9 | 78.1 | 23.6 | 43.0 | 24.3 | |
| Gaokao-Formal | PutnamBench | ||||
| Model | Mean | Mean ≠0 | Mean | Mean ≠0 | |
| Base | 0.215 | 0.678 | 0.106 | 0.563 | |
| SFT | 0.719 | 0.805 | 0.375 | 0.697 | |
| GRPO-only | 0.423 | 0.712 | 0.244 | 0.576 | |
| SFT+GRPO-0% | 0.742 | 0.809 | 0.468 | 0.694 | |
| SFT+GRPO-30% | 0.716 | 0.791 | 0.427 | 0.693 | |
Appendix figures & tables7 assets
Supplementary material from the paper’s appendix.
Appendix
| Gaokao-Formal | PutnamBench | ||||||||
|---|---|---|---|---|---|---|---|---|---|
| Model | @1 | @2 | @4 | @8 | @1 | @2 | @4 | @8 | |
| Base | 19.9 | 26.4 | 33.2 | 40.2 | 11.3 | 16.6 | 22.7 | 29.3 | |
| SFT | 61.8 | 75.8 | 86.1 | 92.3 | 28.5 | 40.2 | 52.9 | 65.6 | |
| GRPO-only | 50.9 | 58.3 | 64.2 | 69.3 | 36.1 | 44.3 | 52.2 | 60.1 | |
| SFT+GRPO-0% | 77.6 | 86.2 | 91.0 | 93.9 | 47.9 | 59.6 | 69.7 | 78.1 | |
| SFT+GRPO-30% | 76.4 | 84.7 | 89.8 | 92.9 | 46.4 | 56.7 | 65.5 | 71.9 | |
| Gaokao-Formal | PutnamBench | ||||
|---|---|---|---|---|---|
| Model | S@1 | S@8 | S@1 | S@8 | |
| Base | 10.2 | 19.4 | 3.3 | 7.7 | |
| SFT | 41.0 | 70.9 | 14.3 | 34.2 | |
| GRPO-only | 28.1 | 40.2 | 11.9 | 19.2 | |
| SFT+GRPO-0% | 51.4 | 72.7 | 23.6 | 43.0 | |
| SFT+GRPO-30% | 48.6 | 70.7 | 22.9 | 38.8 | |
| Model | Gaokao | Putnam |
|---|---|---|
| Base | 9.7 | 8.0 |
| SFT | 20.8 | 14.2 |
| GRPO-only | 22.8 | 24.2 |
| SFT+GRPO-0% | 26.2 | 24.3 |
| SFT+GRPO-30% | 27.8 | 23.5 |
| SFT+GRPO-100% | 22.3 | 14.4 |
| Parameter | Value |
|---|---|
| Base model | Qwen/Qwen3-8B |
| Chat template | qwen3 (thinking disabled) |
| Sequence length | 4096 |
| Sample packing | Enabled (flex attention) |
| Micro batch / Epochs | 2 / 2 |
| Optimizer | AdamW (fused), cosine LR , warmup 0.1 |
| Parameter | Value |
|---|---|
| Rollout | |
| Samples per prompt / Batch / Global | 8 / 64 / 128 |
| Max response length | 16,384 tokens |
| Temperature / Epochs | 1.0 / 1 |
| GRPO | |
| KL loss coeff / type | 0.01 / low-variance KL |
| # | Problem | Failure Mode | Score |
|---|---|---|---|
| 1 | Putnam 1963 A4 | Wrong relationship | 0.1 |
| 2 | Putnam 1964 B4 | Trivially true tautology | 0.0 |
| 3 | Putnam 1963 B2 | Dropped constraint | 0.1 |