Proceedings

The Complexity of Verifying Feedforward Neural Networks in Quantised Settings

Eric Alsmann, Martin Lange, Marco Sälzer

Download BibTeX Cite

Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence. Main Track. Pages 4135-4142.

https://doi.org/10.24963/ijcai.2026/460

Keywords

  • Machine Learning: Trustworthy machine learning
  • Machine Learning: Robustness
  • Machine Learning: Explainable/Interpretable machine learning

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.

Eric Alsmann, Martin Lange, and Marco Sälzer. 2026. The Complexity of Verifying Feedforward Neural Networks in Quantised Settings. In Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-26. IJCAI, 4135–4142. https://doi.org/10.24963/ijcai.2026/460
Welcome Future Conferences AI Journal Division IJCAI Proceedings About IJCAI IJCAI Awards