Section 7.1.1, paragraph 1Experimental state and action representation (binary heaps, set-heap actions, unmasked restoration argmax)
Empirical result Supported by saved experimental runs, not by a proof.
1 Paper text
We use a fixed-width binary encoding of heap sizes with bits per heap. The single-frame input is the encoding of the current heap vector. The two-frame input concatenates the encodings of the previous and current heap vectors. When a previous frame is unavailable (e.g. on the first move of a game), we set the previous frame equal to the current position so that the input dimension is constant and the 2F policy remains well-defined.
Generated from paper_jmlr.tex, lines 1003–1005.
2 Explain this
Setup facts for both experiments: heaps are written in binary with bits; the one-frame (1F) input is the current board, the two-frame (2F) input concatenates previous and current boards (on a first move the previous frame is set equal to the current one). Actions are "set heap to value ", giving logits.
Two evaluation conventions are distinguished: restoration accuracy takes an unmasked argmax over all logits (an illegal prediction counts as wrong), while game play and the rollout routines mask illegal moves.
3 How this is formalised
How this is covered. A description of the saved experimental implementation, taken from the paper; the edition reproduces it unchanged and does not re-run anything. It is not formalised. The formal model of Section 2 (fixed-scale literal-threshold gates) is different from these floating-point networks.
| Paper anchor | sec:state-action-repr-p1 (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 7.1.1, paragraph 1 |
| Claim | Experimental state and action representation (binary heaps, set-heap actions, unmasked restoration argmax) |
| Coverage category | Empirical result |
| Statement source | paper_jmlr.tex lines 1003–1005; SHA-256 of the normalised block source ac95f39a8f37d56c… |
| Explanations | explain/c-exp-repr, formal/c-exp-repr |
| 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).