Papers for
neural network verification teams
Papers whose findings have a practical use for this group, as judged from the abstract. Open a paper to read what it means in practice.
Iterated width 4 neural networks simulate any Turing machine exactly
Iterated Narrow Networks: Turing Completeness at Width 4 on Convex Input Spaces and the Complexity of Verification
Abstract: We study the iterates of a fixed ReLU network $N$ of width 4, that is, the discrete-time system $x_{k+1} = N(x_k)$ on $[0,1]^4$. Equivalently, $x_k$ is the output of a weight-tied network made of $k$ copies of $N$, or of a recurrent network with no external input, started at $x_0$. We prove that every deterministic Turing machine $M$ admits such a network $N_M$. The network can be constructed in polynomial time from $M$. Each iteration has depth $\mathrm{poly}(|M|)$. The iterates of $N_M$ simulate $M$ exactly on every encoded tape. The number of iterations is proportional to the running time of $M$. Moreover, the fourth coordinate irreversibly flags every point of the convex cube $[0,1]^4$ whose simulation reads an invalid digit. This flag is the certificate that makes hardness reductions sound on convex input regions, the regime of practical verifiers. Convex regions were previously inaccessible because of a continuity obstruction inherent to ReLU networks. The correspondence has three consequences. First, reachability for iterated width-4 ReLU networks spans the full complexity hierarchy along the single axis of the time bound: it is NP-complete for a unary bound, NEXP-complete for a binary bound and RE-complete (undecidable) with no bound. Second, two extra neurons of width suffice to extend the hardness to every common smooth activation: at width 6, the robust verification problem (a promise problem with $δ/2δ$ gap) is NP-complete for $\tanh$, sigmoid, GELU, Swish, ELU, and any polynomial-time-computable continuous non-polynomial activation with a polynomial-time-computable Lipschitz constant. Third, the whole spectrum transfers to discretized Neural ODEs in dimension 5.
Verification is hard for narrow deep neural networks with relu activation
Fractal Gadgets for Neural Networks: The Complexity of the Narrow Regime
Abstract: We study the verification problem for deep narrow ReLU neural networks: given a network of bounded width computing a piecewise-affine map on [0,1], does some input satisfy a prescribed output constraint? Classical NP-hardness proofs for ReLU verification use one neuron per Boolean variable and say nothing about networks of small constant width, while width-1 networks are easy to verify. We show that verification of ReLU networks is NP-complete at width 4 for arbitrary inputs in [0,1]. When inputs are restricted to a natural discrete encoding set, NP-completeness already holds at width 3. Together with polynomial-time decidability at width 1, this leaves open only width 2 on the encoding set, and widths 2 and 3 on [0,1]. The technical core is a fractal preprocessing gadget: a width-2 ReLU subnetwork whose iterate vanishes precisely near a finite Cantor-like subset of [0,1] with 2^n points. It reduces verification of a continuous function on [0,1] to verification on 2^n discrete points without increasing the width, and is the missing ingredient for width-bounded hardness reductions. The same construction yields further results at width 3 on the encoding set: the universal problem is coNP-complete, counting zeros is #P-complete, a majority variant is PP-complete, and approximating the minimum output within a constant gap inherited from Max-3Sat is NP-hard. The NP, coNP and inapproximability results lift to all of [0,1] at width 4; lifting counting and majority, and lifting at width 3, remain open.