NIM paper · interactive edition Interactive edition · paper, explanations and Lean proofs.

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 k=4k=4 bits, an N-position has nim-sum σ∈{1,…,15}\sigma \in \{1,\dots,15\}. Of these 15 values, exactly 8 are odd (σ0=1\sigma_0 = 1: the values 1,3,5,7,9,11,13,151,3,5,7,9,11,13,15) and 7 are even (σ0=0\sigma_0 = 0). Head π0\pi_0 detects an N-position only when σ0=1\sigma_0 = 1, so the theoretical N-position recall is 8/15≈0.5338/15 \approx 0.533 (observed: 0.536 on the finite test set). All P-positions are correctly classified (since σ=0\sigma = 0 implies σ0=0\sigma_0 = 0), so on a balanced test set the overall accuracy is 12⋅1+12⋅815=2330≈0.767\tfrac{1}{2}\cdot 1 + \tfrac{1}{2}\cdot\tfrac{8}{15} = \tfrac{23}{30} \approx 0.767 (observed: 0.768). This calculation describes the particular classifier that declares an N-position exactly when r0=1r_0=1. 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).

Coverage record
Paper anchorpar-results-p3 (website anchor; the manuscript has no label here)
Displayed asSection 7.3, paragraph 3 (observed)
ClaimObserved single-head accuracy 0.768 and recall 0.536 on the finite test set
Coverage categoryEmpirical result
Statement sourcepaper_jmlr.tex lines 1181–1187; SHA-256 of the normalised block source e23068ca456c51b6…
Depends onSection 7.3, paragraph 3 (arithmetic)
Explanationsexplain/c-baseline-observed, formal/c-baseline-observed
Build evidencefresh 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).