Parameterized Hardness of Zonotope Containment and Neural Network Verification
This work addresses fundamental verification problems for neural networks, which is crucial for ensuring reliability in machine learning applications, but it is incremental as it builds on prior complexity results to close specific gaps.
The paper tackles the parameterized computational complexity of verifying properties in ReLU neural networks, proving that deciding positivity and related problems for 2-layer networks are W[1]-hard with respect to input dimension d, and showing NP-hardness and W[1]-hardness for approximating maximum values and Lipschitz constants in 2- and 3-layer networks, implying that naive enumeration methods are essentially optimal under the Exponential Time Hypothesis.
Neural networks with ReLU activations are a widely used model in machine learning. It is thus important to have a profound understanding of the properties of the functions computed by such networks. Recently, there has been increasing interest in the (parameterized) computational complexity of determining these properties. In this work, we close several gaps and resolve an open problem posted by Froese et al. [COLT '25] regarding the parameterized complexity of various problems related to network verification. In particular, we prove that deciding positivity (and thus surjectivity) of a function $f\colon\mathbb{R}^d\to\mathbb{R}$ computed by a 2-layer ReLU network is W[1]-hard when parameterized by $d$. This result also implies that zonotope (non-)containment is W[1]-hard with respect to $d$, a problem that is of independent interest in computational geometry, control theory, and robotics. Moreover, we show that approximating the maximum within any multiplicative factor in 2-layer ReLU networks, computing the $L_p$-Lipschitz constant for $p\in(0,\infty]$ in 2-layer networks, and approximating the $L_p$-Lipschitz constant in 3-layer networks are NP-hard and W[1]-hard with respect to $d$. Notably, our hardness results are the strongest known so far and imply that the naive enumeration-based methods for solving these fundamental problems are all essentially optimal under the Exponential Time Hypothesis.