---
title: "The Complexity of Verifying Feedforward Neural Networks in Quantised Settings"
authors:
  - "Eric Alsmann"
  - "Martin Lange"
  - "Marco Sälzer"
doi: "10.24963/ijcai.2026/460"
url: "https://ijcai.org/proceedings/2026/460"
pdf: "https://ijcai.org/proceedings/2026/0460.pdf"
venue: "Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence"
year: 2026
pages: "4135-4142"
track: "Main Track"
keywords:
  - "Machine Learning: Trustworthy machine learning"
  - "Machine Learning: Robustness"
  - "Machine Learning: Explainable/Interpretable machine learning"
---

# The Complexity of Verifying Feedforward Neural Networks in Quantised Settings

Eric Alsmann, Martin Lange, Marco Sälzer

*Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence*, pages 4135-4142. DOI: [10.24963/ijcai.2026/460](https://doi.org/10.24963/ijcai.2026/460)

## 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.