The Complexity of Verifying Feedforward Neural Networks in Quantised Settings
This work provides a complexity landscape for neural network verification in quantised settings, which is important for practitioners dealing with resource-constrained hardware.
The paper characterizes the computational complexity of verifying feedforward neural networks in quantised settings, showing that verification under LP and BV specifications remains NP-complete for quantised FNNs with fixed arithmetic precision, and establishes upper bounds for dynamically quantised FNNs with BV specifications.
We investigate the computational complexity of neural network verification in quantised settings. We distinguish three classes of Feedforward Neural Networks (FNNs): rational FNNs with exact rational weights, quantised FNNs whose weights come from a finite-width arithmetic, and dynamically quantised FNNs in which rational networks are evaluated with respect to a given finite-width arithmetic. We consider two types of specifications used in the literature. Linear programming (LP) specifications are conjunctions of linear constraints, while bit-vector (BV) specifications allow reasoning at the bit level and can express non-linear constraints. Our results give a complexity landscape of these verification problems. For quantised FNNs with fixed arithmetic precision, we show that verification under both LP and BV specifications remains NP-complete, matching the complexity of the rational case. For dynamically quantised FNNs with BV specifications, we establish upper bounds, complementing a previously known PSPACE-hardness result.