Section 7.3, paragraph 3 (observed)Observed single-head accuracy 0.768 and recall 0.536 on the finite test set
Empirical result Supported by saved experimental runs, not by a proof.
1 Paper text
Single-head baseline. The single-head baseline achieves 0.768 overall accuracy and 0.536 N-position recall. These numbers have an exact theoretical explanation. With bits, an N-position has nim-sum . Of these 15 values, exactly 8 are odd (: the values ) and 7 are even (). Head detects an N-position only when , so the theoretical N-position recall is (observed: 0.536 on the finite test set). All P-positions are correctly classified (since implies ), so on a balanced test set the overall accuracy is (observed: 0.768). This calculation describes the particular classifier that declares an N-position exactly when . It is not the winning-move success bound of Theorem 5.12(i), and does not establish a limit on arbitrary classifiers or rollout policies.
Generated from paper_jmlr.tex, lines 1181–1187.
2 Explain this
On the finite test set the single-head baseline scored 0.768 accuracy and 0.536 recall, close to the theoretical 0.767 and 0.533 and consistent with sampling variation on a finite test set. The exact teacher head gives the same 0.768 and 0.536 in Table 2.
3 How this is formalised
How this is covered. Empirical (saved output). The theoretical values are checked in Section 7.3, paragraph 3 (arithmetic).
| Paper anchor | par-results-p3 (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 7.3, paragraph 3 (observed) |
| Claim | Observed single-head accuracy 0.768 and recall 0.536 on the finite test set |
| Coverage category | Empirical result |
| Statement source | paper_jmlr.tex lines 1181–1187; SHA-256 of the normalised block source e23068ca456c51b6… |
| Depends on | Section 7.3, paragraph 3 (arithmetic) |
| Explanations | explain/c-baseline-observed, formal/c-baseline-observed |
| 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).