Section 1, paragraph 5AC0 circuits cannot compute global parity; the connection is made for an explicitly restricted model
External cited result A published result used as background or input; not proved in Lean here.
1 Paper text
Here we turn that difficulty into a question about computation. The class consists of polynomial-size Boolean circuits built from AND, OR and NOT gates, with a number of layers that remains fixed as the input grows. Such circuits can combine many local tests, but cannot compute global parity: whether the total number of input 1s is odd or even. This is the feature that makes the class useful here: it provides a precise model with a provable version of the parity limitation seen in the experiments. We establish the connection for an explicitly restricted neural model, rather than assuming that all neural networks lie in .
Generated from paper_jmlr.tex, lines 91–91.
2 Explain this
What AC0 is. AC0 is the class of Boolean functions computed by circuits of AND, OR and NOT gates (with any number of inputs per gate) whose size grows at most polynomially and whose number of layers stays fixed as the input grows.
What it cannot do. Such circuits can combine many local tests, but they cannot compute the parity of all their input bits once the input is large: this is a classical theorem of circuit complexity.
Why it is used. The earlier experiments pointed to parity as the difficulty; AC0 gives a precise model in which a version of that limitation is provable. Whether it explains the training failures is a separate question.
Caveat. The paper does not assume that neural networks are AC0 circuits. It proves AC0 membership only for a restricted model of fixed-scale threshold networks (Theorem 2.4). The class is AC0, not ACC0: ACC0 allows counting-modulo gates, which can compute parity directly.
3 How this is formalised
The definition of AC0 is standard. The parity lower bound is a classical external result (Furst, Saxe and
Sipser; Håstad). In the Lean development it enters as the named hypothesis HastadNegl, from which the
worst-case statement ParityNotAC0 is derived (ClassicalBoundary.parityNotAC0_of_hastad); see
Remark 2.3 (global parity). The restricted neural model and its simulation are
Theorem 2.4.
| Paper anchor | c-intro-ac0 (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 1, paragraph 5 |
| Claim | AC0 circuits cannot compute global parity; the connection is made for an explicitly restricted model |
| Coverage category | External cited result |
| Statement source | paper_jmlr.tex lines 91–91; SHA-256 of the normalised block source c91a30a19032e1c3… |
| Depends on | Theorem 2.4, Remark 2.3 (global parity) |
| Explanations | explain/c-intro-ac0, formal/c-intro-ac0 |
| Build evidence | fresh isolated rebuild, audit report |
4 Lean statement and source
No Lean statement corresponds to this claim. This is a published classical result. It is cited, not proved in this Lean development.
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).