Section 7.2.5, paragraph 2Checkpoint diagnostic: almost all remaining errors differ from the required change only in the lowest bit
Empirical result Supported by saved experimental runs, not by a proof.
1 Paper text
A diagnostic of the saved checkpoints makes the remaining difficulty more concrete. For a predicted move setting heap to , compare its proposed change with the required nim-sum of . On the reconstructed and independently verified 100,000-position test set, the epoch-23 model makes only legal moves and gets the upper three bits of this change jointly correct on 99.998% of examples. Of its 46,206 failed moves, 46,204 differ from the correct change only in the lowest bit. At epoch 45 all 12,437 errors are confined to that bit; at epoch 178 only two errors remain, both of the same kind. These diagnostic counts weight examples equally, unlike the saved batch-mean accuracies plotted above.
Generated from paper_jmlr.tex, lines 1129–1129.
2 Explain this
A closer look at the saved checkpoints makes the plateau concrete. For a predicted move "set heap to ", compare the change it makes, , with the change needed (the nim-sum of ):
- at epoch 23 the model makes only legal moves and gets the upper three bits of the change right on 99.998% of the 100,000 test positions; of its 46,206 failures, 46,204 are wrong only in the lowest bit;
- at epoch 45 all 12,437 errors are in that bit; at epoch 178 only two errors remain, both of that kind.
These counts weight examples equally, unlike the batch-mean accuracies in the figures.
3 How this is formalised
How this is covered. An empirical diagnostic computed from the saved checkpoints on a reconstructed and independently verified test set, as stated in the paper. Not formalised; the edition does not recompute it.
| Paper anchor | par-learning-in-stages-the-plateau-and-subsequent-improvement-p2 (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 7.2.5, paragraph 2 |
| Claim | Checkpoint diagnostic: almost all remaining errors differ from the required change only in the lowest bit |
| Coverage category | Empirical result |
| Statement source | paper_jmlr.tex lines 1129–1129; SHA-256 of the normalised block source 9749a9392e996382… |
| Explanations | explain/c-diagnostic, formal/c-diagnostic |
| 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).