Section 7.1.3, paragraph 1Soft-target cross-entropy to the uniform distribution over optimal restoration moves
Empirical result Supported by saved experimental runs, not by a proof.
1 Paper text
For each training input (single-frame state or two-frame state-pair), the target is a soft distribution over optimal restoration moves. The policy head is trained with cross-entropy to this target. The soft-target cross-entropy also uses unmasked logits. No value loss is used in this supervised restoration experiment.
Generated from paper_jmlr.tex, lines 1029–1032.
2 Explain this
The target for each input is a probability distribution spread evenly over all optimal restoration moves from the current position, and the network is trained with cross-entropy against that soft target (on unmasked logits). No value loss is used.
3 How this is formalised
How this is covered. Empirical setup; not formalised.
| Paper anchor | sec-training-targets-and-loss-p1 (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 7.1.3, paragraph 1 |
| Claim | Soft-target cross-entropy to the uniform distribution over optimal restoration moves |
| Coverage category | Empirical result |
| Statement source | paper_jmlr.tex lines 1029–1032; SHA-256 of the normalised block source 68aa8bd326b0ab98… |
| Explanations | explain/c-exp-loss, formal/c-exp-loss |
| 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).