Section 7.2.4, “Restoration accuracy (validation/test)”Restoration accuracy: unmasked argmax in the optimal support; batch-mean convention
Empirical result Supported by saved experimental runs, not by a proof.
1 Paper text
Restoration accuracy (validation/test). Given a held-out example, the saved evaluation takes the argmax over all action logits and counts it as correct if it lies in the support of . Illegal predictions therefore count as incorrect, and every legal optimal move is accepted. The saved implementation averages batch accuracies equally, including the shorter final batch, rather than weighting them by batch size. The reported decimals are those saved batch means, not exact correct-example counts divided by 100,000. The same convention applies to the displayed validation curve.
Generated from paper_jmlr.tex, lines 1098–1100.
2 Explain this
A held-out example counts as correct if the argmax over all action logits is one of the optimal moves. Illegal predictions are wrong; every legal optimal move is accepted.
A detail that matters for the decimals: the saved code averaged per-batch accuracies with equal weight, including the shorter last batch. The reported numbers are those batch means, not exact counts divided by 100,000.
3 How this is formalised
How this is covered. An empirical definition, including the averaging convention of the saved implementation. Not formalised.
| Paper anchor | par-restoration-accuracy-validationtest-p1 (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 7.2.4, “Restoration accuracy (validation/test)” |
| Claim | Restoration accuracy: unmasked argmax in the optimal support; batch-mean convention |
| Coverage category | Empirical result |
| Statement source | paper_jmlr.tex lines 1098–1100; SHA-256 of the normalised block source 85fa97c8ca049d32… |
| Explanations | explain/c-exp-metric, formal/c-exp-metric |
| 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).