mathcompose — two ≤4B math models that demonstrate the generator–verifier gap

Thesis: you can't make a 1.5B model out-reason a frontier model, but you can make a small specialist win on the easy side of the generator–verifier asymmetry — and you can measure the asymmetry itself with two small models that compose.

Model V — a generative process verifier. Given a problem and a step-by-step solution, it emits a paragraph-by-paragraph critique ending in \boxed{k} (0-based index of the first wrong step, or -1 if all correct). Evaluated on ProcessBench (objective harmonic-mean F1; target: beat GPT-4o's ~61.9) with PRMBench as the adversarial robustness set.
Model G — a step-by-step solution generator. Distilled from a frontier teacher and filtered so only answer-correct traces survive.
The headline: V reranks G's samples (V-weighted majority / best-of-n). We report the recovered generator–verifier gap (oracle pass@n − majority) at ≤4B — the Weaver headroom result, but ours.

Every core metric is an objective checker (step-label F1, boxed-answer equivalence) — no LLM-judge, so there is no judge bias to argue about.

Both models share one base (Qwen/Qwen2.5-Math-1.5B-Instruct, apache-2.0) and one training path (a generative verifier is just SFT), which is what makes a two-model build tractable.

Why these choices (grounded in `notes/`)

notes/research-small-vs-large-math.md finds the only clean sub-4B "beats GPT-4o" precedent is process verification (GenPRM-1.5B on ProcessBench) → V is the primary model.
The generator–verifier asymmetry is "the key lever" → G + composition turn two models into one coherent demonstration.
notes/brainlift.md: distill the process not the label, data quality over quantity, eval before training → the whole pipeline follows this.
Verified constraints baked in: base context is 4096 tokens; trl 1.7.1 has no PRMTrainer (so V is generative SFT, not a discriminative PRM); transformers 5.x renamed max_seq_length → max_length and torch_dtype → dtype.

Layout

configs/            base.yaml + verifier_v.yaml + generator_g.yaml (extends base)
src/mathcompose/
  common/           chat prompts (ProcessBench critic format), \boxed grading, config, io
  teachers/         pluggable Anthropic/OpenAI teacher (+ offline DummyTeacher)
  datagen/          PRM800K parsing, teacher critique synthesis, answer-filtered CoT, dedup
  data/             V output schema + dataset builders (CLI)
  eval/             ProcessBench, PRMBench, MATH, composition, runners, run.py (CLI)
  train/            shared QLoRA SFT (train.py --task {v,g}) + colab_train.ipynb
  infer/            demo.py (incl. base-vs-tuned side-by-side)
tests/              CPU smoke suite (26 tests)   scripts/smoke_all.sh

Quickstart

0. Prove the harness on CPU (no GPU, no key)

pip install -e .
./scripts/smoke_all.sh            # fast logic tests
./scripts/smoke_all.sh --full     # + tiny-model train/eval + HF dataset probes

1. Build the datasets (needs a teacher key)

The default teacher is the promptlens gateway (OpenAI-compatible). Copy .env.example → .env and set TFY_API_KEY=tfy-... (auto-loaded). Verify with python scripts/check_teacher.py. (Use --teacher openai|anthropic for native providers instead.)

cp .env.example .env && $EDITOR .env      # set TFY_API_KEY
# Model V: PRM800K first-error labels + teacher-synthesized critiques (labels stay authoritative)
python -m mathcompose.data.build_verifier_dataset --prm800k data/raw/prm800k/phase2_train.jsonl \
    --teacher promptlens --limit 15000
# Model G: distill CoT, keep only answer-correct traces
python -m mathcompose.data.build_generator_dataset --source AI-MO/NuminaMath-CoT \
    --teacher promptlens --limit 8000

Contamination against ProcessBench/MATH-500 is enforced automatically (--no-dedup to disable).

2. Train (GPU — free Colab T4 works; see `src/mathcompose/train/colab_train.ipynb`)

python -m mathcompose.train.train --task v --config configs/verifier_v.yaml
python -m mathcompose.train.train --task g --config configs/generator_g.yaml

3. Evaluate (objective, base vs tuned) + the composition

python -m mathcompose.eval.run processbench --tag base   --maj-k 1
python -m mathcompose.eval.run processbench --adapter runs/verifier_v --tag tuned --maj-k 8
python -m mathcompose.eval.run prmbench     --adapter runs/verifier_v --tag tuned
python -m mathcompose.eval.run math         --adapter runs/generator_g --tag tuned
python -m mathcompose.eval.run compose --gen-adapter runs/generator_g --ver-adapter runs/verifier_v \
    --dataset Maxwell-Jia/AIME_2024 --split train --problem-field Problem --answer-field Answer
python -m mathcompose.eval.run report        # -> results/RESULTS.md

4. Demo (for the video)

python -m mathcompose.infer.demo --task v --adapter runs/verifier_v --compare \
    --problem "..." --steps "step 0" "step 1 (wrong)"

What runs where

Piece	Where	Needs
Harness + smoke tests	this repo, CPU	nothing
Data generation	anywhere	a teacher API key (Anthropic/OpenAI)
QLoRA training	Colab/Modal/RunPod GPU	a CUDA GPU (free T4 ok)
Publishing datasets/models	—	your HF token
Demo video	—	you record; script in the plan

Honest framing (from the research note)

"Beats frontier" means beats GPT-4o, not o1-mini/o3. Sub-4B evidence is thin (most precedents are 7B) — expect a step down. The real, defensible claim is the base-vs-tuned delta and the composition lift, both measured objectively. PRMBench is reported alongside ProcessBench as the independent robustness check.

License / attribution

Code: MIT. Training data derives from PRM800K (MIT, OpenAI) and NuminaMath-CoT (apache-2.0); evals use ProcessBench, PRMBench, MATH-500, AIME-2024 (all apache-2.0). Attribute these in any published dataset/model card.