Section 7.2.2, paragraph 1Teacher–random–teacher dataset of 10⁶ examples with soft optimal-move labels

Empirical result Supported by saved experimental runs, not by a proof.

1 Paper text

We generate a dataset of size $D=10^6$ examples of the form $(p, p') \mapsto \pi_{\mathrm{opt}}(\cdot \mid p') ,$ where $\pi_{\mathrm{opt}}(\cdot \mid p')$ is a soft target distribution over optimal moves from $p'$ .

Generated from paper_jmlr.tex, lines 1062–1067.

2 Explain this

Each training example is built in three steps: take a random winning position and apply an optimal move (so the result $p$ has nim-sum zero); apply one uniformly random legal move to get $p'$ ; label $p'$ with the uniform distribution over all optimal moves. This reproduces exactly the restoration situation: the opponent departs from a $P$ -position and the agent must restore it. There are $10^6$ examples, split 80/10/10 with seed 0.

The paper notes two ways in which this helps the learner compared with earlier studies: binary heap encoding, and perfectly labelled restoration targets instead of sparse win/loss outcomes. It also notes that the teacher's first-winning-heap rule makes the distribution of predecessors nonuniform.

3 How this is formalised

How this is covered. Empirical setup, described from the saved run. The fact that $p$ has nim-sum zero and that every label move restores zero follows from Section 7.2, paragraph 1. The dataset itself is not part of this edition.

Coverage record
Paper anchor	`sec-dataset-generation-teacher-random-teacher-p1` (website anchor; the manuscript has no label here)
Displayed as	Section 7.2.2, paragraph 1
Claim	Teacher–random–teacher dataset of 10⁶ examples with soft optimal-move labels
Coverage category	Empirical result
Statement source	paper_jmlr.tex lines 1062–1067; SHA-256 of the normalised block source `f46d017456d5a006…`
Explanations	`explain/c-exp-data`, `formal/c-exp-data`
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).