Reachability In Simple Neural Networks

TL;DR

The paper analyzes the reachability problem Reach for neural networks with piecewise-linear activations, aiming to certify inputs that yield valid outputs under linear specifications. It corrects flaws in prior NP-completeness proofs and shows $ ext{Reach} \,\in\, \text{NP}$ by encoding NN behavior as a PWL-linear program, leveraging polynomial-bounded witnesses. It also proves $ ext{NP}$-hardness via a 3-SAT reduction using gadget-based network constructions, and strengthens the result by showing hardness persists for very restricted networks (e.g., a single hidden layer, output dimension one, or networks with few weight values). The findings suggest reachability verification remains computationally intractable even for compact or structurally simple NN, motivating further study of restricted classes and richer specification languages, including extensions to CNNs and GNNs, as well as questions about quantifiers and problem variants.

Abstract

We investigate the complexity of the reachability problem for (deep) neural networks: does it compute valid output given some valid input? It was recently claimed that the problem is NP-complete for general neural networks and specifications over the input/output dimension given by conjunctions of linear inequalities. We recapitulate the proof and repair some flaws in the original upper and lower bound proofs. Motivated by the general result, we show that NP-hardness already holds for restricted classes of simple specifications and neural networks. Allowing for a single hidden layer and an output dimension of one as well as neural networks with just one negative, zero and one positive weight or bias is sufficient to ensure NP-hardness. Additionally, we give a thorough discussion and outlook of possible extensions for this direction of research on neural network verification.

Figures (4)

• Figure 1: Schema of a neural network with five layers, input dimension of two and output dimension of one. Filled nodes are ReLU nodes, empty nodes are identity nodes. An edge between two nodes $u$ and $v$ with label $w$ denotes that the output of $u$ is weighted with $w$ in the computation of $v$. No edge between $u$ and $v$ implies $w=0$. The bias of a node is depicted by a value above or below the node. If there is no such value then the bias is zero.
• Figure 2: Gadgets used in the reduction from 3sat to Reach. A non-weighted outgoing edge of a gadget is connected to a weighted incoming edge of another gadget in the actual construction or is considered an output of the overall neural network.
• Figure 3: NN resulting from the reduction of the 3sat-formula $(X_0\lor X_1 \lor X_2) \land (\neg X_0 \lor X_1 \lor \neg X_2) \land (\neg X_1 \lor X_2 \lor X_3)$ under the assumption that NN are defined over $\{0,1\}$ only.
• Figure 4: Gadgets used to show that Reach is NP-hard if restricted to NN from $\mathop{\mathit{NN}}\left(\{-c,0,d\}\right)$. A non-weighted outgoing edge of a gadget is connected to a weighted incoming one of another gadget in the actual construction or are considered as outputs of the overall neural networks.

Theorems & Definitions (19)

• Definition 3.1
• Lemma 3.2
• Theorem 3.3
• Corollary 3.4
• Corollary 3.5
• Definition 3.6
• Lemma 3.7
• Lemma 3.8
• Theorem 3.9
• Lemma 3.10