AbstractSummary of the results; each is stated and qualified in the body of the paper
Informal interpretation Motivation, interpretation or scope; not a formal claim.
1 Paper text
Abstract
Why can neural networks struggle to learn optimal play in a game with a simple, efficient solution algorithm? Motivated by empirical difficulties with parity in impartial games, we use NIM to study a representational bottleneck and three ways around it. We show that a restricted model of shallow, fixed-scale quantised networks lies in , a circuit class unable to compute parity on arbitrarily large inputs. This prevents optimal single-position play across all board sizes within the model. The obstruction also guides architectural design: two-frame inputs allow restoration from a known zero-nim-sum position; complementary rollout policies reveal the missing invariant; and persistent recurrence accumulates it row by row. Each route retains shallow network components while supplying additional information or processing time. Supervised experiments illustrate the benefits of two-frame restoration and multiple rollout heads; recurrence is a theoretical construction. These results establish representational possibilities, not guarantees of successful training: does not characterise practical learnability. Core mathematical results and constructions have been checked in Lean, with classical complexity results as explicit external inputs. The interactive edition and complete Lean sources are available online (Riis, 2026a,b).
Generated from paper_jmlr.tex, lines 64–68.
2 Explain this
The abstract compresses the whole paper into a few sentences. Each sentence corresponds to a precise statement inside the paper, and several of them carry conditions that the abstract can only hint at:
- "lies in AC0" is Theorem 2.4, for an explicitly restricted model of fixed-scale threshold networks, not for neural networks in general;
- "prevents optimal single-position play" is Theorem 5.2, which uses the classical fact that parity is not in AC0;
- the three routes around the obstruction are Proposition 5.5 (two frames, given a zero-nim-sum predecessor), Proposition 5.9 (several rollout policies, executed in sequence) and Proposition 5.13 (a recurrent scan whose length grows with the board, with retained state, a reset, and a replay of the board or board storage to choose a move);
- the experiments are single saved supervised and imitation runs (Section 7.2, Section 7.3).
The learnability qualification says what is not claimed: the constructions are representational possibilities, not guarantees that training will find them, and AC0 membership is not a test of learnability.
3 How this is formalised
The abstract itself is not formalised; it summarises. Its mathematical sentences are covered by the records of
the statements listed above, each with its own category. Its verification statement, that core results were checked in
Lean with classical complexity results as explicit external inputs, is reflected on the
coverage page: conditional results name their classical input, HastadNegl, and empirical
results are marked as such.
The abstract cites the interactive edition and the complete Lean source repository. Their full addresses appear as plain text in the references, in both the PDF and the interactive article. Section 10 cites the same resources.
| Paper anchor | abstract (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Abstract |
| Claim | Summary of the results; each is stated and qualified in the body of the paper |
| Coverage category | Informal interpretation |
| Statement source | paper_jmlr.tex lines 64–68; SHA-256 of the normalised block source fc9bca0c3cea0bc0… |
| Depends on | Theorem 2.4, Theorem 5.2 (barrier), Proposition 5.5, Proposition 5.9, Proposition 5.13, Proposition 5.14, Section 7.2.5, “One-frame does not learn restoration; two-frame eventually does”, Section 7.3, paragraph 2 |
| Explanations | explain/c-abstract, formal/c-abstract |
| Build evidence | fresh isolated rebuild, audit report |
4 Lean statement and source
No Lean statement corresponds to this claim. This is interpretation or motivation, not a formal mathematical claim.
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).