Can a Fine-Tuned Small LM Beat a Large LM at Mathematics?

Research report — 2026-07-09. Scope: can a fine-tuned small model (target 0.6B–4B, QLoRA/SFT on an open base) reach benchmark parity with or beat a large/frontier model at a math skill, across four behaviors — proof generation, grading/evaluation, teaching/tutoring, autoformalization — comparing informal (NL) vs formal (verifiable) styles. Purpose: pick (or reject) a behavior for the one-week QLoRA build described in Train Your Own Small Learning Model.md. This report extends brainlift.md (which covers the general SFT/QLoRA/eval stack) with math-specific evidence.

Executive answer

"Beat a frontier model on a public math benchmark" is achievable — but only in the narrow, specialist-beats-generalist sense, only where the task is machine-checkable, and mostly at 7B–8B rather than sub-4B. The pattern is consistent across all four behaviors:

Behavior	Does a small tuned model beat a frontier model?	Best real evidence	Genuine ≤4B?
Formal proof gen (Lean)	Yes, decisively vs generalists	Goedel-Prover-V2-8B > DeepSeek-Prover-V2-671B on miniF2F pass@32 (84.6 vs ~82.4)	Kimina-Distill-1.7B = 72.95% miniF2F (distilled)
Grading / verifying	Yes, on first-error localization	Qwen2.5-Math-PRM-7B (73.5 F1) > GPT-4o (61.9) on ProcessBench	GenPRM-1.5B+Maj@8 (63.4) > GPT-4o ✅
Teaching / tutoring	Yes, on "withhold the answer"	DPO Llama-3.1-8B > GPT-4o in human pedagogy eval	MathDial Flan-T5-780M reveals 4% vs ChatGPT 32%
Autoformalization (statement)	Yes vs frontier	StepFun-Formalizer-7B > R1-671B, o3-pro, Claude-4, Gemini-2.5 on BEq@1	(none shown sub-4B; all ~7B)
Informal PROSE proofs (real analysis)	No — small models don't even compete	No sub-4B prose-proof generator exists in the literature	✗

The single most important distinction: every small-model "win" above is on a task with a cheap, objective correctness signal — a Lean compiler, an integer final answer, a step-label, or a "did it reveal the answer" flag. The one behavior with no such signal — writing rigorous real-analysis prose proofs — is exactly the one where small models are absent and even frontier models are weak. This is the generator–verifier asymmetry in action, and it should drive the project choice.

Cross-cutting frame

1. The generator–verifier asymmetry is confirmed and is the key lever

Verifying/grading a solution is generically easier than producing one, so a small specialist can win at checking while losing at generating.

Measured gap: on GPQA-Diamond, oracle Pass@100 = 82.8% but majority-vote selection = 45.5% — the right answer is usually generated but not selected, so a better (even small) verifier captures huge headroom. (Weaver, Stanford Hazy Research, arXiv:2506.18203; GV-gap formalized in arXiv:2509.17995.) Caveat: asymmetry is not universal — some tasks are "easy to solve, hard to verify."
Process supervision beats outcome supervision at all data scales, and catches right-answer/wrong-reasoning cases (OpenAI "Let's Verify Step by Step", arXiv:2305.20050; released PRM800K = 800k human step labels).
Implication for the four behaviors: grading (2) and formal proving/autoformalization (4) sit on the easy side of the asymmetry; informal prose-proof generation (1) sits on the hard side. Tutoring (3) is a third category — a policy problem (withhold the answer), not a capability problem.

2. Scale calibration — most "small beats frontier" headlines are 7B–32B, NOT sub-4B

Be explicit about the size a result was achieved at. The genuinely sub-4B wins are narrow:

GenPRM-1.5B (+Maj@8) beats GPT-4o on ProcessBench error localization — the strongest clean sub-4B "beats frontier" result found (arXiv:2504.00891, independent lab). Note the win needs test-time voting over 8 samples; greedy Pass@1 (57.3) trails GPT-4o.
Kimina-Prover-Distill-1.7B = 72.95% miniF2F pass@32 — a real sub-2B formal prover, but distilled from a 72B teacher (capability inherited, not independently trained) and reliant on heavy proof search.
DeepSeek-R1-Distill-Qwen-1.5B = 83.9% MATH-500 / 28.9% AIME'24 — beats non-reasoning GPT-4o but this is final-answer accuracy (see §Skill 1), and it loses to o1-mini/o1-preview.
Everything else headline-worthy (Goedel-V2-8B, StepFun-7B, DPO-tutor-8B, Qwen-PRM-7B) is 7B–8B+. At 0.6–4B expect a meaningful step down from these numbers.

3. Contamination / self-report caveats (apply to every number below)

GSM8K/MATH are contaminated. GSM1k (1,000 fresh analog problems) shows drops up to 13%, correlated with memorization; smaller/benchmark-tuned models drop most (Scale AI, arXiv:2405.00332). GSM-Symbolic shows all models degrade on templated variants, with Phi-3/3.5 among the larger droppers (Apple, arXiv:2410.05229) — though a reanalysis argues the contamination-vs-distribution-shift evidence is weaker than headlined.
Many prover/PRM headline numbers are vendor self-reported, sometimes on a same-vendor benchmark (ProcessBench and Qwen2.5-Math-PRM are both Qwen). Independent cross-checks used here: PutnamBench public leaderboard (provers), GenPRM (independent lab, corroborates ProcessBench), PRMBench (independent, tempers it).
Compute regime dominates prover comparisons. pass@32 vs pass@8192 vs step-level multi-agent tree search vs self-correction loops are different compute classes — read every prover % with its sampling budget.
A few 2026-dated sources the agents surfaced cite unreleased models (GPT-5.5, Gemini-3.1); their specific numbers are treated as low-confidence and are not load-bearing here.

Skill 1 — Proof generation

Formal (Lean/Isabelle): small specialists beat frontier generalists — real and robust

Goedel-Prover-V2-8B = 84.6% miniF2F pass@32, explicitly outperforming DeepSeek-Prover-V2-671B (~82.4% matched budget) at ~80–100× fewer params; the 32B version solves 86/PutnamBench (pass@184) vs the 671B's 47, and beats Kimina-72B (arXiv:2508.03613, self-reported; PutnamBench leaderboard corroborates).
Kimina-Prover-Distill-1.7B = 72.95% miniF2F pass@32 (RL variant 76.63%) — smallest competitive prover found; exceeds every pre-2025 7B prover and vastly exceeds GPT-4-direct (~20–31%). Distilled from Kimina-72B (arXiv:2504.11354; HF AI-MO).
BFS-Prover-V2-32B = 95.08% miniF2F (step-level multi-agent tree search) — SOTA-class but very high inference compute (arXiv:2509.06493).
Why small wins here: the Lean compiler is a perfect verifier, so a specialist can be trained with expert iteration and search-verify loops; frontier generalists are "under-trained on Lean 4" (TheoremLlama, arXiv:2407.03203). But note: these are heavily-engineered systems (distillation from huge teachers + tree search + self-correction), not a plain one-week QLoRA.

Informal (real-analysis prose proofs): small models do NOT compete

No sub-4B (indeed no small) prose-proof generator exists in the literature. The Open Proof Corpus (arXiv:2506.21621) evaluates only frontier/≥235B generators (o3, Gemini-2.5-Pro, Qwen3-235B, R1); small models appear at most as 8B graders.
Right answer ≠ right proof: o3's score dropped ~30% when a valid proof was required (only 59.5% of its correct answers had a valid proof). This is the crux — the MATH-500/AIME small-model "wins" below are all on the answer-accuracy axis, which overstates proof ability.
Even frontier models are weak at analysis proofs. On analysis-style proof benchmarks the best models score in the low tens of percent (and open models ~0% on the hardest tiers). FrontierMath: even frontier models are low (o3 ~25% self-reported vs Epoch-independent o3-mini 11%; research-tier ≈ 0%), amid a real contamination controversy (OpenAI funded it and saw nearly all problems). Prose-proof grading itself is a recent, still-open research area needing large LLM judges + reference solutions (ProofBench/ProofGrader, proofgrader.github.io / arXiv:2510.13888).

Final-answer competition math (the "wins" that aren't proofs)

DeepSeek-R1-Distill-Qwen-1.5B/7B = 83.9%/92.8% MATH-500, 28.9%/55.5% AIME'24 — 1.5B beats non-reasoning GPT-4o (74.6/9.3) but not o1-mini (90.0/63.6) (arXiv:2501.12948, self-reported).
rStar-Math: Qwen2.5-Math-7B 58.8→90.0% MATH, 0→53.3% AIME via MCTS + a 7B process reward model; 1.5B → 88.6% MATH; "surpasses o1-preview" on answer accuracy (arXiv:2501.04519).
Phi-4-mini-reasoning (3.8B) = 94.6% MATH-500 / 57.5% AIME'24, distilled from R1 traces (arXiv:2504.21233). All of these are auto-verified integer/expression answers, not graded proofs.

Verdict (Skill 1): formal proving is a genuine small-beats-large domain but demands serious infra; informal real-analysis proof generation is the worst possible one-week target — no small-model precedent, frontier models themselves are weak, and grading is unsolved.

Skill 2 — Grading / evaluating proofs (verification)

This is where the cleanest sub-4B "beats frontier" evidence lives.

Qwen2.5-Math-PRM-7B (73.5 avg F1) beats GPT-4o-0806 (61.9) at first-error localization on ProcessBench (GSM8K/MATH/Olympiad/Omni-MATH) (arXiv:2501.07301). The 72B PRM = 78.3.
GenPRM-1.5B (+Maj@8) = 63.4 F1 > GPT-4o (61.9) — genuine ≤4B win, from an independent lab, trained on just 23K MATH examples; GenPRM-7B (80.5) beats the 10× larger 72B PRM (arXiv:2504.00891). Caveat: the sub-GPT-4o win needs Maj@8 test-time compute + code execution; greedy Pass@1 (57.3) trails GPT-4o.
Load-bearing caveats:
1. All specialists still trail the reasoning frontier model o1-mini (87.9) on ProcessBench.
2. On the harder, adversarial PRMBench, the same 7B PRM (65.5) drops below GPT-4o (66.8) and o1-mini (68.8); all models are far under human (83.8) (arXiv:2501.03124, independent).
3. The advantage comes from supervision quality (human/consensus step labels), not size — untuned open PRMs lose badly (Math-Shepherd-7B 31.5, Skywork-7B 42.1 vs GPT-4o 61.9).
4. Headline ProcessBench is Qwen model on Qwen benchmark (GenPRM independently corroborates).
LLM-as-judge for math grading reaches ~~86–93% agreement with humans (κ≈0.73–0.81); binary pass/fail beats partial-credit scales by ~20 F1 points; judges are stricter than humans (~~10% false-negative bias). Consistent with brainlift.md's judge findings.

Verdict (Skill 2): the generator–verifier asymmetry is real and documented at ≤4B on a ready-made public benchmark. Best-supported "small beats frontier on a benchmark" story of the four — with the honest caveat that "frontier" here means GPT-4o, not o1-mini.

Skill 3 — Teaching / tutoring

Best fit for the project's actual framing ("reliably do ONE narrow behavior"), because pedagogy failure is a policy problem, not a capability problem.

Frontier models are bad tutors by default — they reveal the answer. MRBench: GPT-4 fails the "doesn't reveal the answer" dimension ~47% of the time — worst of all tested LLMs; prompted Mistral-7B (86.5) and Llama-3.1-8B (74.0) already withhold better (NAACL 2025, arXiv:2412.09416).
A fine-tuned small model beats GPT-4o on human pedagogy eval. DPO-tuned Llama-3.1-8B beats GPT-4o on student-correctness (0.65 vs 0.49) and wins the human rubric eval (8.55 vs 8.07, p<0.05) (UMass, arXiv:2503.06424). Caveat: simulated students, and possible GPT-4o self-bias as the automated judge.
The narrow-behavior "reliability" case, quantified at 780M: MathDial's fine-tuned Flan-T5-780M reveals the answer 4% of the time vs prompted ChatGPT's 32%, at comparable early solve-success (EMNLP-F 2023, arXiv:2305.14536).
BEA-2025 shared task: small fine-tuned/open models won the pedagogy tracks (Guidance = Mathstral-7B, Actionability = GLM-4-9B; a 0.5–1.5B entry was competitive); frontier models won only "Mistake Location" (arXiv:2507.10579).
Big caveats: (1) no objective benchmark — pedagogy is scored by human rubric, learned reward model, or LLM-judge, and generic LLM-judges (Prometheus2, Llama-8B) were found unreliable for pedagogy (MRBench). (2) Fine-tuning is not automatically sufficient: MathTutorBench shows two poorly-specialized 7B tutors lost to GPT-4o on scaffolding, and documents a solving-vs-teaching trade-off (arXiv:2502.18940). (3) Essentially no real-student learning-gain evidence (Khanmigo studies null/pending).

Verdict (Skill 3): strongest match to "reliability of a narrow behavior" and to the project's own litmus test (a prompted frontier model can't reliably withhold the answer). Weakest match to "beat on a public benchmark" because the objective benchmark doesn't exist.

Skill 4 — Autoformalization (Lean)

The most "beatable" capability target, thanks to the free type-check signal — but faithfulness is the catch.

StepFun-Formalizer-7B beats every frontier model tested — DeepSeek-R1-671B, o3-pro, Claude-4-thinking, Gemini-2.5-thinking — on BEq@1 (compiles AND is bidirectionally equivalent to a human ground-truth Lean statement): 38.3 vs 18.4/22.6/20.8/17.8 on FormalMATH-Lite (arXiv:2508.04440). 7B ≈ 32B (data-limited).
Herald-7B = 93.2% miniF2F-test statement formalization (Pass@128, compile + NLI back-translation), crushing InternLM2-Math-7B (74.0) and TheoremLlama (50.1) (ICLR 2025, arXiv:2410.10878). Caveat: Pass@128 is a loose "any-of-128" metric.
The free Lean signal powers self-improvement loops with little/no labeled data: FormaRL (GRPO with compiler + consistency reward, arXiv:2508.18914), DeepSeek-Prover expert iteration, Lean Workbook active learning (57K problems @ 93.5% audited).
The catch — compile ≠ faithful. Every serious pipeline bolts an LLM/NLI/critic judge on top of the compiler because a Lean statement can type-check yet mean the wrong thing. Faithfulness eval is a documented open problem: 31.8% of published Lean-4 ProofNet ports were themselves wrong, motivating BEq+/ProofNetVerif and critic models like CriticLean (arXiv:2406.07222, arXiv:2507.06181). Statement autoformalization is much easier than full-proof autoformalization.
Scale note: the winners (StepFun, Herald, Kimina) are all 7B; no sub-4B autoformalizer win was found.

Verdict (Skill 4): strong small-beats-frontier evidence and a built-in verification signal ideal for an expert-iteration loop — but the real deliverable becomes the faithfulness eval, which is unsolved, and the demonstrated wins are at 7B, not sub-4B.

Recommendation for the one-week QLoRA build (0.6–4B)

Is "beating a frontier model on a public benchmark" realistic at 0.6–4B in one week? Partially. It is realistic for a machine-checkable task against a non-reasoning frontier model (GPT-4o), on the easy side of the generator–verifier asymmetry. It is not realistic to beat a reasoning frontier model (o1-mini/o3) or to win at prose-proof generation.

Ranked picks:

PRIMARY — Grading / verification (a fine-tuned first-error-localizer / process verifier).
- Only one of the four with a clean sub-4B "beats GPT-4o on a public benchmark" precedent (GenPRM-1.5B on ProcessBench).
- Fits QLoRA-in-a-week: distill step-level correct/incorrect labels from a frontier teacher (PRM800K-style), train a small verifier, evaluate on the ready-made ProcessBench (objective F1 — no judge-bias problem).
- Sits on the winning side of the asymmetry; the base model likely lacks reliable error-localization (passes the project's "a prompt can't already do it" gate).
- Honest framing to adopt: target "beats GPT-4o-class grading," not o1-mini; report the PRMBench regression as a robustness caveat.
CO-PRIMARY — Tutoring "withhold-the-answer / Socratic hint" behavior.
- Best fit to the project's actual thesis (reliability of a narrow behavior), with the cleanest "prompted frontier model fails, small tune succeeds" evidence (MRBench + DPO-tutor).
- Cheap data (MathDial/Bridge exist; distill a teacher for Socratic traces) and a cheap binary eval ("did it reveal the answer?").
- Trade-off vs pick 1: weaker on "public benchmark" (no objective leaderboard; pedagogy judged by rubric), so it's the better pick if you weight the project's reliability framing over a headline benchmark number.
STRETCH — Statement autoformalization (informal math → Lean statement).
- Free type-check signal enables a self-improvement loop; strong 7B precedent. But winners are 7B not sub-4B, and the real work becomes the faithfulness eval (an open problem) — likely too much for one week at ≤4B unless scoped tightly (one narrow domain, human-audited sample).
AVOID — Informal real-analysis prose-proof generation.
- No small-model precedent, frontier models themselves are weak, and grading is unsolved. This is the hard side of the asymmetry and violates the project's spirit (you'd be chasing a capability even frontier models lack). Formal proof generation is impressive but needs distillation-from-72B + tree-search infra that doesn't fit a one-week QLoRA.

One-line answer: A fine-tuned 0.6–4B model can credibly beat a (non-reasoning) frontier model at math tasks that have a cheap objective checker — grade/verify steps, withhold answers, autoformalize statements — but not at writing rigorous real-analysis proofs. Pick the verifier (for a benchmark win) or the Socratic tutor (for the project's reliability thesis); avoid prose proof generation.

Caveats summary

Sub-4B evidence is thin; most wins are 7B–8B. Budget for a step down at 0.6–4B.
"Beats frontier" almost always means beats GPT-4o, not o1-mini/o3.
Many prover/PRM numbers are vendor self-reported, sometimes same-vendor benchmark; compute budget (pass@k, test-time voting, search) is often doing the heavy lifting.
GSM8K/MATH contamination is real; prefer contamination-controlled or held-out evals.
For grading/formal/autoformalization the checker is objective; for tutoring it is not — its "benchmark" is a rubric/judge, so an adversarial binary behavioral eval (per brainlift.md) matters most there.

Key sources

Formal proving: Goedel-Prover-V2 (arXiv:2508.03613), Kimina-Prover (2504.11354), DeepSeek-Prover-V2 (2504.21801), BFS-Prover-V2 (2509.06493), PutnamBench (2407.11214 + trishullab.github.io/PutnamBench), miniF2F (2109.00110), miniF2F-Revisited (2511.03108). Verification: ProcessBench (2412.06559), "Lessons of Developing PRMs" (2501.07301), GenPRM (2504.00891), PRMBench (2501.03124), Math-Shepherd (2312.08935), Let's Verify Step by Step (2305.20050), Weaver (2506.18203). Tutoring: MathDial (2305.14536), DPO tutor (2503.06424), MRBench (2412.09416), MathTutorBench (2502.18940), BEA-2025 (2507.10579), Bridge (NAACL 2024). Autoformalization: StepFun-Formalizer (2508.04440), Herald (2410.10878), Kimina-Autoformalizer (2504.11354), FormaRL (2508.18914), ProofNet (2302.12433), type-check/BEq+ (2406.07222), CriticLean (2507.06181), MMA (2311.03755). Proof-eval / ceilings: Open Proof Corpus (2506.21621), ProofGrader (2510.13888), FrontierMath (2411.04872). Contamination: GSM1k (2405.00332), GSM-Symbolic (2410.05229).