M1: the first curriculum rung
Multi-turn GRPO on a deliberately harder Lean tier, asking two questions: (i) can we train on M1 from scratch, and (ii) does training on M0 first provide uplift? Companion to the M0 results page.
Round-2 recap: cold-per-rung wins; warm starts cost ~20pts of next-tier transfer; scratch models zero-shot the next tier at 78–82%. Round-3 budget: ~$12 of $300 spent.
Why this round
M0 established that GRPO on Tinker trains open models on locally-graded Lean
proof-completion (18%→88.5% single-turn; multi-turn credit assignment verified).
The plan (PR #138,
docs/curriculum-plan.md) is a ladder to the real Rocq→Lean task where each rung
moves one axis: rollout length, difficulty, or infra.
M0 ──────► M1 ──────► M2 ──────► M3 ──────► M4 ──────► M5 ──────► M6
(done) (THIS)
one-shot multi-turn tool loop containers harder Rocq real binary-
tactic + harder (run lean, + sandboxed Lean syntax, equivalence
block tier, w/ read goal, grading (mathlib- toy tasks
grader edit) style) theorems (seeded)
feedbackM1 moves the difficulty axis while keeping the multi-turn loop M0 already validated (rl11: 40%→92.3%). The interesting scientific question is the transfer one: M0's warm-start experiments cut both ways — SFT warm-starts capped the RL ceiling (entropy collapse: 79.8% vs cold 88.5%), while the output-protocol skills RL taught were worth ~60 points. Does "train on M0 first" behave like a head start or a trap?
Hypotheses (with priors, set before launch)
| id | claim | prior | evidence that moves it |
|---|---|---|---|
| H6 | Multi-turn GRPO trains from scratch at a 3–5% turn-1 frontier | 0.70 | train-reward slope over first 20 iters of rl12 |
| H7a | M0-first gives a head start on M1 (higher curve early) | 0.85 | rl13 phase-1 entry vs rl12 at same iter count |
| H7b | M0-first raises (not caps) the final M1 plateau | 0.60 | final heldout of rl13 vs rl12; watch for entropy-trap signature (pass@1≈pass@k) |
| H9 | Lean error feedback is informative at this tier (turn-2 conditional pass > turn-1) | 0.80 | solved_by_n_turns in evals |
Numbering continues the M0 scratchpad's H1–H5; full set incl. H8, H10–H12
in docs/curriculum-plan.md.
How it's all built, in plain terms
The task
Every task is one Lean 4 file: a few custom definitions (fresh random names like
revr17, so nothing can be pattern-matched from a library) plus one theorem whose
proof is sorry. The model sees that file and answers with ONLY a tactic block in a
```lean fence. The harness — never the model — splices that block into the fixed
statement, so weakening the theorem or smuggling axioms is impossible by construction.
How a dataset (rung) gets built
Each rung is a set of parametric generator functions (~30 lines each in
src/factory.py): a generator picks random names and constants, renders the
definitions, the statement, and — crucially — a gold proof written as a template.
The build script (scripts/build_dataset.py --set m3) generates 240 candidates, runs
every gold proof through the real grader, and ships only tasks whose golds certify (M1–M5 all
certified 240/240). A stratified split (5 heldout per family) is frozen at build time and never
changes. Before writing a generator, each gold-proof pattern is verified by hand as a
standalone Lean file — that iteration loop is minutes, not hours. Every rung also includes a
1-in-6 "bridge" family of trivial concrete evaluations — round 2 proved these are load-bearing:
without them, cold-start GRPO gets zero reward everywhere and no gradient.
The grader (and why there are no containers)
Grading is a plain local Python function, grade_sync — no Docker, no service:
(1) reject forbidden tokens (sorry, axiom, native_decide,
set_option, …); (2) splice the tactic block into the fixed file; (3) run
lean file.lean as a subprocess (~0.07–2s); (4) parse the #print axioms
output and require it to be a subset of {propext, Quot.sound, Classical.choice} —
this is what catches a smuggled sorry (it surfaces as sorryAx).
Concurrency is a semaphore of ≤16 lean processes. Containers only enter the plan at the
tool-loop rung (see docs/curriculum-plan.md): once the model can run commands or
edit files, grading needs isolation; until then a local function is faster and has no
orchestration bugs.
Rollouts: multi-turn, but no tool calling
There is deliberately no tool-calling protocol. A training episode is: prompt → model emits a tactic block → harness grades it → if it failed, the grader's error output is appended as a plain user message ("Your proof failed: … Provide a corrected tactic block") and the model tries once more (2 turns in training, up to 3 in evals). The model's move is always one fenced tactic block. GRPO treats the whole episode as one unit: reward 1 if any turn passed, group-centered advantages applied to every sampled token of every turn. Tool calling is the next infra rung on the ladder, not part of these rounds.
Rung by rung: what each dataset actually contains
Every rung: 240 tasks (200 hard + 40 tier-1 bridge), 6 parametric families, 210 train / 30 heldout (5 per family), 100% gold-certified, fresh random names per task. "cold base" = gpt-oss-20b multi-turn baseline on that rung's heldout.
M0 — the de-risk pools (v1–v4, 46→317 tasks)
Hand-written templates first (concrete arithmetic, single inductions, helper-lemma
list/tree lemmas), then the v4 parametric factory (affine recursions
f (n+1) = f n + c ⊢ closed forms, repeat/sum/len). Cold base 18–23%.
M1 — first hard tier (cold base 5.0%)
| family | statement shape | what makes it hard |
|---|---|---|
| poly_square (t4) | f(n+1)=f n+2n+1 ⊢ f n = n²+b | nonlinear closed form: must normalize with succ_mul/mul_succ before omega can see it |
| compose_affine (t4) | g(g n) = c²n + (ca+a) | invent a closed-form helper, compose it with itself |
| map_rev (t4) | map f (rev l) = rev (map f l) | needs a map-over-append helper lemma |
| fold_rev (t4) | sum/count invariant under reverse | fold-over-append helper |
| revacc (t5) | accumulator reverse = naive reverse | the classic puzzle: helper must be ∀-quantified over the accumulator, plus two append lemmas |
| concrete (t1 bridge) | f 7 = 52 | rfl — keeps early groups off zero variance |
M2 — multi-helper chains (cold base 10.0%)
| family | statement shape | hardness |
|---|---|---|
| rev_invol (t6) | rev (rev l) = l | three chained helpers: app_nil, app_assoc, rev-over-app |
| sum_map_mul (t5) | sum (map (c·) l) = c · sum l | induction + distributivity |
| count_filter (t5) | count k (filter p l) ≤ count k l | double case-split (p x × x==k) per step |
| compose_two (t5) | f (g n) closed form, f≠g | two independent closed-form helpers |
| height_mirror (t5) | height (mirror t) = height t | tree induction + Nat.max_comm |
| concrete (bridge) | eval of sum∘map | rfl |
M3 — accumulators & double induction (cold base 23.3%)
| family | statement shape | hardness |
|---|---|---|
| sumacc (t6) | sacc l 0 = sum l | generalize to ∀ acc: sacc l acc = sum l + acc or the induction fails |
| tsumacc (t7) | tree sum with threaded accumulator | same generalization, two recursive calls threading acc through both branches |
| takedrop_len (t6) | len (take n l) + len (drop n l) = len l | induction on n with inner case-split on l, ih applied at xs |
| pow_mul (t7) | b^(n·m) = (b^n)^m | needs pow-of-sum helper, then nested induction with mul_comm juggling |
| filter_idem (t6) | filter p (filter p l) = filter p l | if-split where the hypothesis must be reused inside the branch |
| concrete (bridge) | accumulator eval | rfl |
M4 — the hardest cliff (cold base 1.7%!)
| family | statement shape | hardness |
|---|---|---|
| insert_count (t7) | count j (ins k l) = [k==j] + count j l | positional insert has an if in the recursion; proof needs induction × two case-splits |
| flatten_tsum (t7) | sumlist (flatten t) = tsum t | sum-over-append helper + tree induction |
| pow_lt_mono (t7) | n < m → 2^n < 2^m | an IMPLICATION: induction must carry the hypothesis, plus a positivity helper |
| rev_map_rev (t7) | rev (map f (rev l)) = map f l | composed helper chain through two structures |
| count_take_le (t7) | count k (take n l) ≤ count k l | double induction + case-split |
| concrete (bridge) | ins/flatten eval | rfl |
M5 — the target rung: insertion sort (cold base 6.7%)
| family | statement shape | hardness |
|---|---|---|
| isort_count (t8) | count j (isort l) = count j l | permutation-by-counts: needs the insert-count lemma as a helper, then sort induction |
| isort_len (t8) | len (isort l) = len l | insert-length helper + induction |
| isort_sorted (t8) | sortedb (isort l) = true | the invariant proof: insert preserves sortedness — case analysis inside an inductive invariant |
| mirror_flatten (t8) | flatten (mirror t) = rev (flatten t) | 3-helper chain (rev/app laws) woven into tree induction |
| gauss_div (t8) | f n = n(n+1)/2 + a (real Nat division) | prove the 2× version by induction, then let omega handle the /2 |
| concrete (bridge) | isort eval | rfl |
The M1 dataset: 240 certified tasks, built to sit on the frontier
Same recipe as M0 (parametric generators → gold proof per task → every gold certified by the real grader before shipping — 240/240 passed first build), but the families are a tier harder. Six families, ~1-in-6 tasks is an easy "bridge" so early groups aren't all zero-variance:
| family | tier | what makes it hard |
|---|---|---|
m1_poly_square | 4 | f (n+1) = f n + 2n+1 ⊢ f n = n²+b — nonlinear closed form; needs the right simp-normalization before omega can see it |
m1_compose_affine | 4 | g (g n) = c²·n + (c·a+a) — must invent a closed-form helper lemma, then compose it with itself |
m1_map_rev | 4 | map f (rev l) = rev (map f l) — needs a map-over-append helper |
m1_fold_rev | 4 | sum/count invariant under reverse — needs a fold-over-append helper |
m1_revacc | 5 | tail-recursive reverse = naive reverse — the classic generalize-the-accumulator puzzle (helper must be ∀-quantified over acc) plus two append lemmas |
m1_concrete | 1 | bridge: concrete evaluation of the quadratic recursion (rfl) |
Every task gets fresh random function names (revr17, zetaq42, …) so
memorized lemma names from M0 training don't apply — the induction structure has to be found.
Split: 210 train / 30 heldout, stratified 5-per-family. Lives at data/m1/tasks.jsonl
(the data dir is now organized as data/m0/ + data/m1/).
Frontier calibration: the band is exactly where a rung wants it
Before spending on RL, both reference policies ran the M1 heldout (30 tasks × 2 repeats, 2 turns with error feedback, $0.30 total):
| family (10 attempts each) | base 20b | rl5 ckpt (M0-trained) |
|---|---|---|
| m1_concrete (bridge) | 3/10 | 10/10 |
| m1_poly_square | 0/10 | 9/10 |
| m1_map_rev | 0/10 | 10/10 |
| m1_fold_rev | 0/10 | 9/10 |
| m1_compose_affine | 0/10 | 0/10 |
| m1_revacc | 0/10 | 1/10 |
Two headlines. First, zero-shot M0 transfer is huge (5%→65% without ever seeing an M1 task): the induction/helper-lemma skills and output protocol generalize to new families and names. Second, the dataset still has a genuine frontier — two families the M0-trained policy can't touch. That 0→65% spread across policies is the shape a curriculum rung wants: trainable-from-warm, cliff-from-cold, headroom for both.
The two arms
| rl12-m1-scratch | rl13-m1-warm | |
|---|---|---|
| question | (i) trainable from scratch? | (ii) does M0-first help? |
| schedule | 60 iters on m1 | 25 iters on m0/v4pool (phase 0), then 60 iters on m1 |
| eval | same fixed m1 heldout (30 tasks, k=4 episodes), every 10 iters, throughout both phases | |
| shared knobs | gpt-oss-20b · LoRA rank 32 · lr 4e-5 · importance-sampling GRPO · G=8 episodes × 12 problems/iter · max_turns 2 · temp 1.0 · 8k tokens/turn | |
Round 2b: two more arms + the next rung's dataset (launched 04:30 UTC)
| run | question | design |
|---|---|---|
| rl14-m1-nobridge | was the tier-1 bridge load-bearing for the cold start (H8)? | scratch, 60 iters, m1 train WITHOUT the 40 bridge tasks; identical heldout |
| rl15-m1-120b | does the rung transfer across model scale? | gpt-oss-120b scratch, 40 iters, same m1 tasks (+ base-120b calibration eval) |
| data/m2/ | next difficulty tier, pre-built & certified (240/240) | multi-helper chains (rev∘rev=id needs 3 helpers), double case-splits, two-function composition; zero-shot calibration vs the M1 finals when they land |
Round 2c: the M2 rung (launched 06:45 UTC)
| run | schedule | question |
|---|---|---|
| rl16-m2-scratch | 40it m2 | cold-start on the harder tier |
| rl17-m2-warmM0 | 25it m0 → 40it m2 | one-rung skip (does M0 transfer stretch two tiers?) |
| rl18-m2-warmM0M1 | 25it m0 → 25it m1 → 40it m2 | the full ladder climb — does sequential curriculum beat skipping? |
All on the fixed m2 heldout (30 tasks). The trainer now supports arbitrary multi-phase curricula (comma-separated pre-phase files).
Round 3: M5-race heldout trajectory (m5 heldout; HW-test arms on their own rungs)
| iter | rl21 cold-20b | rl22 cold-120b | rl23 ladder | rl24 mixed | rl25 m4-cold | rl19 m3hard-cold |
|---|---|---|---|---|---|---|
| — (base) | 6.7% | 13.3% | 6.7% | 6.7% | 1.7% (m4) | ~8% (m3-hard) |
| 9 | 15.0% | — | 21.7% (m3 phase) | 15.0% | 18.3% | 43.3% |
M2 heldout trajectory (multi-turn pass, k=4)
| iter | rl16-cold | rl17-M0→M2 | rl18-M0→M1→M2 |
|---|---|---|---|
| — (refs) | base-20b 10.0% · M1-trained zero-shots: rl15 (120b) 81.7% · rl12 (20b) 78.3% | ||
| 9 | 47.5% | 51.7% (m0 phase) | 45.0% (m0 phase) |
| 19 | 65.8% | 60.8% (m0) | 55.0% (m0) |
| 29 | 75.8% | 66.7% | 60.8% (m1 phase) |
| 39–49 | 77.5% final (p@4 97%) | 70.0% → 65.0% (stopped @49, budget) | 56.7% → 55.0% (m1 phase — m2 score STALLS during m1 training) |
| 59–69 | — | — | 65.8% → 71.7% (m2 phase, still rising; stopped @69, budget) |
M2 calibration: base-20b 10.0% mt (bridge only — same cliff shape as M1). And the round's most striking transfer result: rl15's M1-trained 120b zero-shots the M2 heldout at 81.7% (turn-1 70%; rev_invol 8/10, compose_two 8/10, only count_filter lags at 4/10). And it's not a scale effect: rl12's M1-trained 20b zero-shots M2 at 78.3% (turn-1 63%) — within noise of the 120b. Climbing one rung nearly solves the next for free at both scales — but only for the scratch-trained model: rl13, the M0-warm-started arm that matched rl12 on the M1 heldout (75.8% vs 77.5%), zero-shots M2 at just 58.3%, 20 points behind. The warm start's hidden cost isn't the in-distribution plateau — it's off-distribution generalization. The binding constraint is per-rung skill acquisition, not task novelty.
Why phase-0-in-one-process rather than loading the rl5 checkpoint: Tinker sampler-weights
checkpoints can't seed a training client (create_training_client_from_state rejects
them — only save_state training checkpoints load). Both new runs save proper
training state at the end, so future rungs can warm-start directly.
Results updating live
So far: rl12-m1-scratch train reward flat at 5–10% through iter 7 (2–5 of 12 groups producing gradient — the cold-start cliff is binding, H6 under real stress). rl13-m1-warm climbed its M0 phase 8%→73% train reward by iter 9, and its iter-9 M1 heldout eval — before a single M1 training task — reads 48.3% (pass@4 70%).
Heldout trajectory (m1 heldout, multi-turn pass rate, k=4 episodes/task)
| iter | rl12-m1-scratch | rl13-m1-warm |
|---|---|---|
| — (baselines) | 5.0% (base 20b) | 65.0% (rl5 ckpt ref) |
| 9 | 14.2% (p@4 37%) | 48.3% (phase 0 — M0 tasks only; p@4 70%) |
| 19 | 53.3% (p@4 73%) | 52.5% (end of phase 0; p@4 70%) |
| 29 | 63.3% (p@4 77%) | 60.8% (4 M1-iters into phase 1; p@4 80%) |
| 39 | 68.3% (p@4 83%) | 67.5% (p@4 83%) |
| 49 | 78.3% | 65.8% |
| 29 (rl15-120b) | 72.5% | |
| 19 (rl15-120b) | 68.3% — the 120b matches the 20b's iter-39 level in half the iterations | |
| 59 | 77.5% final (p@4 93%) | 71.7% |
| 69–84 | — | 73.3% → 74.2% → 75.8% final (p@4 93%) |
| 39 (rl15-120b) | 72.5% final (p@4 93%) — and zero-shots M2 at 81.7% | |
| 10 (rl14-nobridge) | STOPPED: reward 0.00, heldout 6.7% ≈ baseline. Without bridge tasks, cold-start GRPO starves — the tier-1 bridge is load-bearing (H8 confirmed) | |
| 9 (rl15-120b) | 51.7% — the 120b goes 5%→51.7% in 9 iters (vs ~19 for the 20b); rl14-nobridge still ~2% train reward at iter 3 | |
Infra changes this round (all flags, no forks)
MTConfiggrewphase0_tasks_file/phase0_iters— curriculum phase switch inside one trainer, task pool reset at the boundary, phase recorded in metrics.save_state— train-resumable checkpoints (the thing sampler weights can't do), so M2+ can continue training any M1 policy.- Multi-turn trainer now writes
rollouts.jsonl(episode texts + per-turn verdicts) — fixes the gap that kept rl11 off Docent; uploaders render full feedback conversations. tests/: 21 pytest cases — task model, generator determinism/uniqueness, dataset invariants (splits, id-disjointness from M0), grader forbidden-token + compile paths, phase scheduling.data/reorganized:m0/(v1–v4 frozen) +m1/, compat symlinks for old configs.
Links
- PR #138 — all code, data, and docs for this work (see
docs/curriculum-plan.mdfor the M0→M6 ladder + bayesian hypotheses) - M0 results page — round 1: model grid, single-turn RL, SFT ablations, multi-turn RL
- Docent: all transcripts — filter
metadata.run=mt-m1-base-20b,mt-m1-rl5ckpt,rl12-m1-scratch,rl13-m1-warm