Upload folder using huggingface_hub

.gitignore

@@ -0,0 +1,23 @@
+# secrets — NEVER commit
+.env
+.env.*
+!.env.example
+
+# data + model artifacts (published to HF Hub, not committed)
+# NOTE: anchored to repo root so they do NOT match the src/mathcompose/data/ package.
+/data/
+/runs/
+*.safetensors
+*.bin
+
+# python
+__pycache__/
+*.pyc
+.pytest_cache/
+*.egg-info/
+.ipynb_checkpoints/
+.venv/
+venv/
+
+# keep results tables committed
+!results/

README.md

@@ -0,0 +1,116 @@
+# 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)
+```bash
+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.)
+```bash
+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`)
+```bash
+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
+```bash
+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)
+```bash
+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.

configs/base.yaml

@@ -0,0 +1,39 @@
+# Shared defaults inherited by verifier_v.yaml and generator_g.yaml.
+# Verified facts baked in: Qwen2.5-Math-1.5B-Instruct is apache-2.0, ctx=4096,
+# uses the CoT system prompt "Please reason step by step, and put your final
+# answer within \boxed{}."  Do NOT use <|endoftext|> as pad token.
+
+model:
+  base_id: "Qwen/Qwen2.5-Math-1.5B-Instruct"
+  max_context: 4096            # HARD ceiling for this base — mind truncation.
+  pad_token: "<|fim_pad|>"     # distinct from eos <|endoftext|>; avoids infinite-gen bug.
+
+lora:
+  r: 16
+  alpha: 32                    # alpha = 2r
+  dropout: 0.05
+  target_modules: "all-linear" # attention + MLP (LoRA-Learns-Less best practice)
+
+train:
+  epochs: 3
+  learning_rate: 2.0e-4
+  lr_scheduler_type: "cosine"
+  warmup_ratio: 0.03
+  per_device_train_batch_size: 2
+  gradient_accumulation_steps: 8
+  gradient_checkpointing: true
+  optim: "paged_adamw_8bit"
+  bf16: true
+  packing: false
+  completion_only_loss: true   # loss on completion only (robust vs assistant_only_loss for Qwen)
+  seed: 0
+  eval_strategy: "steps"       # transformers 5.x name (not evaluation_strategy)
+  eval_steps: 50
+  save_steps: 50
+  logging_steps: 10
+
+quant:
+  load_in_4bit: true
+  bnb_4bit_quant_type: "nf4"
+  bnb_4bit_use_double_quant: true
+  bnb_4bit_compute_dtype: "bfloat16"

configs/generator_g.yaml

@@ -0,0 +1,24 @@
+# Model G — step-by-step solution generator.
+# Inherits configs/base.yaml; keys here override.
+extends: "base.yaml"
+
+task: "g"
+output_dir: "runs/generator_g"
+hub_model_id: null            # e.g. "your-username/mathcompose-generator-1.5b"
+
+data:
+  train_path: "data/generator/train.jsonl"
+  val_path: "data/generator/val.jsonl"
+  # jsonl rows are {"prompt": <problem as chat messages or str>, "completion": <CoT + \boxed{answer}>}
+
+train:
+  max_length: 2048
+  per_device_train_batch_size: 2
+  gradient_accumulation_steps: 8
+
+eval:
+  math500_id: "HuggingFaceH4/MATH-500"
+  aime_id: "Maxwell-Jia/AIME_2024"
+  # Composition (V reranks G):
+  compose_n: 8                 # samples per problem
+  compose_temperature: 0.8

configs/verifier_v.yaml

@@ -0,0 +1,24 @@
+# Model V — generative process verifier / first-error localizer.
+# Inherits configs/base.yaml; keys here override.
+extends: "base.yaml"
+
+task: "v"
+output_dir: "runs/verifier_v"
+hub_model_id: null            # e.g. "your-username/mathcompose-verifier-1.5b"
+
+data:
+  train_path: "data/verifier/train.jsonl"
+  val_path: "data/verifier/val.jsonl"
+  # jsonl rows are {"prompt": <chat messages or str>, "completion": <critique + \boxed{k}>}
+
+train:
+  # Verifier inputs (problem + full solution + per-step critique) are long:
+  # push seq_len toward the 4096 ceiling. Report truncation rate at build time.
+  max_length: 3072
+  per_device_train_batch_size: 1
+  gradient_accumulation_steps: 16
+
+eval:
+  processbench_splits: ["gsm8k", "math", "olympiadbench", "omnimath"]
+  maj_k: 8                     # Maj@k test-time voting for the headline number
+  gpt4o_reference_f1: 61.9     # standard proprietary baseline to beat

data/verifier/README.md

@@ -0,0 +1,21 @@
+---
+license: mit
+task_categories: [text-generation]
+tags: [math, process-verification, ProcessBench, PRM800K, mathcompose]
+---
+
+# mathcompose — Model V (process verifier) SFT data
+
+First-error-localization critiques for training a small generative math verifier.
+Each row: a problem + a step-indexed candidate solution (`prompt`) and a
+paragraph-by-paragraph critique ending in `\boxed{{k}}` (`completion`), where `k`
+is the 0-based index of the first erroneous step (`-1` = all correct).
+
+- **Labels** are ground truth from **PRM800K** (OpenAI, MIT).
+- **Critiques** distilled from **claude-opus-4-8** (rationalization conditioned on
+  the known label; the boxed index is stamped authoritatively, not trusted to the teacher).
+- **Deduped** against ProcessBench + MATH-500 (no eval contamination).
+- `train.jsonl`/`val.jsonl` are class-balanced (~50/50 erroneous/all-correct);
+  `*_full.jsonl` keep the natural PRM800K distribution.
+
+Built by the mathcompose harness. Eval target: ProcessBench first-error F1.

data/verifier/stats.json

@@ -0,0 +1,9 @@
+{
+  "n_total": 3214,
+  "n_train": 3054,
+  "n_val": 160,
+  "n_erroneous": 747,
+  "n_all_correct": 2467,
+  "teacher": "promptlens",
+  "deduped": true
+}

notes/brainlift.md

@@ -0,0 +1,306 @@
+# Brainlift: Training and Optimizing Small Language Models to Reliably Perform Specific Behaviors
+
+## TL;DR
+- **For instilling one narrow, falsifiable behavior into a 0.6B–4B model, the dataset is the deliverable:** LIMA (1,000 examples), s1 (1,000 traces), and QLoRA's own ablations converge on quality-and-diversity over quantity, and QLoRA makes single-GPU tuning routine. Capability is mostly *elicited* from a base model that already latently has it — not installed from scratch.
+- **QLoRA is the right default precisely because it "forgets less"** (Biderman et al.), and reliability comes from an engineering stack — distilling a teacher's *process*, constrained decoding for output form, and an adversarial base-vs-tuned eval — not from a bigger model or a cleverer prompt.
+- **Build the evaluation before you generate a single training row, and make it adversarial**, because small (and large) LMs fail in predictable, testable ways: compositional reasoning collapse (Faith and Fate), irrelevant-clause sensitivity (GSM-Symbolic, up to 65% drop), the reversal curse, lost-in-the-middle, and confident hallucination.
+
+## Purpose
+A portable research knowledge base for instilling ONE specific, falsifiable behavior into a small open base model (0.6B–4B) via supervised fine-tuning (QLoRA), using distillation from a frontier teacher to build the dataset, and evaluating with LLM-as-judge plus a base-vs-tuned comparison.
+
+**In scope:** data-centric generation/curation and distillation; PEFT (LoRA/QLoRA); SFT mechanics; preference optimization (DPO and variants); compression/quantization; small-model landscape; evaluation and LLM-as-judge; reliability and structured output; failure modes and limits of (small) LMs; practitioner playbooks.
+
+**Out of scope:** pretraining from scratch; large-scale RLHF infrastructure; multimodal training; serving/infra beyond quantization formats; agent orchestration.
+
+## Key Findings
+1. **Small-data alignment works when the capability is latent.** Two independent 1,000-example results (LIMA for general alignment, s1 for reasoning) plus QLoRA's finding that data quality beats size establish that a narrow behavior can be reached cheaply — but LoRA-Learns-Less shows this breaks down for genuinely new hard skills.
+2. **Distill the process, not the style.** Orca and DeepSeek-R1 show reasoning traces transfer real capability into small models; Orca explicitly warns that style-only imitation inflates apparent quality on shallow evals.
+3. **PEFT trades peak capacity for forgetting-resistance**, which is a feature for narrow-behavior work. Full fine-tuning still wins on hard new skills.
+4. **LLM-as-judge is usable (>80% human agreement) but biased** (position, verbosity, self-preference); design evals around the biases.
+5. **Reliability = data + constrained decoding + calibration eval.** Neither fine-tuning nor grammar-constrained decoding is individually sufficient.
+6. **Small models fail in named, reproducible ways** — build adversarial evals that target exactly those failure modes.
+
+## DOK 4 — Spiky Points of View
+
+**1. For a narrow behavior, ~1,000–2,000 excellent, diverse examples is enough; past that, more data is usually wasted effort.**
+
+- _Why:_ pretraining already installed the capability, so SFT only has to pin a consistent output policy over what the model already knows (Superficial Alignment Hypothesis). Rows past the first ~1k mostly re-teach that and add overfitting risk.
+- What still helps is coverage of the behavior's input variety, not raw count.
+- Two independent replications on very different tasks (LIMA on alignment, s1 on competition math) landed on the same ~1,000 figure, so it isn't a single-domain fluke.
+- _Evidence:_ LIMA (1,000 examples rival RLHF models trained on 52× more data), s1 (7 vs 394 GPU-hours for near-identical accuracy), QLoRA's quality>size ablation.
+- _When wrong:_ if the base genuinely lacks the capability (novel reasoning, unfamiliar code), LoRA-Learns-Less shows you need more data AND higher rank or full FT.
+- _Abandon when:_ the base-vs-tuned delta plateaus below target despite clean, diverse data; that plateau means the capability is absent, not under-sampled.
+
+**2. Use QLoRA by default and treat "forgets less" as a feature, not a compromise.**
+
+- _Why:_ full FT rewrites high-rank directions across all weights and injects "intruder dimensions" that overwrite unrelated pretrained abilities; LoRA's low-rank cap keeps the update from traveling that far.
+- For one-behavior work you don't want to disturb anything else, so LoRA's capacity ceiling is the guardrail you want, not a weakness.
+- The alternative fails concretely: Raschka saw a model "unlearn arithmetic" from narrow SFT; Luo et al. show forgetting worsens with scale under continual full tuning.
+- QLoRA is single-GPU with no measured quality loss on tested tasks, so the default costs nothing.
+- _Evidence:_ Biderman et al. (LoRA forgets less, retains out-of-domain capability), intruder-dimensions paper (the mechanism), QLoRA (single-GPU, no perf loss), Raschka.
+- _Counter:_ full FT wins peak in-domain accuracy on genuinely hard new skills.
+- _Wrong if:_ your ONLY metric is target-task accuracy and base-capability retention is irrelevant; then use full FT or high-rank (r≈256) LoRA.
+
+**3. Build the eval before you generate a single training row, make it adversarial, and trust base-vs-tuned deltas over any single judge score.**
+
+- Without a pre-committed eval, "we fine-tuned a model" is unfalsifiable; the eval is what turns a vibe into a measurement.
+- Make it adversarial: small models fail in named ways (irrelevant clauses, reversed relations, mid-context facts) a happy-path test never triggers, so a fine-tune that clears only easy cases has learned the surface.
+- Read the delta, not the absolute score: judge biases (position, verbosity, self-preference) distort raw numbers but largely cancel when one judge compares two outputs with randomized order.
+- Prefer binary pass/fail over 1–5: it forces a crisp definition and is far more stable across judge runs.
+- _Evidence:_ Husain (evals first, 60–80% of effort; binary > 1–5), Zheng et al. (quantified biases; >80% human agreement), GSM-Symbolic and Reversal Curse (fragilities to target).
+- _Spiky corollary:_ a fine-tune shipped with no robustness eval should not be trusted, however good the demos.
+- _Wrong if:_ the behavior is code-verifiable by exact-match/regex (skip the judge), or you've validated high judge-human agreement on your task.
+
+**4. Reliability is an engineering stack (data + constrained decoding + a calibration/abstention eval), not a bigger model or a better prompt.**
+
+- Three levers fix three failure sources: fine-tuning raises the odds of correct content but can't guarantee valid form; constrained decoding guarantees form but can push the model off-path and hurt content; a calibration eval surfaces the residual confident-guess errors that only rewarding "I don't know" suppresses.
+- The deeper point: reliability is a tail property (the 1-in-50 malformed output breaks the pipeline), and scaling or prompting shifts the average while leaving the tail. Engineer the tail.
+- _Evidence:_ constrained-decoding literature (Outlines/XGrammar guarantee form), Why-Models-Hallucinate (residual errors are calibration failures), plus fine-tuning raising correct-behavior probability.
+- _Counter:_ constrained decoding adds ~2–5× overhead and can degrade content; over-constraining hides genuine uncertainty.
+- _Wrong if:_ the base is already schema-reliable and latency can't absorb decoding overhead.
+
+## DOK 3 — Insights
+
+**1. The dataset is the deliverable; capability is mostly elicited, not installed.**
+
+- LIMA (1,000 examples), s1 (1,000 traces; 394 vs 7 GPU-hours), and QLoRA's quality>size finding converge: a small, diverse, high-quality set beats a large noisy one.
+- _Why:_ pretraining did the heavy lifting, so SFT mainly selects a consistent output policy over existing knowledge; beyond a point you pay to re-teach what the model knows, and coverage matters more than count.
+- _Tension:_ LoRA-Learns-Less shows that for genuinely NEW capabilities (code, math) low-rank small-data tuning underperforms full FT—elicitation works when the capability is latent, not when it's absent.
+
+**2. Distill the process, not the style.**
+
+- Orca and DeepSeek-R1 show that transferring reasoning traces/explanations (not just final answers) is what moves a real capability into a small model; Orca warns that style-only imitation inflates apparent quality.
+- _Why:_ final-answer-only data teaches outputs without the intermediate computation, so it copies tone and collapses when the problem shifts; traces hand over the steps the student can internalize. It's also why style-rewarding evals overrate imitation-trained models.
+- _Tension:_ DeepSeek-R1 distillation still leaves persistent gaps for ≤7B students; process distillation narrows but doesn't close the teacher-student gap.
+
+**3. LoRA/QLoRA is the right default for behavior instillation precisely because it forgets less.**
+
+- Biderman et al. and the intruder-dimension paper show LoRA sacrifices peak capacity but preserves base competence—ideal when you want ONE behavior without collateral regression.
+- _Why:_ the low-rank cap limits how far the update moves the weights, so unrelated abilities survive; full FT has no such cap. For single-behavior work, preserving everything else is the goal, so the capacity limit is the property you want.
+- Raschka's "unlearned arithmetic" and Luo et al.'s forgetting-scales-with-size results show full FT/narrow data risks broad capability loss.
+- _Steelman for full FT:_ if the behavior is a hard new skill, full FT (or high-rank LoRA, α=2r, all modules) wins on the target metric.
+
+**4. Evaluation must precede and drive training.**
+
+- Hamel Husain (evals first, 60–80% of effort), LIMA (perplexity ≠ quality), and practitioner consensus all treat the eval harness as the real deliverable.
+- _Why:_ loss and perplexity don't track the behavior you care about, so without a behavioral eval you optimize a proxy; the eval is also the only signal for whether the fix is more data, different data, or a different method.
+- A base-vs-tuned LLM-judge comparison on a held-out set is the minimum viable measurement.
+
+**5. LLM-as-judge is usable but biased; design around it.**
+
+- Zheng et al. quantify position, verbosity, and self-preference biases (position can swing win-rate 10–15 points; length bias ~+17%).
+- _Why it's still workable:_ the biases are systematic, not random, so they distort absolute scores but largely cancel in A/B comparisons under a fixed judge with randomized order.
+- Mitigations: randomize order, control for length, don't judge with the same model family, prefer binary pass/fail (Husain).
+- _Tension:_ judges agree with humans >80%, so the biases are manageable, not disqualifying.
+
+**6. Reliability comes from data + decoding, not prompting.**
+
+- Fine-tuning raises the probability of correct behavior; constrained decoding (Outlines/XGrammar) guarantees output FORM.
+- _Why both:_ they govern different things (content odds vs form validity), and reliability is a tail property, so closing it takes both at once rather than a prompt that only shifts the average.
+- Neither alone suffices: constrained decoding can force off-distribution tokens and hurt content; fine-tuning can't guarantee 100% valid structure.
+
+**7. Small models fail in predictable, testable ways; build adversarial evals for exactly those.**
+
+- Named fragilities: GSM-Symbolic (irrelevant-clause drops up to 65%), Faith-and-Fate (multiplication 59%→4%), Reversal Curse (near-0% on reversed facts), Lost-in-the-Middle (U-shaped context use), and the hallucination-calibration work.
+- _Why it helps:_ because the failures are named and reproducible, the papers' own perturbations become your robustness suite, turning known weaknesses into a pre-deployment checklist.
+- A robustness eval should perturb numbers, add distractor clauses, reverse relations, and move key info to the middle.
+
+**8. "Emergence" is partly a measurement artifact.**
+
+- Schaeffer et al. show apparent emergence tracks metric choice.
+- _Why it matters here:_ a behavior that looks absent at small scale under exact-match may just be the metric masking steady progress; continuous metrics (edit distance, token-level, Brier) expose the gradient and prevent premature abandonment.
+
+## DOK 2 — Knowledge Tree
+
+### A. Data-centric AI & distillation
+
+**LIMA: Less Is More for Alignment** — Zhou et al., Meta AI, NeurIPS 2023. https://arxiv.org/abs/2305.11206. *Peer-reviewed / researcher.*
+- Fine-tuned LLaMa-65B on only 1,000 curated prompt-response pairs with standard supervised loss, no RLHF.
+- In a controlled human study, LIMA responses were equivalent or preferred to GPT-4 in 43% of cases; it beat DaVinci003 (RLHF-trained) and Alpaca-65B (trained on 52× more data). Even GPT-4 preferred LIMA's output over its own 19% of the time.
+- Hyperparameters: 15 epochs, LR 1e-5→1e-6, batch 32; perplexity did NOT correlate with generation quality, so checkpoints were selected manually on a 50-example dev set.
+- **DOK 2 Summary:** Proposes the "Superficial Alignment Hypothesis" — nearly all knowledge is learned in pretraining and alignment mainly teaches format/style, so a tiny high-quality dataset can suffice. Intellectual foundation for behavior-focused small-data fine-tuning.
+
+**Self-Instruct / Stanford Alpaca** — Wang et al. 2022 (https://arxiv.org/abs/2212.10560); Taori et al. 2023. *Peer-reviewed + technical / practitioner.*
+- Self-Instruct bootstraps 52K instructions from 175 seed tasks using a base LLM; improved the SUPER-NATURALINSTRUCTIONS baseline by 33%.
+- Alpaca reused the pipeline with text-davinci-003, generated 52K samples, and fine-tuned LLaMA-7B cheaply; AlpaGasus later showed filtering Alpaca's low-quality rows improves the model.
+- **DOK 2 Summary:** Established the template for distilling a teacher's behavior into a smaller student via synthetic instruction data — the direct ancestor of the "generate data from a frontier teacher" workflow.
+
+**Evol-Instruct / WizardLM** — Xu et al. 2023. *Peer-reviewed / researcher.*
+- Iteratively rewrites simple instructions into more complex/diverse ones (in-depth and in-breadth evolution).
+- **DOK 2 Summary:** Complexity and diversity of instructions, not just count, drive instruction-following quality — a concrete lever for dataset design.
+
+**Orca: Progressive Learning from Complex Explanation Traces of GPT-4** — Mukherjee et al., Microsoft 2023. https://arxiv.org/abs/2306.02707. *Peer-reviewed / researcher.*
+- 13B model trained to imitate GPT-4 reasoning via explanation traces and step-by-step thought, with ChatGPT as intermediate teacher; ~5M samples.
+- Beat Vicuna-13B by >100% on Big-Bench Hard and 42% on AGIEval.
+- Explicitly warns: naive imitation makes students copy the STYLE but not the REASONING of teachers, and shallow evaluation overestimates capability.
+- **DOK 2 Summary:** To transfer a behavior (not just surface style), distill the process — reasoning traces and explanations �� and evaluate rigorously, because style mimicry masks capability gaps.
+
+**Textbooks Are All You Need (phi-1) / phi-1.5** — Gunasekar et al. 2023 (https://arxiv.org/abs/2306.11644); Li et al. 2023 (https://arxiv.org/abs/2309.05463). *Peer-reviewed / researcher.*
+- phi-1: 1.3B params, trained on 6B tokens of "textbook-quality" web data + 1B tokens of GPT-3.5 synthetic textbooks/exercises; 50.6% pass@1 on HumanEval, 55.5% on MBPP. phi-1-small (350M) still hit 45% on HumanEval.
+- phi-1.5: 1.3B, matches models 5× larger on reasoning; challenges the notion that capability is determined solely by scale.
+- **DOK 2 Summary:** Data quality can substitute for scale — carefully curated/synthetic "textbook" data lets tiny models punch far above their weight, reinforcing the data-as-deliverable thesis.
+
+**FineWeb-Edu / Cosmopedia / SmolLM-Corpus** — Hugging Face (Penedo et al.). *Technical / practitioner.*
+- Cosmopedia: 25B tokens, 30M synthetic samples (Mixtral-generated textbooks/blogs/stories) — largest open synthetic dataset at release. FineWeb-Edu is an educational-quality filtered subset of FineWeb; FineMath ~50B tokens.
+- **DOK 2 Summary:** Open replications confirm that quality-filtering and synthetic generation at scale produce better small models than raw web crawl.
+
+*Collective note:* The synthetic-data surveys ("Best Practices and Lessons Learned on Synthetic Data," https://arxiv.org/abs/2404.07503; "A Survey on Post-training of LLMs," https://arxiv.org/abs/2503.06072) document that the recurring quality levers are complexity, diversity, and scale, and that quality filtering beats raw quantity. Tooling: **distilabel/Argilla** for programmatic synthetic-data and preference-pair pipelines.
+
+### B. PEFT / LoRA
+
+**LoRA: Low-Rank Adaptation** — Hu et al., Microsoft, ICLR 2022. https://arxiv.org/abs/2106.09685. *Peer-reviewed / researcher.*
+- Freezes base weights, learns low-rank update matrices A,B; far fewer trainable params and no inference latency once merged.
+- **DOK 2 Summary:** The core PEFT method — adapt behavior by learning a small rank-r perturbation instead of all weights.
+
+**QLoRA: Efficient Finetuning of Quantized LLMs** — Dettmers et al., UW, NeurIPS 2023. https://arxiv.org/abs/2305.14314. *Peer-reviewed / researcher.*
+- Finetunes a 65B model on a single 48GB GPU. Innovations: 4-bit NormalFloat (NF4), double quantization (~0.37 bits/param saved, ~3GB on a 65B model), paged optimizers. Storage in NF4, compute de-quantized to bf16.
+- Guanaco reached 99.3% of ChatGPT on the Vicuna benchmark in 24h on one GPU; the authors trained >1,000 models.
+- Found data quality > dataset size for instruction following, and that MMLU does not predict chatbot quality.
+- **DOK 2 Summary:** Makes single-GPU fine-tuning of small models routine, with no measured performance loss vs 16-bit for the tested tasks.
+
+**LoRA Learns Less and Forgets Less** — Biderman et al., Columbia/Databricks Mosaic, TMLR 2024. https://arxiv.org/abs/2405.09673. *Peer-reviewed / researcher.*
+- On code and math, standard low-rank LoRA substantially underperforms full fine-tuning; full FT learns perturbations 10–100× higher rank than typical LoRA configs.
+- But LoRA forgets less (better retains out-of-domain capability) and maintains more diverse generations; mitigates forgetting more than weight decay/dropout. Example: code IFT full-FT scored 0.414 vs LoRA r=64's 0.509 on retention.
+- Best practices: target all modules (attention + MLP), use α=2r, rank ~16 as a starting point, ≥4 epochs; LoRA is highly LR-sensitive.
+- **DOK 2 Summary:** LoRA trades peak in-domain capacity for regularization/forgetting-resistance — a favorable trade when instilling a narrow behavior without wrecking base competence.
+
+**LoRA vs Full Fine-tuning: An Illusion of Equivalence** — Shuttleworth et al. 2024. https://arxiv.org/abs/2410.21228. *Peer-reviewed / researcher.*
+- LoRA introduces "intruder dimensions" — high-ranking singular vectors dissimilar to the pretrained weights — that full FT does not; causal intervention on them shows they drive forgetting.
+- **DOK 2 Summary:** LoRA and full FT reach structurally different solutions; that difference explains both LoRA's forgetting-resistance and its capacity limits.
+
+**Sebastian Raschka — Practical Tips for Finetuning LLMs Using LoRA** (Ahead of AI, 2023). https://magazine.sebastianraschka.com/p/practical-tips-for-finetuning-llms. *Technical blog / practitioner.*
+- QLoRA: ~33% memory savings for ~33% runtime increase. Optimizer choice barely matters. In his sweep r=256/α=512 gave the best performance.
+- Apply LoRA to ALL layers, not just K/V. Multiple epochs on small instruction sets can overfit and hurt.
+- Observed a model "unlearned arithmetic" because Alpaca lacked arithmetic examples — a concrete instance of narrow capability regression.
+- **DOK 2 Summary:** Hard-won operational defaults for LoRA; the "unlearned arithmetic" anecdote grounds the forgetting risk from narrow data.
+
+### C. SFT mechanics
+- **Loss masking / train-on-completions-only**: standard TRL SFTTrainer practice, but "Instruction Tuning With Loss Over Instructions" (Shi et al. 2024) questions always masking the instruction.
+- **Chat templates**: model-specific special tokens (LIMA introduced an explicit EOT token distinct from EOS); mismatched templates silently degrade behavior.
+- **Hyperparameters**: small datasets overfit fast; LIMA found perplexity uncorrelated with quality, so gate on behavioral eval, not loss. Use packing for throughput; watch effective batch size and LR.
+- **DOK 2 Summary (collective):** For narrow-behavior SFT the choices that matter most are correct chat-template/token handling, masking the prompt so loss applies only to completions, and early stopping by behavioral eval rather than loss.
+
+### D. Preference optimization
+
+**DPO: Direct Preference Optimization** — Rafailov et al., Stanford, NeurIPS 2023. https://arxiv.org/abs/2305.18290. *Peer-reviewed / researcher.*
+- Reparameterizes the RLHF reward so the optimal policy has a closed form; trains directly on preference pairs with a simple classification loss — no separate reward model, no sampling during training.
+- Matches or beats PPO-based RLHF on sentiment control, summarization, and single-turn dialogue while being far simpler and more stable.
+- **DOK 2 Summary:** Makes preference tuning accessible on small hardware; the go-to "stretch" step after SFT when you have chosen/rejected pairs.
+
+**ORPO, KTO, SimPO, IPO** — Hong et al. 2024; Ethayarajh et al. 2024; Meng et al. 2024 (https://arxiv.org/abs/2405.14734); Azar et al. 2024. *Peer-reviewed / researcher.*
+- ORPO: reference-model-free, folds preference into SFT via an odds-ratio term (one model, one dataset), more efficient but hyperparameter-sensitive.
+- KTO: learns from unpaired binary (good/bad) signals — no preference pairs required.
+- SimPO: reference-free, length-normalized reward + target margin; reported to outperform DPO and ORPO in its own experiments while tolerating noisier labels.
+- IPO: addresses DPO overfitting with a theoretically grounded objective.
+- **DOK 2 Summary:** A menu trading off data format (paired vs unpaired), compute (reference model or not), and stability; choose by what feedback you can cheaply generate.
+
+*Collective note:* Argilla's RLHF overview (https://argilla.io/blog/mantisnlp-rlhf-part-9/) and post-training-stack write-ups stress that DPO alone optimizes generic preference; controllable/domain behavior often needs SFT first, then a preference pass, and that all these methods are β- and length-term–sensitive.
+
+### E. Compression / quantization & reasoning distillation
+
+**Distilling the Knowledge in a Neural Network** — Hinton, Vinyals, Dean, 2015. https://arxiv.org/abs/1503.02531. *Peer-reviewed / researcher.* Origin of soft-target knowledge distillation.
+
+**DeepSeek-R1 (distilled models)** — DeepSeek-AI, 2025. https://arxiv.org/abs/2501.12948. *Technical / researcher-practitioner.*
+- Fine-tuned six dense students (1.5B–70B, Qwen2.5 & Llama) on 800K reasoning traces from R1; SFT only, no RL stage.
+- Per the R1 technical report, DeepSeek-R1-Distill-Qwen-32B scores 72.6% on AIME 2024, 94.3% on MATH-500, and 57.2% on LiveCodeBench — results that significantly outperform previous open-source models and are comparable to o1-mini.
+- Key claim: distilling from a strong teacher beats running large-scale RL directly on a small model.
+- **DOK 2 Summary:** Landmark evidence that a hard capability (long-CoT reasoning) transfers into small models purely via SFT on teacher traces — though persistent gaps remain for ≤7B students.
+
+**s1: Simple Test-Time Scaling** — Muennighoff et al., Stanford, EMNLP 2025. https://arxiv.org/abs/2501.19393. *Peer-reviewed / researcher.*
+- Per the paper: "After supervised finetuning the Qwen2.5-32B-Instruct language model on s1K and equipping it with budget forcing, our model s1-32B exceeds o1-preview on competition math questions by up to 27% (MATH and AIME24)"; budget forcing (appending "Wait") scaled AIME24 from 50% to 57%.
+- s1K = 1,000 traces selected for difficulty, diversity, quality. Training on the full 59K vs the 1K cost 394 vs 7 H100-hours for marginal gains — data selection dominates.
+- Explicitly invokes LIMA's Superficial Alignment Hypothesis.
+- **DOK 2 Summary:** A second independent confirmation that ~1,000 well-chosen examples can activate a latent capability; the behavior is elicited, not taught from scratch.
+
+**Quantization formats** — GPTQ, AWQ, bitsandbytes (NF4), GGUF/llama.cpp. *Docs / practitioner.*
+- **DOK 2 Summary (collective):** Post-training quantization (GGUF for llama.cpp/CPU, AWQ/GPTQ for GPU) lets a tuned small model deploy on edge; 4-bit is the practical sweet spot.
+
+### F. Small-model landscape
+
+**SmolLM3-3B** — Hugging Face, released July 8, 2025. https://huggingface.co/HuggingFaceTB/SmolLM3-3B. *Technical / practitioner.*
+- 3B, trained on 11.2T tokens; dual reasoning (think/no_think); 64k context (128k via YaRN); fully open (data mixture, configs, 100+ intermediate checkpoints). Trained on 384 H100s for 24 days.
+- Outperforms Llama-3.2-3B and Qwen2.5-3B; competitive with Qwen3-4B and Gemma3-4B. Instruct variant optimized for reasoning and tool use.
+- **DOK 2 Summary:** Best current fully-open small base for tuning, with a documented recipe and a strong instruct variant.
+
+*Collective note:* **Qwen3 (0.6/1.7/4B), Llama 3.2 (1B/3B), Gemma 3 small, Phi family, SmolLM2 (135M/360M/1.7B)** are the practical base pool. Instruct variants ship chat templates and instruction-following priors; base variants give a cleaner slate but need format teaching. Tokenizer/number-tokenization differences matter (Goat attributed arithmetic gains to LLaMA's consistent digit tokenization).
+
+### G. Evaluation & LLM-as-judge
+
+**Judging LLM-as-a-Judge with MT-Bench and Chatbot Arena** — Zheng et al. 2023. https://arxiv.org/abs/2306.05685. *Peer-reviewed / researcher.*
+- Per the paper: "strong LLM judges like GPT-4 can match both controlled and crowdsourced human preferences well, achieving over 80% agreement, the same level of agreement between humans" (validated on ~3K controlled expert votes + ~3K crowdsourced votes).
+- Documents position bias (most judges favor the first answer; only GPT-4 stays consistent in >60% of swapped cases), verbosity bias, and self-enhancement bias (judges favor their own outputs). Independent studies measure length bias around +17% for LLM judges vs ~+13% for humans.
+- **DOK 2 Summary:** LLM-as-judge is scalable and roughly human-aligned but carries measurable biases — always randomize position, control length, and avoid judging with the same model family.
+
+**Hamel Husain — Your AI Product Needs Evals / LLM-as-a-Judge / Evals FAQ** (hamel.dev). https://hamel.dev/blog/posts/evals/. *Technical blog / practitioner.*
+- Error analysis first: read ~100 traces; stop when ~20 traces reveal no new failure mode ("theoretical saturation").
+- Use a single domain-expert "benevolent dictator"; build a custom, friction-free data-viewing tool. Prefer binary pass/fail over 1–5 scales ("Critique Shadowing"); pass rate is a product decision, not necessarily 100%.
+- Per the Evals FAQ: "In the projects we've worked on, we've spent 60-80% of our development time on error analysis and evaluation"; he notes a ~70% pass rate can indicate an eval that is actually stress-testing the app.
+- **DOK 2 Summary:** Build evals before/alongside the model; the eval harness IS the improvement flywheel and the debugging infrastructure.
+
+*Collective note:* **G-Eval** (Liu et al. 2023) uses CoT + form-filling for judge scoring; **JSONSchemaBench** (https://arxiv.org/abs/2501.10868) shows models still struggle with real-world schemas. Watch for contamination, overfitting to the judge, and benchmark gaming.
+
+### H. Reliability & structured output
+
+**Constrained decoding — Outlines, XGrammar, Guidance, llama.cpp GBNF; JSONSchemaBench** — Willard & Louf 2023; Dong et al. 2024 (XGrammar); https://arxiv.org/abs/2501.10868. *Docs + peer-reviewed / practitioner.*
+- FSM/token-masking sets invalid-token logits to −∞, guaranteeing schema-valid output; Outlines compiles JSON schemas for ~O(1) valid-token lookup per step.
+- Overhead ranges from minimal to ~2–5× for naive implementations; XGrammar is current SOTA for low overhead. Output quality can suffer when constraints force the model off its preferred tokens, but constrained decoding sometimes IMPROVES task performance.
+- **DOK 2 Summary:** For structured-output behaviors, constrained decoding guarantees form while fine-tuning improves the model's tendency to produce correct content within that form — complementary, not substitutes.
+
+### I. Failure modes & limits (dedicated strand)
+
+**GSM-Symbolic** — Mirzadeh et al., Apple, 2024 (ICLR 2025). https://arxiv.org/abs/2410.05229. *Peer-reviewed / researcher.*
+- All tested models drop accuracy when only numbers change in a template; performance degrades further as clause count rises.
+- Per the paper: "adding seemingly relevant but ultimately irrelevant information to problems, we demonstrate substantial performance drops (up to 65%) across all state-of-the-art models" — Phi-3-mini experienced over a 65% drop on the GSM-NoOp variant.
+- Interpretation: reasoning resembles sophisticated pattern matching, not robust logic. **Contested:** Ivanova and others critique the statistical rigor; treat as evidence of fragility, not proof of "no reasoning."
+
+**Faith and Fate: Limits of Transformers on Compositionality** — Dziri et al., NeurIPS 2023. https://arxiv.org/abs/2305.18654. *Peer-reviewed / researcher.*
+- GPT-4 zero-shot: 59% on 3×3-digit multiplication, dropping to 4% on 4×4; a few-shot scratchpad lifts 3×3 to 92% but stays near 0 on the hardest cases.
+- Transformers reduce compositional reasoning to "linearized subgraph matching"; under stated assumptions the probability of error converges toward 1 as problem size grows. Exhaustive fine-tuning (~1.8M multiplication pairs) generalized in-distribution but "utterly failed" out-of-distribution.
+
+**Why Language Models Hallucinate** — Kalai, Nachum, Vempala, Zhang (OpenAI/Georgia Tech), 2025. https://arxiv.org/abs/2509.04664. *Researcher.*
+- Frames hallucination as statistical error: generative error rate is lower-bounded by the "Is-It-Valid" binary misclassification rate — even with clean data, generating valid outputs is statistically harder than classifying validity.
+- Post-training persists/worsens hallucination because benchmarks reward confident guessing over "I don't know"; the proposed fix is reworking eval metrics to reward calibrated uncertainty/abstention.
+
+**Lost in the Middle: How Language Models Use Long Contexts** — Liu et al., TACL 2024. https://arxiv.org/abs/2307.03172. *Peer-reviewed / researcher.*
+- U-shaped accuracy: models use info at the start/end of context well and degrade sharply in the middle, even in explicitly long-context models.
+
+**Are Emergent Abilities of Large Language Models a Mirage?** — Schaeffer, Miranda, Koyejo, Stanford, NeurIPS 2023. https://arxiv.org/abs/2304.15004. *Peer-reviewed / researcher.*
+- Core claim: apparent "emergence" appears "due to the researcher's choice of metric rather than due to fundamental changes in model behavior with scale." Nonlinear/discontinuous metrics (exact match) manufacture sharp jumps; linear/continuous metrics (token edit distance, Brier score) show smooth, predictable scaling. They even *induce* apparent emergence in vision models by choosing metrics.
+
+**The Reversal Curse: LLMs trained on "A is B" fail to learn "B is A"** — Berglund et al., ICLR 2024. https://arxiv.org/abs/2309.12288. *Peer-reviewed / researcher.*
+- Models trained on "A is B" do not generalize to "B is A": "near 0% accuracy on reversals" across GPT-3-350M, Llama-7B, and GPT-3-175B; the log-probability of the correct reversed name is no higher than a random name. Data augmentation with paraphrases did not fix it. (In-context, models CAN reverse; the curse is about stored/trained knowledge.)
+
+**An Empirical Study of Catastrophic Forgetting in LLMs During Continual Fine-tuning** — Luo et al., 2023 (EMNLP 2025 proceedings). https://arxiv.org/abs/2308.08747. *Peer-reviewed / researcher.*
+- Catastrophic forgetting observed across 1B–7B models, and severity INTENSIFIES with scale during continual instruction tuning. Decoder-only BLOOMZ forgets less than encoder-decoder mT0. General instruction tuning (Alpaca vs LLaMA) mitigates forgetting; continual tuning can also reduce some biases (e.g., gender bias).
+
+**Alignment tax** — Ouyang et al. (InstructGPT), NeurIPS 2022. https://arxiv.org/abs/2203.02155; confirmed by Lin et al., EMNLP 2024, https://arxiv.org/abs/2309.06256.
+- InstructGPT coined the term: RLHF "comes at the cost of lower performance on certain tasks," with regressions on SQuAD, DROP, HellaSwag, and WMT'15 Fr→En. Mitigation: PPO-ptx (mixing pretraining-distribution gradients into PPO) largely closes the gap without hurting labeler scores. Lin et al. independently confirm the tax on OpenLLaMA-3B/Mistral-7B and note DPO induces less tax than other RLHF algorithms.
+
+**DOK 2 Summary (collective for I):** Small (and large) LMs fail systematically at compositional/multi-step reasoning, robustness to irrelevant info, symmetric fact retrieval, middle-of-context use, and calibrated uncertainty. Fine-tuning a narrow behavior can cause narrow forgetting and an alignment tax. Design evals to probe these exact fragilities.
+
+### J. Practitioner playbooks
+- **Hamel Husain** (evals), **Sebastian Raschka** (LoRA experiments; "Build a Reasoning Model From Scratch"), **Unsloth / Axolotl** docs (fast QLoRA recipes; HF alignment-handbook), **Argilla / distilabel** (data + preference pipelines).
+- **DOK 2 Summary:** The consensus workflow — define behavior + eval → generate/curate teacher data → QLoRA SFT → base-vs-tuned judge eval → optional DPO → quantize/deploy.
+
+### K. Forums / community
+- r/LocalLLaMA, Hugging Face forums, Unsloth/Axolotl Discords, Hacker News threads on QLoRA/DeepSeek-R1. Useful for hardware-specific gotchas, chat-template bugs, and reproductions; treat single-poster claims as anecdotes to verify.
+
+## Recommendations
+
+**Stage 0 — Define and instrument (before any training).** Write the ONE behavior as a falsifiable spec. Build the eval harness first: a held-out behavioral set plus an adversarial set that perturbs numbers, injects irrelevant clauses (GSM-Symbolic style), reverses relations (reversal curse), and shifts key info to the middle (lost-in-the-middle). Decide the judge protocol now — binary pass/fail, randomized answer order, a different model family as judge. *Benchmark that gates progress:* baseline the untuned model on this harness; the whole project is measured as the base-vs-tuned delta.
+
+**Stage 1 — Data.** Generate ~1,000–2,000 examples from a frontier teacher, distilling the *process* (reasoning traces/explanations), then filter for quality and diversity (AlpaGasus-style). Use distilabel/Argilla for pipelines. *Threshold to add more data:* only if the base-vs-tuned delta plateaus below target with clean data — that signals a missing latent capability, not a data-quantity problem.
+
+**Stage 2 — Train.** QLoRA (NF4, double quant) on a fully-open small base (SmolLM3-3B or Qwen3-1.7B/4B). Defaults: target all modules, α=2r, r≈16 (raise to 64–256 only if the target metric is capacity-bound), ≥3–4 epochs, sweep LR (LoRA is LR-sensitic). Mask the prompt (loss on completions only); verify the exact chat template. Early-stop on the behavioral eval, not loss. *Escalate to full FT or high-rank LoRA if:* the behavior is a genuinely new hard skill and low-rank LoRA underperforms full FT on the target metric.
+
+**Stage 3 — Preference tuning (stretch).** Only after SFT clears most of the target. Build chosen/rejected pairs (or unpaired good/bad for KTO) and run DPO (or ORPO to fold it into one stage). Re-run the full eval to check for an alignment tax — regression on base capabilities. *Threshold to keep it:* preference tuning must improve the target behavior without dropping retained-capability checks.
+
+**Stage 4 — Reliability & deploy.** Add constrained decoding (Outlines/XGrammar) for any structured output; measure the quality cost vs the validity gain. Quantize to GGUF (llama.cpp) or AWQ/GPTQ for deployment. *Kill-switch:* if constrained decoding measurably degrades content quality and the base is already schema-reliable, drop it.
+
+## Caveats
+- **Contested reasoning claims.** GSM-Symbolic's "not genuine reasoning" framing is disputed (Ivanova and others critique statistical rigor); treat it as strong evidence of *fragility*, not proof of no reasoning.
+- **Vendor vs independent.** DeepSeek-R1, SmolLM3, and QLoRA headline numbers are self-reported by the authors/vendors; the s1, LIMA, MT-Bench, GSM-Symbolic, Faith-and-Fate, and LoRA-Learns-Less findings are peer-reviewed but some rely on GPT-4-as-judge, which carries the biases documented in Section G.
+- **Alignment-tax magnitude is method-dependent.** InstructGPT quantifies regressions qualitatively; the headline drop is largely mitigated by PPO-ptx and DPO, so the "tax" is real but not fixed — measure it on your own benchmarks.
+- **Scale gap in the evidence.** Several marquee results (LIMA-65B, s1-32B, Guanaco-65B, Faith-and-Fate on GPT-4) are on models much larger than the 0.6B–4B target range; the *mechanisms* (superficial alignment, forgetting, compositional limits) transfer, but exact numbers will not. Small models show these failure modes at least as strongly.
+- **Fast-moving field.** Model releases (SmolLM3, Qwen3, DeepSeek-R1) and preference methods (SimPO/ORPO/KTO) are recent; recheck for newer bases and recipes before committing.
+- **Two searches were cut short by budget** (a direct pull of the emergent-abilities and reversal-curse primary PDFs); those facts were verified via a dedicated sub-search against the primary arXiv abstracts and are cited accordingly.

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

@@ -0,0 +1,287 @@
+# 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).

pyproject.toml

@@ -0,0 +1,24 @@
+[build-system]
+requires = ["setuptools>=68"]
+build-backend = "setuptools.build_meta"
+
+[project]
+name = "mathcompose"
+version = "0.1.0"
+description = "Two <=4B math models (generative verifier + solution generator) that demonstrate the generator-verifier gap."
+requires-python = ">=3.10"
+dynamic = ["dependencies"]
+
+[tool.setuptools.packages.find]
+where = ["src"]
+
+[tool.setuptools.dynamic]
+dependencies = { file = ["requirements.txt"] }
+
+[tool.pytest.ini_options]
+testpaths = ["tests"]
+addopts = "-q"
+markers = [
+    "network: test hits the network (HF Hub); skip with -m 'not network'",
+    "slow: slow test (loads a model)",
+]

requirements-gpu.txt

@@ -0,0 +1,9 @@
+# Extra deps for the GPU training/inference path (Colab / Modal / RunPod).
+# Install on top of requirements.txt on a CUDA box:
+#   pip install -r requirements.txt -r requirements-gpu.txt
+#
+# NOTE: install a CUDA build of torch first (Colab ships one). The CPU box uses
+# torch==*+cpu, which cannot run 4-bit QLoRA.
+bitsandbytes>=0.43        # 4-bit NF4 kernels for QLoRA (requires CUDA)
+# Optional speedup (UNCONFIRMED against transformers 5.13 — pin transformers down if you use it):
+#   pip install unsloth

requirements.txt

@@ -0,0 +1,19 @@
+# CPU / harness dependencies (already present in the dev box).
+# Pinned loosely to the versions this project was built and verified against.
+transformers>=5.13,<6
+trl>=1.7,<2
+peft>=0.19,<0.20
+accelerate>=1.14
+datasets>=5.0
+huggingface_hub>=1.22
+tokenizers>=0.22
+safetensors>=0.8
+sympy>=1.12
+pyyaml>=6
+numpy>=2.0
+pandas>=2.2
+tqdm>=4.66
+# Teacher clients are optional and imported lazily; install the one you use:
+#   pip install anthropic        # for the Anthropic teacher
+#   pip install openai           # for the OpenAI teacher
+# Neither is required for CPU smoke tests (DummyTeacher has no external deps).

results/teacher_bakeoff.md

@@ -0,0 +1,28 @@
+# Teacher bake-off — Model G (solution generator)
+
+Data-driven teacher selection. 40 NuminaMath-CoT problems, one solution each,
+graded by boxed-answer equivalence (`scripts/teacher_bakeoff.py`).
+
+    scripts/teacher_bakeoff.py --models gpt-5.6-sol claude-opus-4-8 claude-sonnet-5 --n 40
+
+| model | keep-rate | median tok | p90 tok | % over 2048 | sec/ex |
+|---|---|---|---|---|---|
+| **claude-opus-4-8** | **57%** | 155 | 703 | 0% | 6.7 |
+| gpt-5.6-sol | 32% | 103 | 324 | 0% | 10.4 |
+| claude-sonnet-5 | 12% | 224 | 691 | 0% | 9.9 |
+
+**Winner: `claude-opus-4-8`** — highest keep-rate (most usable data per call),
+fastest, and traces fit the 4096-token student ceiling with room to spare.
+
+`claude-fable-5` was requested but **excluded**: 403 on both routes (AWS Bedrock
+Marketplace access not granted on this gateway account).
+
+**Caveats:** n=40 is noisy; absolute keep-rates are depressed by NuminaMath
+difficulty + strict grading + format adherence, not just model capability — the
+*relative* ranking is the signal. For the real G build, rejection sampling with
+`--max-attempts > 1` lifts the effective keep-rate.
+
+## Teacher assignments
+- **Model G** (solution generator): `claude-opus-4-8`.
+- **Model V** (critique writer; label already known from PRM800K → easier job):
+  `claude-haiku-4-5` (cheaper) is sufficient; use `claude-opus-4-8` if budget allows.

scripts/check_teacher.py

@@ -0,0 +1,45 @@
+"""Verify the teacher gateway is reachable and returns text.
+
+    python scripts/check_teacher.py                 # default: promptlens
+    python scripts/check_teacher.py --teacher openai
+
+Loads .env, sends a 1-line prompt, prints the reply. Exits non-zero on failure.
+"""
+import argparse
+import sys
+from pathlib import Path
+
+sys.path.insert(0, str(Path(__file__).resolve().parents[1] / "src"))
+
+from mathcompose.teachers import get_teacher  # noqa: E402
+
+
+def main() -> int:
+    ap = argparse.ArgumentParser()
+    ap.add_argument("--teacher", default="promptlens")
+    ap.add_argument("--model", default=None)
+    ap.add_argument("--prompt", default="Reply with exactly: pong")
+    args = ap.parse_args()
+
+    try:
+        teacher = get_teacher(args.teacher, **({"model": args.model} if args.model else {}))
+    except Exception as e:
+        print(f"[FAIL] could not build teacher '{args.teacher}': {e}")
+        return 1
+
+    who = f"{args.teacher} (model={getattr(teacher, 'model', '?')}, base_url={getattr(teacher, 'base_url', None)})"
+    print(f"calling {who} ...")
+    try:
+        reply = teacher.complete(
+            [{"role": "user", "content": args.prompt}], temperature=0.0, max_tokens=32
+        )
+    except Exception as e:
+        print(f"[FAIL] teacher call errored: {type(e).__name__}: {e}")
+        return 1
+
+    print(f"[OK] reply: {reply!r}")
+    return 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())

scripts/download_prm800k.py

@@ -0,0 +1,48 @@
+"""Download PRM800K step-label files (OpenAI, MIT) into data/raw/prm800k/.
+
+    python scripts/download_prm800k.py                 # phase2_train (what we use)
+    python scripts/download_prm800k.py --all           # all four phase files
+
+The GitHub raw URLs serve the real JSONL (schema: question/label/steps/...),
+which is exactly what mathcompose.datagen.prm800k_loader expects.
+"""
+import argparse
+import sys
+import urllib.request
+from pathlib import Path
+
+BASE = "https://github.com/openai/prm800k/raw/main/prm800k/data"
+FILES = ["phase2_train.jsonl", "phase1_train.jsonl", "phase2_test.jsonl", "phase1_test.jsonl"]
+
+
+def download(name: str, out_dir: Path) -> None:
+    url = f"{BASE}/{name}"
+    dest = out_dir / name
+    dest.parent.mkdir(parents=True, exist_ok=True)
+    print(f"downloading {name} -> {dest}")
+
+    def _hook(block, bsize, total):
+        if total > 0:
+            pct = min(100, block * bsize * 100 // total)
+            sys.stdout.write(f"\r  {pct:3d}%  ({block * bsize / 1e6:.0f} MB)")
+            sys.stdout.flush()
+
+    urllib.request.urlretrieve(url, dest, reporthook=_hook)
+    print(f"\r  done: {dest.stat().st_size / 1e6:.1f} MB{' ' * 10}")
+
+
+def main() -> int:
+    ap = argparse.ArgumentParser()
+    ap.add_argument("--out-dir", default="data/raw/prm800k")
+    ap.add_argument("--all", action="store_true", help="download all four phase files")
+    args = ap.parse_args()
+    names = FILES if args.all else ["phase2_train.jsonl"]
+    for n in names:
+        download(n, Path(args.out_dir))
+    print("\nNext: python -m mathcompose.data.build_verifier_dataset "
+          f"--prm800k {args.out_dir}/phase2_train.jsonl --teacher promptlens --limit 15000")
+    return 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())

scripts/publish_hf.py

@@ -0,0 +1,99 @@
+"""Publish to HF Hub: the V dataset (deliverable) + a self-contained code+data
+snapshot the Colab notebook can pull with just an HF token (no GitHub needed).
+
+    # after setting HF_TOKEN in .env:
+    python scripts/publish_hf.py --dataset --code
+
+Creates:
+  <user>/mathcompose-verifier   (dataset repo)  — data/verifier/*.jsonl + card
+  <user>/mathcompose            (model repo)     — full code + data/verifier
+                                                    (excludes data/raw, runs, caches)
+The Colab notebook snapshot_downloads the model repo, `pip install -e .`, trains.
+"""
+import argparse
+import sys
+from pathlib import Path
+
+sys.path.insert(0, str(Path(__file__).resolve().parents[1] / "src"))
+from mathcompose.common.env import load_dotenv, first_env  # noqa: E402
+
+ROOT = Path(__file__).resolve().parents[1]
+
+DATASET_CARD = """---
+license: mit
+task_categories: [text-generation]
+tags: [math, process-verification, ProcessBench, PRM800K, mathcompose]
+---
+
+# mathcompose — Model V (process verifier) SFT data
+
+First-error-localization critiques for training a small generative math verifier.
+Each row: a problem + a step-indexed candidate solution (`prompt`) and a
+paragraph-by-paragraph critique ending in `\\boxed{{k}}` (`completion`), where `k`
+is the 0-based index of the first erroneous step (`-1` = all correct).
+
+- **Labels** are ground truth from **PRM800K** (OpenAI, MIT).
+- **Critiques** distilled from **claude-opus-4-8** (rationalization conditioned on
+  the known label; the boxed index is stamped authoritatively, not trusted to the teacher).
+- **Deduped** against ProcessBench + MATH-500 (no eval contamination).
+- `train.jsonl`/`val.jsonl` are class-balanced (~50/50 erroneous/all-correct);
+  `*_full.jsonl` keep the natural PRM800K distribution.
+
+Built by the mathcompose harness. Eval target: ProcessBench first-error F1.
+"""
+
+
+def main() -> int:
+    ap = argparse.ArgumentParser()
+    ap.add_argument("--dataset", action="store_true", help="publish the dataset repo")
+    ap.add_argument("--code", action="store_true", help="publish the code+data snapshot repo")
+    ap.add_argument("--user", default=None, help="HF username/org (default: from token)")
+    ap.add_argument("--dataset-repo", default=None)
+    ap.add_argument("--code-repo", default=None)
+    ap.add_argument("--private", action="store_true")
+    args = ap.parse_args()
+    if not (args.dataset or args.code):
+        args.dataset = args.code = True
+
+    load_dotenv()
+    token = first_env(["HF_TOKEN", "HUGGING_FACE_HUB_TOKEN", "HUGGINGFACE_TOKEN"])
+    if not token:
+        print("No HF token — set HF_TOKEN in .env."); return 1
+
+    from huggingface_hub import HfApi
+    api = HfApi(token=token)
+    user = args.user or api.whoami()["name"]
+    ds_repo = args.dataset_repo or f"{user}/mathcompose-verifier"
+    code_repo = args.code_repo or f"{user}/mathcompose"
+
+    if args.dataset:
+        print(f"publishing dataset -> {ds_repo}")
+        api.create_repo(ds_repo, repo_type="dataset", exist_ok=True, private=args.private)
+        (ROOT / "data/verifier/README.md").write_text(DATASET_CARD)
+        api.upload_folder(
+            folder_path=str(ROOT / "data/verifier"),
+            repo_id=ds_repo, repo_type="dataset",
+            allow_patterns=["*.jsonl", "README.md"],
+        )
+        print(f"  https://huggingface.co/datasets/{ds_repo}")
+
+    if args.code:
+        print(f"publishing code+data snapshot -> {code_repo}")
+        api.create_repo(code_repo, repo_type="model", exist_ok=True, private=args.private)
+        api.upload_folder(
+            folder_path=str(ROOT),
+            repo_id=code_repo, repo_type="model",
+            ignore_patterns=[
+                "data/raw/*", "**/__pycache__/*", "*.egg-info/*", "**/*.pyc",
+                "runs/*", ".git/*", ".pytest_cache/*", "data/verifier/*_full.jsonl",
+                ".env", ".env.*",
+            ],
+        )
+        print(f"  https://huggingface.co/{code_repo}")
+
+    print("\nColab: snapshot_download the model repo, `pip install -e .`, then train.")
+    return 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())

scripts/rebalance_verifier.py

@@ -0,0 +1,53 @@
+"""Rebalance the Model-V dataset by downsampling all-correct (-1) examples.
+
+ProcessBench F1 = harmonic_mean(acc_error, acc_correct), so a training set skewed
+toward -1 biases V to over-accept, crushing acc_error and thus F1. This makes a
+~balanced default (correct:erroneous = --ratio) and preserves the original.
+
+    python scripts/rebalance_verifier.py            # train.jsonl + val.jsonl, ratio 1.0
+    python scripts/rebalance_verifier.py --ratio 1.5
+
+Original files are moved to *_full.jsonl; the balanced set takes the canonical name.
+"""
+import argparse
+import json
+import random
+from pathlib import Path
+
+
+def rebalance(path: Path, ratio: float, seed: int) -> tuple[int, int, int]:
+    rows = [json.loads(l) for l in path.read_text().splitlines() if l.strip()]
+    err = [r for r in rows if r.get("first_error_index", -1) != -1]
+    cor = [r for r in rows if r.get("first_error_index", -1) == -1]
+    rng = random.Random(seed)
+    rng.shuffle(cor)
+    keep_cor = cor[: int(round(len(err) * ratio))]
+    balanced = err + keep_cor
+    rng.shuffle(balanced)
+
+    full = path.with_name(path.stem + "_full.jsonl")
+    if not full.exists():
+        path.rename(full)  # preserve original once
+    with open(path, "w") as f:
+        for r in balanced:
+            f.write(json.dumps(r, ensure_ascii=False) + "\n")
+    return len(err), len(keep_cor), len(balanced)
+
+
+def main() -> int:
+    ap = argparse.ArgumentParser()
+    ap.add_argument("--dir", default="data/verifier")
+    ap.add_argument("--ratio", type=float, default=1.0, help="correct:erroneous ratio to keep")
+    ap.add_argument("--seed", type=int, default=0)
+    args = ap.parse_args()
+    for name in ("train.jsonl", "val.jsonl"):
+        p = Path(args.dir) / name
+        if not p.exists():
+            continue
+        e, c, t = rebalance(p, args.ratio, args.seed)
+        print(f"{name}: {t} rows (erroneous {e}, all-correct {c}); original -> {p.stem}_full.jsonl")
+    return 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())

scripts/smoke_all.sh

@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+# CPU smoke suite — proves the harness works before spending GPU.
+# Fast logic-only tests by default; add --full to include the tiny-model
+# train/eval and the HF dataset-schema probes (needs network).
+set -euo pipefail
+cd "$(dirname "$0")/.."
+
+export HF_HUB_DISABLE_PROGRESS_BARS=1
+export TOKENIZERS_PARALLELISM=false
+
+if [[ "${1:-}" == "--full" ]]; then
+  echo ">> full smoke suite (logic + tiny-model train/eval + dataset probes)"
+  python -m pytest -q -p no:cacheprovider
+else
+  echo ">> fast smoke suite (pure logic; no model/network)"
+  python -m pytest -q -m "not slow and not network" -p no:cacheprovider
+  echo
+  echo "   (run './scripts/smoke_all.sh --full' to also exercise training + datasets)"
+fi

scripts/teacher_bakeoff.py

@@ -0,0 +1,99 @@
+"""Pick a teacher empirically: keep-rate + trace-length-vs-ceiling per model.
+
+    # after setting TFY_API_KEY in .env:
+    python scripts/teacher_bakeoff.py --models claude-fable-5 gpt-5.6-sol --n 40
+
+For each model it distills N solutions (same problems), grades the boxed answer,
+and reports: keep-rate (higher = better/cheaper data), median/p90 trace length in
+STUDENT tokens, and the fraction that would overflow the generator's max_length
+(dropped). Highest keep-rate that mostly fits the ceiling wins.
+
+The V-critique job is easier (label is known from PRM800K), so a lighter/cheaper
+model usually suffices there regardless of who wins for G.
+"""
+import argparse
+import statistics as stats
+import sys
+import time
+from pathlib import Path
+
+sys.path.insert(0, str(Path(__file__).resolve().parents[1] / "src"))
+
+from mathcompose.common.chat import load_tokenizer  # noqa: E402
+from mathcompose.common.math_grade import extract_last_boxed, grade_answer  # noqa: E402
+from mathcompose.datagen.gen_generator_data import Problem, synthesize_solution  # noqa: E402
+from mathcompose.teachers import get_teacher  # noqa: E402
+
+
+def load_problems(source, split, n, problem_field, solution_field):
+    """Stream the source (no full download) and collect the first n problems that
+    have a parseable boxed gold answer."""
+    from datasets import load_dataset
+
+    ds = load_dataset(source, split=split, streaming=True)
+    out = []
+    for row in ds:
+        prob = row.get(problem_field)
+        ans = extract_last_boxed(row.get(solution_field) or "")
+        if prob and ans:
+            out.append(Problem(problem=prob, answer=ans))
+        if len(out) >= n:
+            break
+    return out
+
+
+def main() -> int:
+    ap = argparse.ArgumentParser()
+    ap.add_argument("--models", nargs="+", required=True, help="gateway model slugs to compare")
+    ap.add_argument("--teacher", default="promptlens")
+    ap.add_argument("--n", type=int, default=40)
+    ap.add_argument("--source", default="AI-MO/NuminaMath-CoT")
+    ap.add_argument("--split", default="train")
+    ap.add_argument("--problem-field", default="problem")
+    ap.add_argument("--solution-field", default="solution")
+    ap.add_argument("--max-tokens", type=int, default=2048, help="teacher output cap")
+    ap.add_argument("--ceiling", type=int, default=2048, help="generator max_length; traces over this are dropped")
+    ap.add_argument("--base-id", default="Qwen/Qwen2.5-Math-1.5B-Instruct")
+    args = ap.parse_args()
+
+    problems = load_problems(args.source, args.split, args.n, args.problem_field, args.solution_field)
+    print(f"loaded {len(problems)} problems from {args.source}\n")
+    tok = load_tokenizer(args.base_id)
+
+    rows = []
+    for slug in args.models:
+        teacher = get_teacher(args.teacher, model=slug)
+        kept, lens, t0 = 0, [], time.time()
+        for p in problems:
+            try:
+                sol = synthesize_solution(teacher, p.problem, temperature=0.7, max_tokens=args.max_tokens)
+            except Exception as e:
+                print(f"  [{slug}] call failed: {type(e).__name__}: {e}")
+                continue
+            n_tok = len(tok(sol)["input_ids"])
+            lens.append(n_tok)
+            if grade_answer(extract_last_boxed(sol), p.answer):
+                kept += 1
+        dt = time.time() - t0
+        n = len(lens) or 1
+        rows.append({
+            "model": slug,
+            "keep_rate": kept / len(problems),
+            "median_tok": int(stats.median(lens)) if lens else 0,
+            "p90_tok": int(sorted(lens)[int(0.9 * (len(lens) - 1))]) if lens else 0,
+            "over_ceiling": sum(1 for x in lens if x > args.ceiling) / n,
+            "sec_per_ex": dt / len(problems),
+        })
+
+    print(f"\n{'model':<24}{'keep':>8}{'med_tok':>9}{'p90_tok':>9}{'>ceil':>8}{'s/ex':>8}")
+    print("-" * 66)
+    for r in sorted(rows, key=lambda r: -r["keep_rate"]):
+        print(f"{r['model']:<24}{r['keep_rate']:>7.0%}{r['median_tok']:>9}{r['p90_tok']:>9}"
+              f"{r['over_ceiling']:>7.0%}{r['sec_per_ex']:>7.1f}")
+    print("\nPick the highest keep-rate whose p90_tok comfortably fits the ceiling "
+          f"({args.ceiling}). Set it via TFY_MODEL or --model at build time.")
+    return 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())

src/mathcompose/__init__.py

@@ -0,0 +1,14 @@
+"""mathcompose — two <=4B math models (generative verifier + solution generator)
+that together demonstrate the generator-verifier gap.
+
+Subpackages:
+  common   — chat templating, boxed-answer grading, config, seeding (no heavy deps)
+  teachers — pluggable frontier teacher clients (+ offline DummyTeacher)
+  datagen  — build V/G training data (PRM800K parsing, teacher distillation, dedup)
+  data     — V output schema + dataset builders
+  eval     — ProcessBench / PRMBench / MATH / composition metrics (objective, no judge)
+  train    — shared QLoRA SFT entrypoint
+  infer    — inference demo
+"""
+
+__version__ = "0.1.0"

src/mathcompose/common/__init__.py

@@ -0,0 +1,21 @@
+from .math_grade import (
+    extract_boxed,
+    extract_last_boxed,
+    extract_boxed_int,
+    grade_answer,
+    normalize_final_answer,
+    normalize_problem_text,
+)
+from .seeding import set_seed
+from .config import load_config
+
+__all__ = [
+    "extract_boxed",
+    "extract_last_boxed",
+    "extract_boxed_int",
+    "grade_answer",
+    "normalize_final_answer",
+    "normalize_problem_text",
+    "set_seed",
+    "load_config",
+]

src/mathcompose/common/chat.py

@@ -0,0 +1,108 @@
+r"""Prompt construction + tokenizer/chat-template helpers.
+
+Prompt builders are pure-Python (no heavy deps) so datagen and tests can build
+prompts without importing transformers. ``load_tokenizer`` is the only function
+that touches transformers, and it applies the Qwen2.5-Math pad-token fix.
+
+Model V speaks the *official ProcessBench critic prompt*: the solution is split
+into paragraphs, tagged and indexed from 0; V critiques each and returns the
+0-based index of the first erroneous paragraph in ``\boxed{}`` (``-1`` = all
+correct). Using ProcessBench's own format means the same model scores
+ProcessBench *and* reranks Model G with zero prompt divergence.
+"""
+from __future__ import annotations
+
+from typing import Optional
+
+# Qwen2.5-Math default CoT system prompt (do NOT use the TIR variant here).
+GENERATOR_SYSTEM = (
+    "Please reason step by step, and put your final answer within \\boxed{}."
+)
+
+VERIFIER_SYSTEM = (
+    "You are a meticulous math grader. You are given a problem and a candidate "
+    "solution split into indexed paragraphs. Critically review the solution one "
+    "paragraph at a time and find the FIRST paragraph that contains an error."
+)
+
+# The official ProcessBench critic instruction (verbatim intent).
+_VERIFIER_INSTRUCTION = (
+    "The following is a math problem and a solution (split into paragraphs, "
+    "enclosed with tags and indexed from 0):\n\n"
+    "[Math Problem]\n{problem}\n\n"
+    "[Solution]\n{tagged_steps}\n\n"
+    "Your task is to review and critique the solution paragraph by paragraph. "
+    "Once you identify an error in a paragraph, return the index of the paragraph "
+    "where the earliest error occurs. Otherwise, return the index of -1 (which "
+    "typically denotes \"all correct\").\n\n"
+    "Please put your final answer (i.e., the index) in \\boxed{{}}."
+)
+
+
+def tag_steps(steps: list[str]) -> str:
+    """Render a list of solution steps as indexed <paragraph_i> blocks."""
+    return "\n\n".join(
+        f"<paragraph_{i}>\n{s.strip()}\n</paragraph_{i}>" for i, s in enumerate(steps)
+    )
+
+
+def build_verifier_prompt(problem: str, steps: list[str]) -> str:
+    """User-turn content for Model V (ProcessBench critic format)."""
+    return _VERIFIER_INSTRUCTION.format(problem=problem.strip(), tagged_steps=tag_steps(steps))
+
+
+def verifier_messages(problem: str, steps: list[str]) -> list[dict]:
+    return [
+        {"role": "system", "content": VERIFIER_SYSTEM},
+        {"role": "user", "content": build_verifier_prompt(problem, steps)},
+    ]
+
+
+def build_generator_prompt(problem: str) -> str:
+    return problem.strip()
+
+
+def generator_messages(problem: str) -> list[dict]:
+    return [
+        {"role": "system", "content": GENERATOR_SYSTEM},
+        {"role": "user", "content": build_generator_prompt(problem)},
+    ]
+
+
+def split_into_steps(solution: str) -> list[str]:
+    """Split a free-form solution into paragraph 'steps' the way ProcessBench does
+    (double-newline separated, non-empty). Used when reranking G's own outputs."""
+    parts = [p.strip() for p in solution.replace("\r\n", "\n").split("\n\n")]
+    return [p for p in parts if p]
+
+
+# ----------------------------------------------------------------------------
+# Tokenizer (transformers) — only import when actually loading a model.
+# ----------------------------------------------------------------------------
+
+def load_tokenizer(base_id: str, pad_token: Optional[str] = "<|fim_pad|>"):
+    """Load the tokenizer and apply the Qwen pad-token fix.
+
+    Using <|endoftext|> as the pad token triggers infinite generations after
+    finetuning (documented Qwen2.5 gotcha); we pin a distinct pad token.
+    """
+    from transformers import AutoTokenizer
+
+    tok = AutoTokenizer.from_pretrained(base_id)
+    if pad_token and pad_token in tok.get_vocab():
+        tok.pad_token = pad_token
+    elif tok.pad_token is None:
+        tok.pad_token = tok.eos_token
+    # Base (non-chat) models and some tiny test tokenizers ship no chat template;
+    # fall back to a minimal ChatML so apply_chat_template always works.
+    if getattr(tok, "chat_template", None) is None:
+        tok.chat_template = _MINIMAL_CHATML
+    return tok
+
+
+_MINIMAL_CHATML = (
+    "{% for m in messages %}"
+    "{{ '<|im_start|>' + m['role'] + '\n' + m['content'] + '<|im_end|>\n' }}"
+    "{% endfor %}"
+    "{% if add_generation_prompt %}{{ '<|im_start|>assistant\n' }}{% endif %}"
+)

src/mathcompose/common/config.py

@@ -0,0 +1,33 @@
+"""Tiny YAML config loader with single-level `extends` inheritance and deep-merge.
+
+    cfg = load_config("configs/verifier_v.yaml")
+    cfg["model"]["base_id"]  # inherited from base.yaml, overridable per-file
+"""
+from __future__ import annotations
+
+import copy
+from pathlib import Path
+from typing import Any
+
+import yaml
+
+
+def _deep_merge(base: dict, override: dict) -> dict:
+    out = copy.deepcopy(base)
+    for k, v in override.items():
+        if isinstance(v, dict) and isinstance(out.get(k), dict):
+            out[k] = _deep_merge(out[k], v)
+        else:
+            out[k] = copy.deepcopy(v)
+    return out
+
+
+def load_config(path: str | Path) -> dict[str, Any]:
+    path = Path(path)
+    with open(path) as f:
+        cfg = yaml.safe_load(f) or {}
+    parent = cfg.pop("extends", None)
+    if parent:
+        parent_cfg = load_config(path.parent / parent)
+        cfg = _deep_merge(parent_cfg, cfg)
+    return cfg

src/mathcompose/common/env.py

@@ -0,0 +1,39 @@
+"""Minimal .env loader (no python-dotenv dependency).
+
+Parses simple KEY=VALUE lines (optionally `export KEY=VALUE`, quoted values,
+`#` comments) from a .env file and puts them in os.environ. Existing env vars
+win unless override=True.
+"""
+from __future__ import annotations
+
+import os
+from pathlib import Path
+
+
+def load_dotenv(path: str | Path = ".env", override: bool = False) -> bool:
+    p = Path(path)
+    if not p.exists():
+        return False
+    for raw in p.read_text().splitlines():
+        line = raw.strip()
+        if not line or line.startswith("#"):
+            continue
+        if line.startswith("export "):
+            line = line[len("export "):]
+        if "=" not in line:
+            continue
+        key, val = line.split("=", 1)
+        key = key.strip()
+        val = val.strip().strip('"').strip("'")
+        if override or key not in os.environ:
+            os.environ[key] = val
+    return True
+
+
+def first_env(names: list[str]) -> str | None:
+    """Return the first set-and-non-empty env var among names."""
+    for n in names:
+        v = os.environ.get(n)
+        if v:
+            return v
+    return None

src/mathcompose/common/io.py

@@ -0,0 +1,25 @@
+"""jsonl read/write helpers."""
+from __future__ import annotations
+
+import json
+from pathlib import Path
+from typing import Iterable, Iterator
+
+
+def write_jsonl(rows: Iterable[dict], path: str | Path) -> int:
+    path = Path(path)
+    path.parent.mkdir(parents=True, exist_ok=True)
+    n = 0
+    with open(path, "w") as f:
+        for r in rows:
+            f.write(json.dumps(r, ensure_ascii=False) + "\n")
+            n += 1
+    return n
+
+
+def read_jsonl(path: str | Path) -> Iterator[dict]:
+    with open(path) as f:
+        for line in f:
+            line = line.strip()
+            if line:
+                yield json.loads(line)

src/mathcompose/common/math_grade.py

@@ -0,0 +1,227 @@
+r"""Boxed-answer extraction and math-equivalence grading.
+
+Two independent jobs:
+
+1. ``extract_boxed_int`` — pull the integer inside the LAST ``\boxed{...}``.
+   Used by Model V, whose canonical output ends in ``\boxed{k}`` (first-error
+   index, ``-1`` = all steps correct). This is the ProcessBench primitive.
+
+2. ``grade_answer`` — decide whether a predicted final answer is mathematically
+   equivalent to the gold answer. Used by Model G's eval and by the data filter.
+   Best-effort: string normalization -> sympy simplify -> numeric fallback,
+   fully guarded so it degrades to a normalized string compare. Swap in
+   ``math_verify`` / the PRM800K sympy grader later if you want stricter grading.
+"""
+from __future__ import annotations
+
+import re
+from typing import Optional
+
+# ----------------------------------------------------------------------------
+# Boxed extraction (balanced-brace aware)
+# ----------------------------------------------------------------------------
+
+_BOXED_PREFIXES = (r"\boxed", r"\fbox")
+
+
+def _find_boxed_spans(text: str) -> list[str]:
+    """Return the *contents* of every ``\boxed{...}`` / ``\fbox{...}`` with
+    balanced-brace matching (so ``\boxed{\frac{1}{2}}`` returns ``\frac{1}{2}``)."""
+    results: list[str] = []
+    for prefix in _BOXED_PREFIXES:
+        start = 0
+        while True:
+            idx = text.find(prefix, start)
+            if idx == -1:
+                break
+            i = idx + len(prefix)
+            # skip whitespace, expect an opening brace
+            while i < len(text) and text[i] in " \t":
+                i += 1
+            if i >= len(text) or text[i] != "{":
+                # \boxed without braces, e.g. "\boxed -1" — grab the token
+                m = re.match(r"\s*(-?\d+)", text[idx + len(prefix):])
+                if m:
+                    results.append(m.group(1))
+                start = idx + len(prefix)
+                continue
+            depth = 0
+            j = i
+            while j < len(text):
+                if text[j] == "{":
+                    depth += 1
+                elif text[j] == "}":
+                    depth -= 1
+                    if depth == 0:
+                        break
+                j += 1
+            results.append(text[i + 1 : j])
+            start = j + 1
+    return results
+
+
+def extract_boxed(text: str) -> Optional[str]:
+    """Contents of the FIRST boxed expression, or None."""
+    spans = _find_boxed_spans(text)
+    return spans[0] if spans else None
+
+
+def extract_last_boxed(text: str) -> Optional[str]:
+    """Contents of the LAST boxed expression, or None. This is the final answer."""
+    spans = _find_boxed_spans(text)
+    return spans[-1] if spans else None
+
+
+def extract_boxed_int(text: str) -> Optional[int]:
+    """Integer inside the LAST boxed expression (Model V's first-error index).
+
+    Tolerant of ``\boxed{-1}``, ``\boxed{ 3 }``, ``\boxed{\text{-1}}``, and a
+    bare trailing ``-1`` if no box is present at all.
+    """
+    span = extract_last_boxed(text)
+    if span is not None:
+        m = re.search(r"-?\d+", span)
+        if m:
+            return int(m.group())
+    # Last-ditch: a trailing integer on the final non-empty line.
+    for line in reversed([l for l in text.strip().splitlines() if l.strip()]):
+        m = re.search(r"(-?\d+)\s*$", line.strip())
+        if m:
+            return int(m.group(1))
+    return None
+
+
+# ----------------------------------------------------------------------------
+# Answer normalization + equivalence
+# ----------------------------------------------------------------------------
+
+_SUBST = [
+    (r"\\left", ""),
+    (r"\\right", ""),
+    (r"\\!", ""),
+    (r"\\,", ""),
+    (r"\\;", ""),
+    (r"\\ ", " "),
+    (r"\\%", ""),
+    (r"\\\$", ""),
+    (r"\\cdot", "*"),
+    (r"\\times", "*"),
+    (r"\\div", "/"),
+    (r"\\pi", "pi"),
+    (r"\\pm", ""),
+]
+
+
+def _strip_text_wrappers(s: str) -> str:
+    # \text{...}, \mathrm{...}, \mbox{...} -> inner
+    for macro in ("text", "mathrm", "mbox", "textbf", "mathbf"):
+        s = re.sub(r"\\" + macro + r"\{([^{}]*)\}", r"\1", s)
+    return s
+
+
+def _normalize_answer(s: str) -> str:
+    if s is None:
+        return ""
+    s = str(s).strip()
+    # strip surrounding math delimiters and whitespace
+    s = s.replace("$", "").replace("\\(", "").replace("\\)", "")
+    s = s.replace("\\[", "").replace("\\]", "")
+    s = _strip_text_wrappers(s)
+    for pat, rep in _SUBST:
+        s = re.sub(pat, rep, s)
+    s = s.replace("°", "")          # degree sign
+    s = s.replace("^{\\circ}", "").replace("^\\circ", "").replace("\\circ", "")
+    s = s.replace(" ", "")
+    s = s.rstrip(".")
+    # thousands separators inside numbers: 1,000 -> 1000
+    s = re.sub(r"(?<=\d),(?=\d{3}\b)", "", s)
+    # trailing units words like "dollars", "cm" — conservative: only strip a
+    # trailing alpha run if the rest is numeric-ish.
+    return s
+
+
+def _latex_to_sympy(s: str) -> str:
+    """Very small latex->sympy-parseable rewrite (no latex2sympy dependency)."""
+    # \frac{a}{b} -> ((a)/(b))  (repeat for nesting)
+    for _ in range(6):
+        new = re.sub(r"\\d?frac\{([^{}]*)\}\{([^{}]*)\}", r"((\1)/(\2))", s)
+        new = re.sub(r"\\sqrt\{([^{}]*)\}", r"sqrt(\1)", new)
+        new = re.sub(r"\\sqrt\[(\d+)\]\{([^{}]*)\}", r"(\2)**(1/\1)", new)
+        if new == s:
+            break
+        s = new
+    s = s.replace("{", "(").replace("}", ")")
+    s = re.sub(r"\^", "**", s)
+    s = s.replace("\\", "")
+    return s
+
+
+def _try_float(s: str) -> Optional[float]:
+    try:
+        return float(s)
+    except (ValueError, TypeError):
+        return None
+
+
+def normalize_final_answer(s: str) -> str:
+    """Public normalizer for bucketing answers in majority voting."""
+    return _normalize_answer(s)
+
+
+def grade_answer(pred: Optional[str], gold: Optional[str]) -> bool:
+    """True iff `pred` is mathematically equivalent to `gold`.
+
+    Order: exact normalized string -> numeric -> sympy simplify. Fully guarded.
+    """
+    if pred is None or gold is None:
+        return False
+    p, g = _normalize_answer(pred), _normalize_answer(gold)
+    if p == "" and g == "":
+        return False
+    if p == g:
+        return True
+
+    # numeric comparison
+    pf, gf = _try_float(p), _try_float(g)
+    if pf is not None and gf is not None:
+        return abs(pf - gf) <= 1e-6 * max(1.0, abs(gf))
+
+    # symbolic comparison
+    try:
+        import sympy as sp
+        from sympy.parsing.sympy_parser import (
+            parse_expr,
+            standard_transformations,
+            implicit_multiplication_application,
+        )
+
+        transforms = standard_transformations + (
+            implicit_multiplication_application,
+        )
+        ep = parse_expr(_latex_to_sympy(p), transformations=transforms, evaluate=True)
+        eg = parse_expr(_latex_to_sympy(g), transformations=transforms, evaluate=True)
+        diff = sp.simplify(ep - eg)
+        if diff == 0:
+            return True
+        # fall back to numeric equality of the two expressions
+        try:
+            return bool(abs(float(ep) - float(eg)) <= 1e-6)
+        except (TypeError, ValueError):
+            return False
+    except Exception:
+        return False
+
+
+# ----------------------------------------------------------------------------
+# Problem-text normalization for contamination dedup
+# ----------------------------------------------------------------------------
+
+def normalize_problem_text(s: str) -> str:
+    """Aggressive normalization so the same problem from different sources
+    (PRM800K vs ProcessBench vs MATH-500) collides for dedup."""
+    if s is None:
+        return ""
+    s = s.lower()
+    s = _strip_text_wrappers(s)
+    s = re.sub(r"[^a-z0-9]+", "", s)   # keep only alnum; drop all latex/space/punct
+    return s

src/mathcompose/common/parallel.py

@@ -0,0 +1,44 @@
+"""Ordered, fault-tolerant thread-pool map for I/O-bound teacher calls.
+
+API calls are I/O-bound, so threads give near-linear speedup. Results preserve
+input order; any item whose fn raises becomes None (so callers filter(None)).
+"""
+from __future__ import annotations
+
+from concurrent.futures import ThreadPoolExecutor, as_completed
+from typing import Callable, Iterable, Optional
+
+
+def thread_map(
+    fn: Callable,
+    items: Iterable,
+    workers: int = 8,
+    desc: Optional[str] = None,
+) -> list:
+    items = list(items)
+    results: list = [None] * len(items)
+
+    try:
+        from tqdm.auto import tqdm
+    except Exception:  # pragma: no cover
+        def tqdm(x, **k):
+            return x
+
+    if workers <= 1:
+        seq = enumerate(items)
+        for i, x in tqdm(seq, total=len(items), desc=desc):
+            try:
+                results[i] = fn(x)
+            except Exception:
+                results[i] = None
+        return results
+
+    with ThreadPoolExecutor(max_workers=workers) as ex:
+        futs = {ex.submit(fn, x): i for i, x in enumerate(items)}
+        for fut in tqdm(as_completed(futs), total=len(items), desc=desc):
+            i = futs[fut]
+            try:
+                results[i] = fut.result()
+            except Exception:
+                results[i] = None
+    return results

src/mathcompose/common/seeding.py

@@ -0,0 +1,24 @@
+"""Deterministic seeding across random / numpy / torch (torch optional)."""
+from __future__ import annotations
+
+import os
+import random
+
+
+def set_seed(seed: int = 0) -> None:
+    os.environ["PYTHONHASHSEED"] = str(seed)
+    random.seed(seed)
+    try:
+        import numpy as np
+
+        np.random.seed(seed)
+    except Exception:
+        pass
+    try:
+        import torch
+
+        torch.manual_seed(seed)
+        if torch.cuda.is_available():
+            torch.cuda.manual_seed_all(seed)
+    except Exception:
+        pass

src/mathcompose/data/__init__.py

@@ -0,0 +1,13 @@
+from .schema import (
+    StepVerdict,
+    VerifierOutput,
+    serialize_verifier_output,
+    parse_verifier_output,
+)
+
+__all__ = [
+    "StepVerdict",
+    "VerifierOutput",
+    "serialize_verifier_output",
+    "parse_verifier_output",
+]

src/mathcompose/data/build_generator_dataset.py

@@ -0,0 +1,117 @@
+r"""Build Model G's SFT dataset by distilling CoT solutions from the teacher and
+keeping only answer-correct traces.
+
+    python -m mathcompose.data.build_generator_dataset \
+        --source AI-MO/NuminaMath-CoT --split train \
+        --teacher anthropic --limit 8000 --out-dir data/generator
+
+Problem/answer are read from the HF dataset; if no explicit answer field exists,
+the gold answer is taken from the LAST \boxed{} in the dataset's own solution.
+"""
+from __future__ import annotations
+
+import argparse
+import json
+import random
+from pathlib import Path
+
+from ..common.io import write_jsonl
+from ..common.math_grade import extract_last_boxed, grade_answer
+from ..common.parallel import thread_map
+from ..teachers import get_teacher
+from ..datagen.dedup import build_contamination_set, is_contaminated
+from ..datagen.gen_generator_data import Problem, synthesize_solution, make_generator_row
+
+
+def _load_problems(source: str, split: str, problem_field: str, answer_field: str | None,
+                   solution_field: str, limit: int | None) -> list[Problem]:
+    from datasets import load_dataset
+
+    ds = load_dataset(source, split=split)
+    if limit:
+        ds = ds.select(range(min(limit, len(ds))))
+    problems: list[Problem] = []
+    for row in ds:
+        prob = row.get(problem_field)
+        if not prob:
+            continue
+        if answer_field and row.get(answer_field) not in (None, ""):
+            ans = str(row[answer_field])
+        else:
+            sol = row.get(solution_field) or ""
+            ans = extract_last_boxed(sol)
+        if not ans:
+            continue
+        problems.append(Problem(problem=prob, answer=ans))
+    return problems
+
+
+def main() -> None:
+    ap = argparse.ArgumentParser(description=__doc__)
+    ap.add_argument("--source", default="AI-MO/NuminaMath-CoT")
+    ap.add_argument("--split", default="train")
+    ap.add_argument("--problem-field", default="problem")
+    ap.add_argument("--answer-field", default=None, help="explicit answer column, if any")
+    ap.add_argument("--solution-field", default="solution", help="fallback: parse \\boxed{} from here")
+    ap.add_argument("--out-dir", default="data/generator")
+    ap.add_argument("--teacher", default="promptlens",
+                    choices=["promptlens", "tfy", "anthropic", "openai", "dummy"])
+    ap.add_argument("--model", default=None)
+    ap.add_argument("--limit", type=int, default=None)
+    ap.add_argument("--val-frac", type=float, default=0.05)
+    ap.add_argument("--temperature", type=float, default=0.7)
+    ap.add_argument("--max-attempts", type=int, default=2)
+    ap.add_argument("--workers", type=int, default=8, help="concurrent teacher calls")
+    ap.add_argument("--keep-all", action="store_true", help="skip the answer-correct filter")
+    ap.add_argument("--no-dedup", action="store_true")
+    ap.add_argument("--seed", type=int, default=0)
+    args = ap.parse_args()
+
+    random.seed(args.seed)
+    teacher = get_teacher(args.teacher, **({"model": args.model} if args.model else {}))
+
+    banned = set()
+    if not args.no_dedup:
+        print("Building contamination set from ProcessBench + MATH-500 ...")
+        banned = build_contamination_set()
+        print(f"  {len(banned)} eval problems banned")
+
+    problems = [
+        p for p in _load_problems(args.source, args.split, args.problem_field,
+                                  args.answer_field, args.solution_field, args.limit)
+        if not (banned and is_contaminated(p.problem, banned))
+    ]
+    print(f"Loaded {len(problems)} problems; distilling "
+          f"({args.workers} workers, teacher={args.teacher}) ...")
+
+    def _one(p):
+        for _ in range(args.max_attempts):
+            sol = synthesize_solution(teacher, p.problem, temperature=args.temperature)
+            if args.keep_all or grade_answer(extract_last_boxed(sol), p.answer):
+                return make_generator_row(p.problem, sol)
+        return None
+
+    rows = [r for r in thread_map(_one, problems, workers=args.workers, desc="generator") if r]
+    random.shuffle(rows)
+
+    n_val = max(1, int(len(rows) * args.val_frac)) if rows else 0
+    val, train = rows[:n_val], rows[n_val:]
+
+    out = Path(args.out_dir)
+    n_train = write_jsonl(train, out / "train.jsonl")
+    n_val = write_jsonl(val, out / "val.jsonl")
+    stats = {
+        "n_problems": len(problems),
+        "n_kept": len(rows),
+        "n_train": n_train,
+        "n_val": n_val,
+        "keep_rate": (len(rows) / len(problems)) if problems else 0.0,
+        "teacher": args.teacher,
+        "filtered_by_answer": not args.keep_all,
+    }
+    (out / "stats.json").write_text(json.dumps(stats, indent=2))
+    print(json.dumps(stats, indent=2))
+
+
+if __name__ == "__main__":
+    main()

src/mathcompose/data/build_verifier_dataset.py

@@ -0,0 +1,85 @@
+r"""Build Model V's SFT dataset from PRM800K.
+
+    python -m mathcompose.data.build_verifier_dataset \
+        --prm800k data/raw/prm800k/phase2_train.jsonl \
+        --teacher anthropic --limit 15000 --out-dir data/verifier
+
+Writes data/verifier/{train,val}.jsonl (+ stats.json). Contamination against
+ProcessBench/MATH-500 is enforced unless --no-dedup.
+"""
+from __future__ import annotations
+
+import argparse
+import json
+import random
+from pathlib import Path
+
+from ..common.io import write_jsonl
+from ..common.parallel import thread_map
+from ..teachers import get_teacher
+from ..datagen.prm800k_loader import iter_prm800k
+from ..datagen.dedup import build_contamination_set, is_contaminated
+from ..datagen.gen_verifier_data import synthesize_verifier_completion, make_verifier_row
+
+
+def main() -> None:
+    ap = argparse.ArgumentParser(description=__doc__)
+    ap.add_argument("--prm800k", required=True, help="path to PRM800K .jsonl")
+    ap.add_argument("--out-dir", default="data/verifier")
+    ap.add_argument("--teacher", default="promptlens",
+                    choices=["promptlens", "tfy", "anthropic", "openai", "dummy"])
+    ap.add_argument("--model", default=None, help="teacher model id override")
+    ap.add_argument("--limit", type=int, default=None)
+    ap.add_argument("--val-frac", type=float, default=0.05)
+    ap.add_argument("--temperature", type=float, default=0.4)
+    ap.add_argument("--workers", type=int, default=8, help="concurrent teacher calls")
+    ap.add_argument("--no-dedup", action="store_true")
+    ap.add_argument("--seed", type=int, default=0)
+    args = ap.parse_args()
+
+    random.seed(args.seed)
+    teacher = get_teacher(args.teacher, **({"model": args.model} if args.model else {}))
+
+    banned = set()
+    if not args.no_dedup:
+        print("Building contamination set from ProcessBench + MATH-500 ...")
+        banned = build_contamination_set()
+        print(f"  {len(banned)} eval problems banned")
+
+    records = [
+        r for r in iter_prm800k(args.prm800k, limit=args.limit)
+        if not (banned and is_contaminated(r.problem, banned))
+    ]
+    print(f"synthesizing critiques for {len(records)} records "
+          f"({args.workers} workers, teacher={args.teacher}) ...")
+
+    def _one(rec):
+        completion = synthesize_verifier_completion(teacher, rec, temperature=args.temperature)
+        return make_verifier_row(rec, completion)
+
+    rows = [r for r in thread_map(_one, records, workers=args.workers, desc="verifier") if r]
+    random.shuffle(rows)
+
+    n_val = max(1, int(len(rows) * args.val_frac)) if rows else 0
+    val, train = rows[:n_val], rows[n_val:]
+
+    out = Path(args.out_dir)
+    n_train = write_jsonl(train, out / "train.jsonl")
+    n_val = write_jsonl(val, out / "val.jsonl")
+
+    err = sum(1 for r in rows if r.get("first_error_index", -1) != -1)
+    stats = {
+        "n_total": len(rows),
+        "n_train": n_train,
+        "n_val": n_val,
+        "n_erroneous": err,
+        "n_all_correct": len(rows) - err,
+        "teacher": args.teacher,
+        "deduped": not args.no_dedup,
+    }
+    (out / "stats.json").write_text(json.dumps(stats, indent=2))
+    print(json.dumps(stats, indent=2))
+
+
+if __name__ == "__main__":
+    main()

src/mathcompose/data/schema.py

@@ -0,0 +1,93 @@
+r"""Model V's canonical output schema — the single primitive that lets one model
+both score ProcessBench and rerank Model G.
+
+Serialized completion (what V is trained to produce and what we parse back):
+
+    Paragraph 0: <one-line critique>. Verdict: correct
+    Paragraph 1: <one-line critique>. Verdict: incorrect
+
+    The earliest error is in paragraph 1.
+
+    \boxed{1}
+
+The trailing ``\boxed{k}`` is authoritative: ``k`` = 0-based index of the first
+incorrect paragraph, ``-1`` = all correct. Per-paragraph ``Verdict:`` lines are
+a secondary, best-effort signal (useful for analysis and soft rerank scores).
+"""
+from __future__ import annotations
+
+import re
+from dataclasses import dataclass, field
+from typing import Optional
+
+
+@dataclass
+class StepVerdict:
+    index: int
+    verdict: str  # "correct" | "incorrect"
+    critique: str = ""
+
+
+@dataclass
+class VerifierOutput:
+    first_error_index: int          # -1 == all correct
+    steps: list[StepVerdict] = field(default_factory=list)
+    raw: str = ""
+
+    @property
+    def all_correct(self) -> bool:
+        return self.first_error_index == -1
+
+
+def serialize_verifier_output(
+    step_verdicts: list[StepVerdict], first_error_index: int
+) -> str:
+    """Render a training-target completion from structured verdicts."""
+    lines = []
+    for sv in step_verdicts:
+        crit = sv.critique.strip()
+        prefix = f"Paragraph {sv.index}: "
+        body = (crit + " " if crit else "")
+        lines.append(f"{prefix}{body}Verdict: {sv.verdict}")
+    body = "\n".join(lines)
+    if first_error_index == -1:
+        tail = "\n\nAll paragraphs are correct."
+    else:
+        tail = f"\n\nThe earliest error is in paragraph {first_error_index}."
+    return f"{body}{tail}\n\n\\boxed{{{first_error_index}}}"
+
+
+_VERDICT_RE = re.compile(
+    r"[Pp]aragraph\s*(\d+)\s*:?.*?[Vv]erdict\s*:?\s*(correct|incorrect)",
+    re.DOTALL,
+)
+
+
+def parse_verifier_output(text: str) -> VerifierOutput:
+    """Parse raw model text back into a VerifierOutput.
+
+    The boxed integer is authoritative for ``first_error_index``. If no box is
+    present we fall back to the earliest paragraph explicitly marked incorrect.
+    """
+    from ..common.math_grade import extract_boxed_int
+
+    step_verdicts: list[StepVerdict] = []
+    for m in _VERDICT_RE.finditer(text):
+        step_verdicts.append(StepVerdict(index=int(m.group(1)), verdict=m.group(2)))
+
+    idx = extract_boxed_int(text)
+    if idx is None:
+        # fall back: earliest "incorrect" paragraph, else -1 if any verdicts seen
+        incorrect = [sv.index for sv in step_verdicts if sv.verdict == "incorrect"]
+        if incorrect:
+            idx = min(incorrect)
+        elif step_verdicts:
+            idx = -1
+        else:
+            idx = None  # genuinely unparseable
+
+    return VerifierOutput(
+        first_error_index=idx if idx is not None else -2,  # -2 == parse failure sentinel
+        steps=step_verdicts,
+        raw=text,
+    )

src/mathcompose/datagen/__init__.py

@@ -0,0 +1,11 @@
+"""Data-generation pipeline for Model V (verifier) and Model G (generator)."""
+from .prm800k_loader import PRM800KRecord, parse_prm800k_row, iter_prm800k
+from .dedup import build_contamination_set, is_contaminated
+
+__all__ = [
+    "PRM800KRecord",
+    "parse_prm800k_row",
+    "iter_prm800k",
+    "build_contamination_set",
+    "is_contaminated",
+]

src/mathcompose/datagen/dedup.py

@@ -0,0 +1,48 @@
+r"""Contamination guard.
+
+PRM800K is built on MATH; ProcessBench's ``math``/``olympiadbench`` subsets and
+MATH-500 also derive from MATH. Training V on a problem that appears in the eval
+would inflate the score. We drop any training problem whose normalized text
+collides with an eval problem.
+"""
+from __future__ import annotations
+
+from typing import Iterable, Optional
+
+from ..common.math_grade import normalize_problem_text
+
+
+def build_contamination_set(
+    processbench_splits: Iterable[str] = ("math", "olympiadbench", "omnimath", "gsm8k"),
+    include_math500: bool = True,
+    extra_problems: Optional[Iterable[str]] = None,
+    processbench_id: str = "Qwen/ProcessBench",
+    math500_id: str = "HuggingFaceH4/MATH-500",
+) -> set[str]:
+    """Normalized problem texts appearing in the eval sets. Requires network
+    (HF Hub) unless you pass only ``extra_problems``."""
+    banned: set[str] = set()
+    from datasets import load_dataset
+
+    for split in processbench_splits:
+        try:
+            ds = load_dataset(processbench_id, split=split)
+            for p in ds["problem"]:
+                banned.add(normalize_problem_text(p))
+        except Exception:
+            continue
+    if include_math500:
+        try:
+            ds = load_dataset(math500_id, split="test")
+            for p in ds["problem"]:
+                banned.add(normalize_problem_text(p))
+        except Exception:
+            pass
+    if extra_problems:
+        for p in extra_problems:
+            banned.add(normalize_problem_text(p))
+    return banned
+
+
+def is_contaminated(problem: str, banned: set[str]) -> bool:
+    return normalize_problem_text(problem) in banned

src/mathcompose/datagen/gen_generator_data.py

@@ -0,0 +1,70 @@
+r"""Synthesize Model G training rows: distill CoT solutions from the teacher and
+keep only those whose ``\boxed{}`` answer is correct (rejection sampling on a
+free objective signal).
+"""
+from __future__ import annotations
+
+from dataclasses import dataclass
+from typing import Iterable, Iterator, Optional
+
+from ..common.chat import generator_messages, GENERATOR_SYSTEM
+from ..common.math_grade import extract_last_boxed, grade_answer
+from .dedup import is_contaminated
+
+
+@dataclass
+class Problem:
+    problem: str
+    answer: str
+
+
+def synthesize_solution(teacher, problem: str, *, temperature: float = 0.7, max_tokens: int = 2048) -> str:
+    return teacher.complete(generator_messages(problem), temperature=temperature, max_tokens=max_tokens)
+
+
+def make_generator_row(problem: str, solution: str) -> dict:
+    return {
+        "prompt": [
+            {"role": "system", "content": GENERATOR_SYSTEM},
+            {"role": "user", "content": problem.strip()},
+        ],
+        "completion": [{"role": "assistant", "content": solution.strip()}],
+    }
+
+
+def generate_generator_dataset(
+    problems: Iterable[Problem],
+    teacher,
+    banned: Optional[set[str]] = None,
+    *,
+    temperature: float = 0.7,
+    keep_only_correct: bool = True,
+    max_attempts: int = 1,
+    skip_on_error: bool = True,
+) -> Iterator[dict]:
+    """Yield filtered G training rows.
+
+    For each problem, sample up to ``max_attempts`` solutions and keep the first
+    whose boxed answer matches the gold (when ``keep_only_correct``). This is the
+    rejection-sampling filter that makes the dataset the deliverable.
+    """
+    for p in problems:
+        if banned and is_contaminated(p.problem, banned):
+            continue
+        kept = None
+        for _ in range(max_attempts):
+            try:
+                sol = synthesize_solution(teacher, p.problem, temperature=temperature)
+            except Exception:
+                if skip_on_error:
+                    break
+                raise
+            if not keep_only_correct:
+                kept = sol
+                break
+            pred = extract_last_boxed(sol)
+            if pred is not None and grade_answer(pred, p.answer):
+                kept = sol
+                break
+        if kept is not None:
+            yield make_generator_row(p.problem, kept)

src/mathcompose/datagen/gen_verifier_data.py

@@ -0,0 +1,96 @@
+r"""Synthesize Model V training rows from PRM800K records.
+
+Key idea (GenPRM-style rationale synthesis): the *label* (first-error index) is
+ground truth from PRM800K. The teacher only writes the paragraph-by-paragraph
+*critique prose*, conditioned on that known index ("rationalization with hint").
+We then STAMP the authoritative ``\boxed{gold}`` onto the completion, so a
+teacher that boxes the wrong index can never corrupt a label.
+
+Two distinct prompts:
+  * synthesis prompt (to the teacher) — INCLUDES the gold index.
+  * stored training prompt (what V sees) — the plain ProcessBench critic prompt,
+    with NO gold leak; V must learn to find the error itself.
+"""
+from __future__ import annotations
+
+import re
+from typing import Iterable, Iterator, Optional
+
+from ..common.chat import build_verifier_prompt, verifier_messages, VERIFIER_SYSTEM
+from .prm800k_loader import PRM800KRecord
+from .dedup import is_contaminated
+
+_SYNTH_INSTRUCTION = (
+    "You are writing a high-quality critique for a grader-training dataset.\n\n"
+    "{prompt}\n\n"
+    "GROUND TRUTH (for your eyes only — never reveal that you were told): "
+    "{gold_desc}\n\n"
+    "Write a concise paragraph-by-paragraph critique. For each paragraph i, output "
+    "exactly one line:\n"
+    "  Paragraph i: <one-sentence analysis>. Verdict: correct\n"
+    "or\n"
+    "  Paragraph i: <one-sentence analysis>. Verdict: incorrect\n"
+    "Paragraphs before the first error are correct; the first error is the paragraph "
+    "named above; do not analyze paragraphs after the first error. Finish with a short "
+    "sentence naming the earliest error paragraph (or stating all paragraphs are correct). "
+    "Do NOT write a \\boxed{{}} — it is appended automatically."
+)
+
+
+def _gold_desc(idx: int) -> str:
+    if idx == -1:
+        return "the solution is fully correct (no erroneous paragraph)."
+    return f"the FIRST error occurs in paragraph {idx}."
+
+
+def _strip_trailing_box(text: str) -> str:
+    return re.sub(r"\\boxed\{[^{}]*\}\s*$", "", text.strip()).strip()
+
+
+def synthesize_verifier_completion(
+    teacher, rec: PRM800KRecord, *, temperature: float = 0.4, max_tokens: int = 1536
+) -> str:
+    """Teacher critique + authoritative boxed label."""
+    synth_prompt = _SYNTH_INSTRUCTION.format(
+        prompt=build_verifier_prompt(rec.problem, rec.steps),
+        gold_desc=_gold_desc(rec.first_error_index),
+    )
+    messages = [
+        {"role": "system", "content": VERIFIER_SYSTEM},
+        {"role": "user", "content": synth_prompt},
+    ]
+    critique = teacher.complete(messages, temperature=temperature, max_tokens=max_tokens)
+    critique = _strip_trailing_box(critique)
+    return f"{critique}\n\n\\boxed{{{rec.first_error_index}}}"
+
+
+def make_verifier_row(rec: PRM800KRecord, completion: str) -> dict:
+    """Conversational prompt-completion row (triggers TRL completion_only_loss)."""
+    prompt_msgs = verifier_messages(rec.problem, rec.steps)  # system + user, no gold
+    return {
+        "prompt": prompt_msgs,
+        "completion": [{"role": "assistant", "content": completion}],
+        "first_error_index": rec.first_error_index,  # kept for inspection/stats
+    }
+
+
+def generate_verifier_dataset(
+    records: Iterable[PRM800KRecord],
+    teacher,
+    banned: Optional[set[str]] = None,
+    *,
+    temperature: float = 0.4,
+    skip_on_error: bool = True,
+) -> Iterator[dict]:
+    """Yield training rows; drops contaminated problems and (optionally) teacher
+    failures."""
+    for rec in records:
+        if banned and is_contaminated(rec.problem, banned):
+            continue
+        try:
+            completion = synthesize_verifier_completion(teacher, rec, temperature=temperature)
+        except Exception:
+            if skip_on_error:
+                continue
+            raise
+        yield make_verifier_row(rec, completion)

src/mathcompose/datagen/prm800k_loader.py

@@ -0,0 +1,113 @@
+r"""Parse PRM800K (OpenAI "Let's Verify Step by Step", MIT license) into
+first-error-localization records.
+
+PRM800K rows (newline-delimited JSON) look like::
+
+    {
+      "question": {"problem": "...", "ground_truth_answer": "..."},
+      "label": {
+        "steps": [
+          {"completions": [{"text": "...", "rating": 1}], "chosen_completion": 0,
+           "human_completion": null},
+          ...
+        ],
+        "finish_reason": "solution" | "found_error" | "give_up"
+      }
+    }
+
+We reconstruct the solution as the sequence of *chosen* step texts and set
+``first_error_index`` = index of the first step whose chosen completion is rated
+``-1`` (or ``-1`` if the whole solution is correct). PRM800K phase-2 stops
+labeling after the first mistake, so the erroneous step is the last one we keep.
+
+The parser accepts either a path to a ``.jsonl`` file or an iterable of dict
+rows (handy for tests / fixtures).
+"""
+from __future__ import annotations
+
+import json
+from dataclasses import dataclass
+from pathlib import Path
+from typing import Iterable, Iterator, Optional, Union
+
+
+@dataclass
+class PRM800KRecord:
+    problem: str
+    steps: list[str]
+    first_error_index: int          # -1 == all correct
+    ground_truth_answer: Optional[str] = None
+
+
+def _chosen_text_and_rating(step: dict) -> tuple[Optional[str], Optional[int]]:
+    """Return (text, rating) for the human-selected completion of a step."""
+    human = step.get("human_completion")
+    completions = step.get("completions") or []
+    ci = step.get("chosen_completion")
+
+    if ci is not None and 0 <= ci < len(completions):
+        c = completions[ci]
+        return c.get("text"), c.get("rating")
+    if human:  # human wrote a correct step
+        text = human if isinstance(human, str) else human.get("text")
+        return text, 1
+    if completions:  # fall back to first completion
+        c = completions[0]
+        return c.get("text"), c.get("rating")
+    return None, None
+
+
+def parse_prm800k_row(row: dict) -> Optional[PRM800KRecord]:
+    """Convert one PRM800K row into a record, or None if it can't be used."""
+    q = row.get("question") or {}
+    problem = q.get("problem")
+    label = row.get("label") or {}
+    raw_steps = label.get("steps") or []
+    if not problem or not raw_steps:
+        return None
+
+    steps: list[str] = []
+    first_error = -1
+    for i, step in enumerate(raw_steps):
+        text, rating = _chosen_text_and_rating(step)
+        if text is None:
+            break
+        steps.append(text.strip())
+        if rating is not None and rating < 0:
+            first_error = i
+            break  # phase-2: labeling stops at the first mistake
+
+    if not steps:
+        return None
+    return PRM800KRecord(
+        problem=problem.strip(),
+        steps=steps,
+        first_error_index=first_error,
+        ground_truth_answer=q.get("ground_truth_answer"),
+    )
+
+
+def iter_prm800k(
+    source: Union[str, Path, Iterable[dict]],
+    limit: Optional[int] = None,
+) -> Iterator[PRM800KRecord]:
+    """Yield PRM800KRecords from a .jsonl path or an iterable of dict rows."""
+    def _rows() -> Iterator[dict]:
+        if isinstance(source, (str, Path)):
+            with open(source) as f:
+                for line in f:
+                    line = line.strip()
+                    if line:
+                        yield json.loads(line)
+        else:
+            yield from source
+
+    n = 0
+    for row in _rows():
+        rec = parse_prm800k_row(row)
+        if rec is None:
+            continue
+        yield rec
+        n += 1
+        if limit is not None and n >= limit:
+            return

src/mathcompose/eval/__init__.py

@@ -0,0 +1,11 @@
+from .parse import (
+    first_error_index,
+    majority_index,
+    p_correct_from_samples,
+)
+
+__all__ = [
+    "first_error_index",
+    "majority_index",
+    "p_correct_from_samples",
+]

src/mathcompose/eval/compose.py

@@ -0,0 +1,101 @@
+r"""Composition eval: does Model V recover Model G's headroom?
+
+For each problem we sample n solutions from G and compare selection strategies:
+  pass@1        greedy/first sample                         (floor)
+  maj@n         plain majority vote over final answers       (baseline)
+  oracle pass@n any sample correct                           (ceiling)
+  weighted_maj  majority weighted by V's p_correct           (V result)
+  best_of_n     single highest-V-scored sample               (V result)
+
+generator-verifier gap = oracle - maj@n ; V's value = how much of that gap the
+weighted vote recovers. This reproduces the Weaver headroom result at <=4B.
+
+Pure w.r.t. two callbacks (solve_fn, v_score_fn) so it is unit-testable with
+fakes; the real callbacks come from eval/runners.py.
+"""
+from __future__ import annotations
+
+from collections import defaultdict
+from typing import Callable, Optional, Sequence
+
+from ..common.chat import split_into_steps
+from ..common.math_grade import extract_last_boxed, grade_answer, normalize_final_answer
+from .parse import p_correct_from_samples
+
+SolveFn = Callable[[str], list[str]]          # problem -> n solution strings
+VScoreFn = Callable[[str, list[str]], float]  # (problem, solution_steps) -> p_correct in [0,1]
+
+_NONE_KEY = "__no_answer__"
+
+
+def _weighted_vote(answers: Sequence[Optional[str]], weights: Sequence[float],
+                   correct: Sequence[bool]) -> bool:
+    """Return whether the max-weight answer bucket is correct."""
+    buckets: dict[str, dict] = defaultdict(lambda: {"w": 0.0, "correct": False})
+    for ans, w, ok in zip(answers, weights, correct):
+        key = normalize_final_answer(ans) if ans else _NONE_KEY
+        b = buckets[key]
+        b["w"] += w
+        b["correct"] = b["correct"] or ok
+    if not buckets:
+        return False
+    winner = max(buckets.values(), key=lambda b: b["w"])
+    return bool(winner["correct"])
+
+
+def evaluate_composition(
+    problems: Sequence[tuple[str, str]],   # (problem, gold_answer)
+    solve_fn: SolveFn,
+    v_score_fn: VScoreFn,
+    progress: bool = True,
+) -> dict:
+    try:
+        from tqdm.auto import tqdm
+    except Exception:  # pragma: no cover
+        def tqdm(x, **k):
+            return x
+
+    acc = {k: 0 for k in ["pass@1", "maj@n", "oracle", "weighted_maj", "best_of_n"]}
+    n_total = 0
+
+    it = tqdm(problems, desc="compose") if progress else problems
+    for problem, gold in it:
+        samples = solve_fn(problem)
+        if not samples:
+            n_total += 1
+            continue
+        answers = [extract_last_boxed(s) for s in samples]
+        correct = [grade_answer(a, gold) for a in answers]
+        v_scores = [v_score_fn(problem, split_into_steps(s)) for s in samples]
+
+        n_total += 1
+        acc["pass@1"] += 1 if correct[0] else 0
+        acc["oracle"] += 1 if any(correct) else 0
+        acc["maj@n"] += 1 if _weighted_vote(answers, [1.0] * len(samples), correct) else 0
+        acc["weighted_maj"] += 1 if _weighted_vote(answers, v_scores, correct) else 0
+        # best-of-n: single highest-V sample
+        best_i = max(range(len(samples)), key=lambda i: v_scores[i])
+        acc["best_of_n"] += 1 if correct[best_i] else 0
+
+    out = {k: (v / n_total if n_total else 0.0) for k, v in acc.items()}
+    out["n"] = n_total
+    gap = out["oracle"] - out["maj@n"]
+    out["generator_verifier_gap"] = gap
+    out["gap_recovered_by_V"] = (
+        (out["weighted_maj"] - out["maj@n"]) / gap if gap > 1e-9 else None
+    )
+    return out
+
+
+def make_v_scorer(runner, k: int = 4, temperature: float = 0.6,
+                  max_new_tokens: int = 1024) -> VScoreFn:
+    """Build a V-score callback from an HFRunner: sample k critiques per solution
+    and return the fraction that judged it fully correct."""
+    from ..common.chat import verifier_messages
+
+    def v_score_fn(problem: str, solution_steps: list[str]) -> float:
+        samples = runner.chat(verifier_messages(problem, solution_steps), n=k,
+                              temperature=temperature, max_new_tokens=max_new_tokens)
+        return p_correct_from_samples(samples)
+
+    return v_score_fn

src/mathcompose/eval/math500.py

@@ -0,0 +1,62 @@
+r"""Model G answer-accuracy eval (objective: boxed answer vs gold, no judge).
+
+Works for MATH-500 (fields problem/answer) and AIME_2024 (fields Problem/Answer)
+via configurable field names. Reports pass@1 (first sample) and pass@k
+(any-of-k correct).
+"""
+from __future__ import annotations
+
+from typing import Callable, Optional, Sequence
+
+from ..common.math_grade import extract_last_boxed, grade_answer
+
+# solve_fn(problem) -> list of k solution strings
+SolveFn = Callable[[str], list[str]]
+
+
+def _any_correct(samples: Sequence[str], gold: str) -> list[bool]:
+    return [grade_answer(extract_last_boxed(s), gold) for s in samples]
+
+
+def evaluate_generator(
+    solve_fn: SolveFn,
+    dataset_id: str = "HuggingFaceH4/MATH-500",
+    split: str = "test",
+    problem_field: str = "problem",
+    answer_field: str = "answer",
+    limit: Optional[int] = None,
+    progress: bool = True,
+) -> dict:
+    from datasets import load_dataset
+
+    try:
+        from tqdm.auto import tqdm
+    except Exception:  # pragma: no cover
+        def tqdm(x, **k):
+            return x
+
+    ds = load_dataset(dataset_id, split=split)
+    if limit is not None:
+        ds = ds.select(range(min(limit, len(ds))))
+
+    n_total = 0
+    n_pass1 = 0
+    n_passk = 0
+    it = tqdm(ds, desc=f"MATH/{dataset_id.split('/')[-1]}") if progress else ds
+    for row in it:
+        gold = str(row[answer_field])
+        samples = solve_fn(row[problem_field])
+        if not samples:
+            n_total += 1
+            continue
+        flags = _any_correct(samples, gold)
+        n_total += 1
+        n_pass1 += 1 if flags[0] else 0
+        n_passk += 1 if any(flags) else 0
+
+    return {
+        "dataset": dataset_id,
+        "n": n_total,
+        "pass@1": n_pass1 / n_total if n_total else 0.0,
+        "pass@k": n_passk / n_total if n_total else 0.0,
+    }

src/mathcompose/eval/parse.py

@@ -0,0 +1,46 @@
+"""Eval-facing helpers over Model V's output — used by ProcessBench scoring
+(single output or Maj@k) and by the composition reranker.
+
+A parse failure maps to the sentinel ``-2`` so it never accidentally equals a
+gold label (which is >= -1); i.e. an unparseable V output is scored as wrong.
+"""
+from __future__ import annotations
+
+from collections import Counter
+
+from ..data.schema import parse_verifier_output
+
+PARSE_FAIL = -2
+
+
+def first_error_index(text: str) -> int:
+    """0-based first-error index (or -1 all-correct; PARSE_FAIL if unparseable)."""
+    return parse_verifier_output(text).first_error_index
+
+
+def majority_index(samples: list[str]) -> int:
+    """Maj@k over the first-error index across k sampled V outputs.
+
+    Parse failures are dropped before voting; if every sample failed, returns
+    PARSE_FAIL. Ties broken by the smallest (earliest) index — the conservative
+    choice for *first*-error localization.
+    """
+    idxs = [first_error_index(s) for s in samples]
+    idxs = [i for i in idxs if i != PARSE_FAIL]
+    if not idxs:
+        return PARSE_FAIL
+    counts = Counter(idxs)
+    top = max(counts.values())
+    winners = [i for i, c in counts.items() if c == top]
+    return min(winners)
+
+
+def p_correct_from_samples(samples: list[str]) -> float:
+    """Solution-level correctness probability for reranking Model G:
+    fraction of k verifier samples that judged the whole solution correct
+    (first_error_index == -1). Parse failures count as 'not correct'.
+    """
+    if not samples:
+        return 0.0
+    good = sum(1 for s in samples if first_error_index(s) == -1)
+    return good / len(samples)

src/mathcompose/eval/prmbench.py

@@ -0,0 +1,85 @@
+r"""PRMBench robustness eval (hitsmy/PRMBench_Preview, apache-2.0).
+
+Each row pairs a correct ``original_process`` with a ``modified_process`` that has
+injected errors at ``error_steps`` (1-based), tagged with a ``classification``
+category (confidence, redundancy, ...). This stresses whether V gets fooled into
+accepting subtly-wrong reasoning.
+
+We report a simplified but faithful robustness picture (the official ``mr_eval``
+toolkit computes finer per-category scores):
+  detection   — fraction of MODIFIED processes where V flags any error (index != -1)
+  localization— fraction where V's flagged index hits a gold error step
+  false_pos   — fraction of ORIGINAL (correct) processes V wrongly flags (index != -1)
+  per_category detection breakdown.
+
+Uses the same ``verify_fn`` as ProcessBench, so V is evaluated identically.
+"""
+from __future__ import annotations
+
+from collections import defaultdict
+from typing import Callable, Optional
+
+from .parse import majority_index
+
+VerifyFn = Callable[[str, list[str]], list[str]]
+
+
+def evaluate_prmbench(
+    verify_fn: VerifyFn,
+    dataset_id: str = "hitsmy/PRMBench_Preview",
+    split: str = "train",
+    limit: Optional[int] = None,
+    error_steps_base: int = 1,          # PRMBench error_steps are 1-based
+    include_original: bool = True,      # also run the false-positive pass
+    progress: bool = True,
+) -> dict:
+    from datasets import load_dataset
+
+    try:
+        from tqdm.auto import tqdm
+    except Exception:  # pragma: no cover
+        def tqdm(x, **k):
+            return x
+
+    ds = load_dataset(dataset_id, split=split)
+    if limit is not None:
+        ds = ds.select(range(min(limit, len(ds))))
+
+    n_mod = detected = localized = 0
+    n_orig = false_pos = 0
+    per_cat: dict[str, dict] = defaultdict(lambda: {"n": 0, "detected": 0})
+
+    it = tqdm(ds, desc="PRMBench") if progress else ds
+    for row in it:
+        q_mod = row.get("modified_question") or row.get("question") or ""
+        steps_mod = list(row.get("modified_process") or [])
+        gold0 = {int(e) - error_steps_base for e in (row.get("error_steps") or [])}
+        cat = row.get("classification") or "unknown"
+        if steps_mod and gold0:
+            pred = majority_index(verify_fn(q_mod, steps_mod))
+            n_mod += 1
+            is_detected = pred != -1
+            detected += 1 if is_detected else 0
+            localized += 1 if pred in gold0 else 0
+            per_cat[cat]["n"] += 1
+            per_cat[cat]["detected"] += 1 if is_detected else 0
+
+        if include_original:
+            q_orig = row.get("original_question") or row.get("question") or ""
+            steps_orig = list(row.get("original_process") or [])
+            if steps_orig:
+                pred_o = majority_index(verify_fn(q_orig, steps_orig))
+                n_orig += 1
+                false_pos += 1 if pred_o != -1 else 0
+
+    return {
+        "dataset": dataset_id,
+        "n_modified": n_mod,
+        "detection": detected / n_mod if n_mod else 0.0,
+        "localization": localized / n_mod if n_mod else 0.0,
+        "false_positive_rate": (false_pos / n_orig) if n_orig else None,
+        "per_category_detection": {
+            c: {"n": d["n"], "detection": d["detected"] / d["n"] if d["n"] else 0.0}
+            for c, d in sorted(per_cat.items())
+        },
+    }

src/mathcompose/eval/processbench.py

@@ -0,0 +1,116 @@
+r"""ProcessBench evaluation — the core objective metric for Model V.
+
+Dataset: ``Qwen/ProcessBench`` (apache-2.0), 4 splits (gsm8k 400, math 1000,
+olympiadbench 1000, omnimath 1000). Each row: ``problem`` (str),
+``steps`` (list[str]), ``label`` (int; 0-based index of first erroneous step,
+``-1`` == all correct), ``final_answer_correct`` (bool).
+
+Official metric (per subset, then averaged across the 4 subsets):
+    acc_error   = accuracy on erroneous samples (pred index == gold index)
+    acc_correct = accuracy on correct samples   (pred index == -1)
+    F1          = harmonic_mean(acc_error, acc_correct)
+
+The scoring functions here are pure (no model, no network) so they can be unit
+tested. ``evaluate`` takes a ``verify_fn`` callback that returns k raw V outputs
+for one (problem, steps); Maj@k reduction happens via ``majority_index``.
+"""
+from __future__ import annotations
+
+from dataclasses import dataclass, asdict
+from typing import Callable, Optional, Sequence
+
+from .parse import majority_index
+
+DEFAULT_SPLITS = ("gsm8k", "math", "olympiadbench", "omnimath")
+
+# verify_fn(problem, steps) -> list of k raw V-output strings
+VerifyFn = Callable[[str, list[str]], list[str]]
+
+
+def harmonic_mean(a: float, b: float) -> float:
+    if a + b == 0:
+        return 0.0
+    return 2 * a * b / (a + b)
+
+
+@dataclass
+class SubsetScore:
+    subset: str
+    n_error: int
+    n_correct: int
+    acc_error: float
+    acc_correct: float
+    f1: float
+
+    def as_dict(self) -> dict:
+        return asdict(self)
+
+
+def score_subset(
+    subset: str,
+    gold_labels: Sequence[int],
+    pred_indices: Sequence[int],
+) -> SubsetScore:
+    """Compute acc_error / acc_correct / harmonic-mean F1 for one subset."""
+    assert len(gold_labels) == len(pred_indices)
+    n_error = n_correct = 0
+    hit_error = hit_correct = 0
+    for gold, pred in zip(gold_labels, pred_indices):
+        if gold == -1:
+            n_correct += 1
+            if pred == -1:
+                hit_correct += 1
+        else:
+            n_error += 1
+            if pred == gold:
+                hit_error += 1
+    acc_error = hit_error / n_error if n_error else 0.0
+    acc_correct = hit_correct / n_correct if n_correct else 0.0
+    return SubsetScore(
+        subset=subset,
+        n_error=n_error,
+        n_correct=n_correct,
+        acc_error=acc_error,
+        acc_correct=acc_correct,
+        f1=harmonic_mean(acc_error, acc_correct),
+    )
+
+
+def evaluate(
+    verify_fn: VerifyFn,
+    splits: Sequence[str] = DEFAULT_SPLITS,
+    limit: Optional[int] = None,
+    dataset_id: str = "Qwen/ProcessBench",
+    progress: bool = True,
+) -> dict:
+    """Run V over ProcessBench and return per-subset scores + the averaged F1.
+
+    ``limit`` caps examples per split (use a small value for CPU smoke tests).
+    """
+    from datasets import load_dataset
+
+    try:
+        from tqdm.auto import tqdm
+    except Exception:  # pragma: no cover
+        def tqdm(x, **k):
+            return x
+
+    per_subset: list[SubsetScore] = []
+    for split in splits:
+        ds = load_dataset(dataset_id, split=split)
+        if limit is not None:
+            ds = ds.select(range(min(limit, len(ds))))
+        golds, preds = [], []
+        it = tqdm(ds, desc=f"ProcessBench/{split}") if progress else ds
+        for row in it:
+            samples = verify_fn(row["problem"], list(row["steps"]))
+            preds.append(majority_index(samples))
+            golds.append(int(row["label"]))
+        per_subset.append(score_subset(split, golds, preds))
+
+    avg_f1 = sum(s.f1 for s in per_subset) / len(per_subset) if per_subset else 0.0
+    return {
+        "subsets": {s.subset: s.as_dict() for s in per_subset},
+        "average_f1": avg_f1,
+        "gpt4o_reference_f1": 61.9,
+    }

src/mathcompose/eval/run.py

@@ -0,0 +1,151 @@
+r"""One CLI to run every eval against a base or tuned model and write results.
+
+    # Verifier on ProcessBench (base then tuned -> comparison table):
+    python -m mathcompose.eval.run processbench --adapter runs/verifier_v --maj-k 8
+    python -m mathcompose.eval.run processbench --tag base           # no adapter
+
+    python -m mathcompose.eval.run prmbench --adapter runs/verifier_v --limit 300
+    python -m mathcompose.eval.run math   --adapter runs/generator_g --dataset HuggingFaceH4/MATH-500
+    python -m mathcompose.eval.run compose --gen-adapter runs/generator_g --ver-adapter runs/verifier_v
+
+Each subcommand writes results/<name>_<tag>.json. `report` collates them into a
+markdown table (results/RESULTS.md).
+"""
+from __future__ import annotations
+
+import argparse
+import json
+from pathlib import Path
+
+RESULTS_DIR = Path("results")
+
+
+def _save(name: str, tag: str, payload: dict) -> None:
+    RESULTS_DIR.mkdir(parents=True, exist_ok=True)
+    path = RESULTS_DIR / f"{name}_{tag}.json"
+    path.write_text(json.dumps(payload, indent=2))
+    print(f"\nwrote {path}")
+    print(json.dumps(payload, indent=2))
+
+
+def _runner(base_id, adapter):
+    from .runners import HFRunner
+    return HFRunner(base_id, adapter_path=adapter)
+
+
+def cmd_processbench(a):
+    from .processbench import evaluate
+    from .runners import make_verify_fn
+    r = _runner(a.base_id, a.adapter)
+    verify_fn = make_verify_fn(r, n=a.maj_k, temperature=(0.6 if a.maj_k > 1 else 0.0))
+    res = evaluate(verify_fn, splits=tuple(a.splits), limit=a.limit)
+    _save("processbench", a.tag, res)
+
+
+def cmd_prmbench(a):
+    from .prmbench import evaluate_prmbench
+    from .runners import make_verify_fn
+    r = _runner(a.base_id, a.adapter)
+    verify_fn = make_verify_fn(r, n=a.maj_k, temperature=(0.6 if a.maj_k > 1 else 0.0))
+    res = evaluate_prmbench(verify_fn, limit=a.limit)
+    _save("prmbench", a.tag, res)
+
+
+def cmd_math(a):
+    from .math500 import evaluate_generator
+    from .runners import make_solve_fn
+    r = _runner(a.base_id, a.adapter)
+    solve_fn = make_solve_fn(r, n=a.k, temperature=(0.8 if a.k > 1 else 0.0))
+    res = evaluate_generator(solve_fn, dataset_id=a.dataset, split=a.split,
+                             problem_field=a.problem_field, answer_field=a.answer_field,
+                             limit=a.limit)
+    _save("math", a.tag, res)
+
+
+def cmd_compose(a):
+    from datasets import load_dataset
+    from .compose import evaluate_composition, make_v_scorer
+    from .runners import HFRunner, make_solve_fn
+
+    gen = HFRunner(a.base_id, adapter_path=a.gen_adapter)
+    ver = HFRunner(a.base_id, adapter_path=a.ver_adapter)
+    solve_fn = make_solve_fn(gen, n=a.n, temperature=a.temperature)
+    v_score_fn = make_v_scorer(ver, k=a.ver_k)
+
+    ds = load_dataset(a.dataset, split=a.split)
+    if a.limit:
+        ds = ds.select(range(min(a.limit, len(ds))))
+    problems = [(row[a.problem_field], str(row[a.answer_field])) for row in ds]
+    res = evaluate_composition(problems, solve_fn, v_score_fn)
+    _save("compose", a.tag, res)
+
+
+def cmd_report(a):
+    rows = []
+    for p in sorted(RESULTS_DIR.glob("*.json")):
+        rows.append((p.stem, json.loads(p.read_text())))
+    lines = ["# Results\n"]
+    for name, data in rows:
+        lines.append(f"## {name}\n")
+        lines.append("```json")
+        lines.append(json.dumps(data, indent=2))
+        lines.append("```\n")
+    out = RESULTS_DIR / "RESULTS.md"
+    out.write_text("\n".join(lines))
+    print(f"wrote {out}")
+
+
+def main() -> None:
+    ap = argparse.ArgumentParser(description=__doc__)
+    ap.add_argument("--base-id", default="Qwen/Qwen2.5-Math-1.5B-Instruct")
+    sub = ap.add_subparsers(dest="cmd", required=True)
+
+    p = sub.add_parser("processbench")
+    p.add_argument("--adapter", default=None)
+    p.add_argument("--tag", default="tuned")
+    p.add_argument("--maj-k", type=int, default=1)
+    p.add_argument("--limit", type=int, default=None)
+    p.add_argument("--splits", nargs="+", default=["gsm8k", "math", "olympiadbench", "omnimath"])
+    p.set_defaults(func=cmd_processbench)
+
+    p = sub.add_parser("prmbench")
+    p.add_argument("--adapter", default=None)
+    p.add_argument("--tag", default="tuned")
+    p.add_argument("--maj-k", type=int, default=1)
+    p.add_argument("--limit", type=int, default=None)
+    p.set_defaults(func=cmd_prmbench)
+
+    p = sub.add_parser("math")
+    p.add_argument("--adapter", default=None)
+    p.add_argument("--tag", default="tuned")
+    p.add_argument("--dataset", default="HuggingFaceH4/MATH-500")
+    p.add_argument("--split", default="test")
+    p.add_argument("--problem-field", default="problem")
+    p.add_argument("--answer-field", default="answer")
+    p.add_argument("--k", type=int, default=1)
+    p.add_argument("--limit", type=int, default=None)
+    p.set_defaults(func=cmd_math)
+
+    p = sub.add_parser("compose")
+    p.add_argument("--gen-adapter", default=None)
+    p.add_argument("--ver-adapter", default=None)
+    p.add_argument("--tag", default="compose")
+    p.add_argument("--dataset", default="HuggingFaceH4/MATH-500")
+    p.add_argument("--split", default="test")
+    p.add_argument("--problem-field", default="problem")
+    p.add_argument("--answer-field", default="answer")
+    p.add_argument("--n", type=int, default=8)
+    p.add_argument("--ver-k", type=int, default=4)
+    p.add_argument("--temperature", type=float, default=0.8)
+    p.add_argument("--limit", type=int, default=None)
+    p.set_defaults(func=cmd_compose)
+
+    p = sub.add_parser("report")
+    p.set_defaults(func=cmd_report)
+
+    a = ap.parse_args()
+    a.func(a)
+
+
+if __name__ == "__main__":
+    main()

src/mathcompose/eval/runners.py

@@ -0,0 +1,105 @@
+r"""HF generation wrapper + factory closures used by every eval.
+
+``HFRunner`` loads a base model (optionally with a LoRA adapter merged in),
+applies the chat template, and samples n completions. It imports torch /
+transformers lazily so the rest of the package stays importable on machines
+without them.
+
+Factories:
+  make_verify_fn(runner, n)  -> verify_fn(problem, steps) -> list[str]   (Model V)
+  make_solve_fn(runner, n)   -> solve_fn(problem)         -> list[str]   (Model G)
+"""
+from __future__ import annotations
+
+from typing import Callable, Optional
+
+from ..common.chat import verifier_messages, generator_messages
+
+
+class HFRunner:
+    def __init__(
+        self,
+        base_id: str,
+        adapter_path: Optional[str] = None,
+        device: Optional[str] = None,
+        dtype: str = "auto",
+        max_context: int = 4096,
+        pad_token: str = "<|fim_pad|>",
+    ):
+        import torch
+        from transformers import AutoModelForCausalLM
+
+        from ..common.chat import load_tokenizer
+
+        self.tokenizer = load_tokenizer(base_id, pad_token=pad_token)
+        self.max_context = max_context
+        self.device = device or ("cuda" if torch.cuda.is_available() else "cpu")
+
+        torch_dtype = {"auto": "auto", "bf16": torch.bfloat16, "fp16": torch.float16,
+                       "fp32": torch.float32}.get(dtype, "auto")
+        # transformers 5.x: `dtype=` (torch_dtype is deprecated)
+        model = AutoModelForCausalLM.from_pretrained(base_id, dtype=torch_dtype)
+        if adapter_path:
+            from peft import PeftModel
+
+            model = PeftModel.from_pretrained(model, adapter_path)
+        self.model = model.to(self.device).eval()
+
+    def chat(
+        self,
+        messages: list[dict],
+        n: int = 1,
+        temperature: float = 0.0,
+        max_new_tokens: int = 1024,
+        repetition_penalty: float = 1.1,
+    ) -> list[str]:
+        """Return n decoded completions (generated text only)."""
+        import torch
+
+        # transformers 5.x returns a BatchEncoding (dict) here, not a bare tensor.
+        enc = self.tokenizer.apply_chat_template(
+            messages, add_generation_prompt=True, return_tensors="pt", return_dict=True,
+        )
+        input_ids = enc["input_ids"]
+        attn = enc.get("attention_mask")
+
+        # keep room for generation under the hard context ceiling
+        max_prompt = max(1, self.max_context - max_new_tokens)
+        if input_ids.shape[-1] > max_prompt:
+            input_ids = input_ids[:, -max_prompt:]
+            if attn is not None:
+                attn = attn[:, -max_prompt:]
+        input_ids = input_ids.to(self.device)
+        attn = attn.to(self.device) if attn is not None else None
+
+        do_sample = bool(temperature and temperature > 0)
+        gen_kwargs = dict(
+            max_new_tokens=max_new_tokens,
+            do_sample=do_sample,
+            num_return_sequences=n,
+            pad_token_id=self.tokenizer.pad_token_id,
+            repetition_penalty=repetition_penalty,
+        )
+        if do_sample:
+            gen_kwargs.update(temperature=temperature, top_p=0.95)
+
+        with torch.no_grad():
+            out = self.model.generate(input_ids, attention_mask=attn, **gen_kwargs)
+        gen = out[:, input_ids.shape[-1]:]
+        return self.tokenizer.batch_decode(gen, skip_special_tokens=True)
+
+
+def make_verify_fn(runner: HFRunner, n: int = 1, temperature: float = 0.0,
+                   max_new_tokens: int = 1024) -> Callable[[str, list[str]], list[str]]:
+    def verify_fn(problem: str, steps: list[str]) -> list[str]:
+        return runner.chat(verifier_messages(problem, steps), n=n,
+                           temperature=temperature, max_new_tokens=max_new_tokens)
+    return verify_fn
+
+
+def make_solve_fn(runner: HFRunner, n: int = 1, temperature: float = 0.0,
+                  max_new_tokens: int = 1024) -> Callable[[str], list[str]]:
+    def solve_fn(problem: str) -> list[str]:
+        return runner.chat(generator_messages(problem), n=n,
+                           temperature=temperature, max_new_tokens=max_new_tokens)
+    return solve_fn

src/mathcompose/infer/demo.py

@@ -0,0 +1,67 @@
+r"""Inference demo for Model V and Model G, with a base-vs-tuned side-by-side
+mode for the demo video.
+
+    # Verify a solution with the tuned verifier:
+    python -m mathcompose.infer.demo --task v --adapter runs/verifier_v \
+        --problem "Compute 1+1." --steps "We add." "1+1=3."
+
+    # Solve a problem:
+    python -m mathcompose.infer.demo --task g --adapter runs/generator_g \
+        --problem "What is 12*11?"
+
+    # Base vs tuned side by side (the money shot for the video):
+    python -m mathcompose.infer.demo --task v --adapter runs/verifier_v --compare \
+        --problem "..." --steps "..." "..."
+"""
+from __future__ import annotations
+
+import argparse
+
+from ..common.chat import verifier_messages, generator_messages
+from ..data.schema import parse_verifier_output
+
+
+def run_verifier(runner, problem: str, steps: list[str], temperature: float = 0.0) -> str:
+    out = runner.chat(verifier_messages(problem, steps), n=1, temperature=temperature,
+                      max_new_tokens=1024)[0]
+    parsed = parse_verifier_output(out)
+    verdict = ("all steps correct" if parsed.first_error_index == -1
+               else f"first error at step {parsed.first_error_index}")
+    return f"[V verdict: {verdict}]\n{out}"
+
+
+def run_generator(runner, problem: str, temperature: float = 0.0) -> str:
+    return runner.chat(generator_messages(problem), n=1, temperature=temperature,
+                       max_new_tokens=1024)[0]
+
+
+def main() -> None:
+    ap = argparse.ArgumentParser(description=__doc__)
+    ap.add_argument("--task", choices=["v", "g"], required=True)
+    ap.add_argument("--base-id", default="Qwen/Qwen2.5-Math-1.5B-Instruct")
+    ap.add_argument("--adapter", default=None, help="path/hub id of the tuned adapter")
+    ap.add_argument("--problem", required=True)
+    ap.add_argument("--steps", nargs="*", default=None, help="solution steps (task v)")
+    ap.add_argument("--temperature", type=float, default=0.0)
+    ap.add_argument("--compare", action="store_true", help="show base vs tuned")
+    args = ap.parse_args()
+
+    from ..eval.runners import HFRunner
+
+    def do(runner, tag):
+        print(f"\n===== {tag} =====")
+        if args.task == "v":
+            print(run_verifier(runner, args.problem, args.steps or [], args.temperature))
+        else:
+            print(run_generator(runner, args.problem, args.temperature))
+
+    if args.compare:
+        do(HFRunner(args.base_id, adapter_path=None), "BASE (untuned)")
+        if args.adapter:
+            do(HFRunner(args.base_id, adapter_path=args.adapter), "TUNED")
+    else:
+        do(HFRunner(args.base_id, adapter_path=args.adapter), "TUNED" if args.adapter else "BASE")
+
+
+if __name__ == "__main__":
+    main()