Pretraining ablations, week of September 21, 2026

For context, see previous work.

Summary #

I set up auto research to determine what pretraining setup would lead to the best RL performance on our natural deduction task.

The only optimizations agents made to the pretrain that I was confident worked before checking the held-out set were:

1. Lean tokenizer
2. Muon optimizer

Leon’s new RL recipe does much better on recipe 39 I sent him than on recipe 1 (~2x more proofs). And held-out performance correlates very strongly with validation performance. These update me against p-hacking and make me more inclined to accept Fable’s crazy experiments.

If you made me ship a pretrain implementation to the core of the repo today, I would probably ask Claude to simplify what I have a fair amount, run it again, and if performances drop <10% just use that.

Graphs below mention ‘lean era’ and ‘token era.’ Halfway through the week I updated my tokenizer to use lean because Dan did this and saw much better results. This led to a step change in performance and thus I split my graphs up into before lean and after lean.

Mistakes Made: #

1. It took me far too long to realize that the agents thought speedups were out of bounds (and thus they were training tiny models). Torch.compile didn’t even work. Claude is somehow struggling mightily to get this to work right now, it’s still not done, which I feel bad about.
2. In general, I spent way too many tokens letting autoresearch spin without validating its outputs.

Methodology: #

1. Freeze training data to Dan’s set (155k pretrain examples, 1.5k RL proofs for expert iteration, 1.1k proofs not trained on and used to decide whether run is kept, 1.2k proofs held out until after runs finish)
2. Advance based on pass@64 on the eval set.
3. Freeze RL methodology (very vanilla expert iteration)
4. Freeze GPU budget: 300s of pretrain, ~2,100 seconds of RL (both of these numbers got increased).
5. Parameter cap of 10m. Almost never got hit because pretrain time was the limiting factor

The Winning Model #

Run 153-claude⁠^[1]

How it got here: every kept Lean-protocol change, each 3-seed mean vs the previous incumbent.

Not in the winner: 150-fable’s bigram embedding table also kept (673), landing two minutes after 151 and briefly replacing it at HEAD, but 153 was built on 151 and overwrote it. The exact table (107² x 384 = 4.4M params) does not fit under the cap at width 384; 155-claude re-added it low-rank (11,449 x 32 table + 32 -> 384 projection) and scored 668 vs 687, with round-1 targets solved down 43% (419 vs 736). Full-rank vs low-rank and width are confounded there.

Findings #

Does Pretrain Loss Correlate With RL Theorems Learned? #

A: Not really. You would expect a negative sign below:

• Token era: $r = -0.29$, Spearman $\rho = -0.24$ ($n = 81$)
• Lean era: $r = +0.21$, Spearman $\rho = +0.29$ ($n = 99$)

Outliers excluded: label smoothing (017) in the token era, and in the Lean era the two broken runs (166-fable2, 162-fable) that are off the chart.

Validation Theorems Solved vs Held-Out Theorems Solved #

• Token era: $r = 0.998$, Spearman $\rho = 0.995$ ($n = 82$)
• Lean era: $r = 0.99$, Spearman $\rho = 0.99$ ($n = 100$)

Pretrain Loss, RL Theorems #

The bottom panel is 72 textbook problems that no run trained or was selected on, scored offline like the holdout, at 256 samples per problem.⁠^[2] They track dev less tightly than the holdout does:

• Token era: $r = 0.88$, Spearman $\rho = 0.86$ ($n = 82$)
• Lean era: $r = 0.76$, Spearman $\rho = 0.73$ ($n = 99$)

The best textbook run, the bigram table (150), solves 21.7 of 72 on average over its three seeds. It was kept, but it ties for tenth on dev. The incumbent (153) solves 18.7.

Progress on longer theorems: #

Length here is the shorter of two proofs of each theorem: the model’s shortest verified proof (with uncited lines pruned) and the deterministically-generated reference proof.⁠^[3]⁠^[4]

Pass@k Curves #

Potpourri #

LoC over time #

The model is one file, pretrain.py, the only file agents edit. It builds on frozen modules from Dan’s fork (the base GPT and Block classes, the tokenizer, the loss), so this counts what the loop added on top, not the whole model.

Why Does the Lean Tokenizer Work so much Better? #

I suspect it has a lot to do with depth invariance. Stealing Dan’s unary-| hypothesis:

In the ND world, if the model is in a depth-three box, it has to write something like

N13 | | | P : AS ;
N14 | | | (QvP) : ORI2 N13 ;

Whereas in the Lean world depth is not marked by bars but by parens:

( fun ( n14 : P ) => by
    have n15 : (Q ∨ P) := Or.inr n14 ;
    exact n15 )

There are more parens wrapped around this fun, but locally we don’t care about them.

How Do We Deal With Relative References and Getting Past 7 Lines? #

We number statements, eg:

N1 (PvQ) : PR ;
  N2 | P : AS ;
  N3 | (QvP) : ORI2 N2 ;
  N4 | Q : AS ;
  N5 | (QvP) : ORI1 N4 ;
N6 (QvP) : ORE N1 N2 N3 N4 N5 ; QED

We then add a random offset so that the model sees more than six ‘name’ tokens:

-- ND, offset +11
N12 (PvQ) : PR ;
  N13 | P : AS ;
  N14 | (QvP) : ORI2 N13 ;
  N15 | Q : AS ;
  N16 | (QvP) : ORI1 N15 ;
N17 (QvP) : ORE N12 N13 N14 N15 N16 ; QED

-- Lean, offset +11
have n12 : (P ∨ Q) := h1 ;
have n13 : (Q ∨ P) := Or.elim n12
    ( fun ( n14 : P ) => by
        have n15 : (Q ∨ P) := Or.inr n14 ;
        exact n15 )
    ( fun ( n16 : Q ) => by
        have n17 : (Q ∨ P) := Or.inl n16 ;
        exact n17 ) ;
exact n13

In practice offset is random 0-64. I did not ablate this.

Longer Summary of Results (Claude Written) #

Top 10 single-change jumps. Metric: dev theorems solved at length $\geq 7$, mean of seeds 0/1/2. Delta is vs the incumbent the run was compared against. Protocol changes are excluded.

Just below the cutoff: 129 (LR floor 0.1 → 0.3, +15), 153 (width 384, +15), 150 (bigram table, +14), 151 (width 320, +14).

Protocol jumps (not comparable, not ideas): 000 → 012 (56 → 148, 600 s → 1200 s harness and 3-seed bar); 081 → 100 (404 → 563, Lean tokenizer + Lean ∧ nd_verify reward + 2400 s).

Noise: pooled one-seed sd is 41.6 (token era) and 44.7 (Lean era), so the SE of a difference of two 3-seed means is ~36. Only Muon (~1.8 SE) and Polar Express (~1.3 SE) clear it. Ranks 6, 8 and 10 (+52 combined) came from the AdamW finish, which 040 then deleted at a tie. Keeps are selected for being high, so kept deltas overstate true effects. 153 (687) has held for 30+ runs (154–184), many of which scored 670–685.

By era: token era 148 → 404 (2.7×), almost all from the Muon family. Lean era 563 → 687 (+22%), from architecture and position encoding, plus spending 148’s token-batching speed on width.