Section 7.3, paragraph 2Imitation training of the four heads (seed 7, 12 epochs, 2×10⁵ examples)

Empirical result Supported by saved experimental runs, not by a proof.

1 Paper text

The network uses the same shared-trunk architecture as Table 1 (two hidden layers of width $H=256$ with LayerNorm), with $B$ independent linear output heads each producing $N \cdot 2^k = 320$ action logits. Training uses Adam (learning rate $10^{-3}$ , batch size 1024) for 12 epochs on $2\times10^5$ imitation examples, with a separate 20,000-example validation set and seed 7 in the saved notebook.

Generated from paper_jmlr.tex, lines 1156–1157.

2 Explain this

The four heads share a trunk (two hidden layers of width 256 with LayerNorm) and have separate linear outputs of 320 logits each. They are trained by imitation of $\pi_0,\dots,\pi_3$ with soft targets: Adam, learning rate $10^{-3}$ , batch 1024, 12 epochs, $2\times10^5$ examples, a 20,000-example validation set, seed 7.

3 How this is formalised

How this is covered. Empirical setup from the saved notebook; not formalised.

Coverage record
Paper anchor	`par-training-the-rollout-heads-p2` (website anchor; the manuscript has no label here)
Displayed as	Section 7.3, paragraph 2
Claim	Imitation training of the four heads (seed 7, 12 epochs, 2×10⁵ examples)
Coverage category	Empirical result
Statement source	paper_jmlr.tex lines 1156–1157; SHA-256 of the normalised block source `e6f5aa9a0ee2ccb6…`
Explanations	`explain/c-fsm-training`, `formal/c-fsm-training`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

No Lean statement corresponds to this claim. This is an empirical statement about saved experimental runs. Lean proofs do not certify training runs, curves or checkpoints.

Build evidence: fresh isolated rebuild of all 38 bundled modules with Lean (version 4.26.0, started 2026-10-10T15:21:56Z, finished 2026-10-10T15:27:00Z: 38/38 modules compiled, 1588 axiom reports, no errors. See Build for the commands and the independent audit of 2026-10-10 (dated evidence).