Homecs.CCarXiv:2605.29537

The Complexity of Verifying Feedforward Neural Networks in Quantised Settings

cs.CCMachine Learningcs.LO2026-05v1license

Abstract

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.

Cite

@article{arxiv.2605.29537,
  title  = {The Complexity of Verifying Feedforward Neural Networks in Quantised Settings},
  author = {Eric Alsmann and Martin Lange and Marco Sälzer},
  journal= {arXiv preprint arXiv:2605.29537},
  year   = {2026}
}