Complexity of Injectivity and Verification of ReLU Neural Networks

TL;DR

This paper investigates the computational complexity of injectivity and verification problems in ReLU neural networks, establishing coNP-completeness results and exploring tractability in specific cases, with implications for safety-critical applications.

Contribution

It proves the coNP-completeness of injectivity decision and network verification problems, and introduces fixed-parameter algorithms for small input dimensions, advancing understanding of neural network interpretability and verification.

Findings

Injectivity decision is coNP-complete.

Network verification is coNP-hard for general input domains.

Surjectivity relates to zonotope containment and is characterized for 1D outputs.

Abstract

Neural networks with ReLU activation play a key role in modern machine learning. Understanding the functions represented by ReLU networks is a major topic in current research as this enables a better interpretability of learning processes. Injectivity of a function computed by a ReLU network, that is, the question if different inputs to the network always lead to different outputs, plays a crucial role whenever invertibility of the function is required, such as, e.g., for inverse problems or generative models. The exact computational complexity of deciding injectivity was recently posed as an open problem (Puthawala et al. [JMLR 2022]). We answer this question by proving coNP-completeness. On the positive side, we show that the problem for a single ReLU-layer is still tractable for small input dimension; more precisely, we present a parameterized algorithm which yields fixed-parameter tractability with respect to the input dimension. In addition, we study the network verification problem which is to verify that certain inputs only yield specific outputs. This is of great importance since neural networks are increasingly used in safety-critical systems. We prove that network verification is coNP-hard for a general class of input domains. Our results also exclude constant-factor polynomial-time approximations for the maximum of a function computed by a ReLU network. In this context, we also characterize surjectivity of functions computed by ReLU networks with one-dimensional output which turns out to be the complement of a basic network verification task. We reveal interesting connections to computational convexity by formulating the surjectivity problem as a zonotope containment problem