notes/research-small-vs-large-math.md

# 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:**

1. **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.

2. **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.

3. **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).

4. **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).