Section 7.2.3, paragraph 1Training protocol and the ten saved checkpoints
Empirical result Supported by saved experimental runs, not by a proof.
1 Paper text
We train each model with supervised learning using cross-entropy to the soft target distribution. We use Adam with learning rate and batch size 512 for 200 epochs. To study performance as a function of training, we save checkpoints per model at epochs
Generated from paper_jmlr.tex, lines 1089–1093.
2 Explain this
Both models are trained with Adam (learning rate , batch size 512) for 200 epochs, and ten checkpoints are saved at epochs 1, 23, 45, 67, 89, 112, 134, 156, 178 and 200.
3 How this is formalised
How this is covered. Empirical setup; not formalised. The edition uses the saved checkpoints' results only and does not create intermediate checkpoints.
| Paper anchor | sec-training-and-checkpoints-p1 (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 7.2.3, paragraph 1 |
| Claim | Training protocol and the ten saved checkpoints |
| Coverage category | Empirical result |
| Statement source | paper_jmlr.tex lines 1089–1093; SHA-256 of the normalised block source f02efd47ec196f3c… |
| Explanations | explain/c-exp-training, formal/c-exp-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).