pith. sign in

arxiv: 2605.29537 · v1 · pith:WB5TMBPSnew · submitted 2026-05-28 · 💻 cs.CC · cs.LG· cs.LO

The Complexity of Verifying Feedforward Neural Networks in Quantised Settings

Eric Alsmann , Martin Lange , Marco S\"alzer This is my paper

Pith reviewed 2026-06-29 00:07 UTC · model grok-4.3

classification 💻 cs.CC cs.LGcs.LO
keywords neural network verificationcomputational complexityquantised neural networksNP-completenessfeedforward networkslinear programmingbit-vector specifications
0
0 comments X

The pith

Verification of feedforward neural networks with fixed quantised weights remains NP-complete for both linear programming and bit-vector specifications.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper maps the computational complexity of verifying feedforward neural networks when moving from exact rational arithmetic to finite-width quantised arithmetic. It proves that fixed quantised networks retain NP-completeness for verification under linear constraints and under bit-level constraints, matching the rational case. For dynamically quantised networks evaluated under bit-vector specifications, it supplies upper bounds that sit alongside a known PSPACE-hardness lower bound. These distinctions matter because they show which aspects of quantisation preserve or alter the inherent difficulty of the verification task.

Core claim

For quantised FNNs with fixed arithmetic precision, verification under both LP and BV specifications remains NP-complete, matching the complexity of the rational case. For dynamically quantised FNNs with BV specifications, upper bounds are established that complement a previously known PSPACE-hardness result.

What carries the argument

The three-class distinction of rational, fixed-quantised, and dynamically-quantised feedforward neural networks, paired with the split between linear programming and bit-vector specifications.

Load-bearing premise

That distinguishing rational, fixed-quantised, and dynamically-quantised networks along with LP and BV specifications is enough to capture all effects of finite arithmetic on verification complexity.

What would settle it

A proof that verification for fixed-quantised FNNs under LP specifications can be done in polynomial time would falsify the NP-completeness claim.

Figures

Figures reproduced from arXiv: 2605.29537 by Eric Alsmann, Marco S\"alzer, Martin Lange.

Figure 1
Figure 1. Figure 1: FNN gadgets, one for each component of a propositional [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The manuscript investigates the computational complexity of verifying feedforward neural networks (FNNs) in quantised arithmetic settings. It introduces three classes of FNNs: rational FNNs with exact rational weights, quantised FNNs with weights from a fixed finite-width arithmetic, and dynamically quantised FNNs where rational networks are evaluated using a given finite-width arithmetic. Two specification types are considered: LP specifications consisting of conjunctions of linear constraints, and BV specifications that allow bit-level reasoning and non-linear constraints. The central claims are that verification for fixed-quantised FNNs is NP-complete under both LP and BV specifications, matching the rational case, and that upper bounds are provided for dynamically quantised FNNs under BV specifications, complementing a known PSPACE-hardness result.

Significance. If the results hold, this work provides a valuable complexity classification for neural network verification problems in settings that model practical finite-precision computations. This is significant because it demonstrates that fixed quantisation preserves the NP-completeness of the rational case for both specification types, while dynamic quantisation leads to higher complexity classes. Such results can guide the development of verification algorithms and highlight the computational implications of arithmetic precision in safety-critical neural network applications. The paper's use of standard complexity theory tools to map these distinctions is a strength.

minor comments (2)
  1. The abstract would be strengthened by including a brief outline of the proof techniques or reduction strategies used to establish the NP-completeness results.
  2. Consider adding a summary table in the introduction or conclusion that lists the complexity results for all combinations of network class and specification type for quick reference.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive and supportive review, including the accurate summary of our results on the complexity of verifying quantised FNNs and the recommendation for minor revision. No specific major comments were provided in the report.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper establishes complexity results (NP-completeness for fixed-quantised FNNs under LP/BV specs, matching the rational case; upper bounds for dynamic-quantised BV) directly from the definitions of the three network classes and two specification types. These distinctions are introduced as a sufficient partition of relevant arithmetic effects, and the claims are presented as standard reductions and membership arguments without any fitted parameters, self-referential constructions, or load-bearing self-citations that collapse the derivation to its inputs. The PSPACE-hardness reference is external and only complemented, not used to force the new upper bounds.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claims rest entirely on standard definitions and results from computational complexity theory; no free parameters, ad-hoc axioms, or invented entities are introduced.

axioms (1)
  • standard math Standard definitions of NP-completeness via polynomial-time reductions and PSPACE-hardness via standard reductions
    The paper invokes these definitions to classify the verification problems for each network and specification class.

pith-pipeline@v0.9.1-grok · 5699 in / 1242 out tokens · 30142 ms · 2026-06-29T00:07:31.166927+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

20 extracted references · 2 canonical work pages

  1. [1]

    Johnson, and Changliu Liu

    [Brixet al., 2023 ] Christopher Brix, Mark Niklas Müller, Stanley Bak, Taylor T. Johnson, and Changliu Liu. First three years of the international verification of neural net- works competition (VNN-COMP).Int. J. Softw. Tools Technol. Transf., 25(3):329–339,

    2023

  2. [2]

    URLhttps://arxiv.org/abs/2412.19985

    [Brixet al., 2024 ] Christopher Brix, Stanley Bak, Taylor T. Johnson, and Haoze Wu. The fifth international verifica- tion of neural networks competition (VNN-COMP 2024): Summary and results.CoRR, abs/2412.19985,

    work page arXiv 2024

  3. [3]

    MIT Press, Cambridge, MA, USA, October

    [Esparza and Blondin, 2023] Javier Esparza and Michael Blondin.Automata Theory: An Algorithmic Approach. MIT Press, Cambridge, MA, USA, October

    2023

  4. [4]

    Succinct representations of graphs.Inf

    [Galperin and Wigderson, 1983] Hana Galperin and Avi Wigderson. Succinct representations of graphs.Inf. Con- trol., 56(3):183–198,

    1983

  5. [5]

    https://doi.org/10.48550/arXiv.2103.13630, http://arxiv.org/abs/2103.13630

    [Gholamiet al., 2021 ] Amir Gholami, Sehoon Kim, Zhen Dong, Zhewei Yao, Michael W. Mahoney, and Kurt Keutzer. A survey of quantization methods for efficient neural network inference.CoRR, abs/2103.13630,

    work page arXiv 2021

  6. [6]

    Henzinger, Mathias Lechner, and Ðor¯de Žikeli ´c

    [Henzingeret al., 2021 ] Thomas A. Henzinger, Mathias Lechner, and Ðor¯de Žikeli ´c. Scalable verification of quan- tized neural networks.Proceedings of the AAAI Confer- ence on Artificial Intelligence, 35(5):3787–3795,

    2021

  7. [7]

    A survey of safety and trustwor- thiness of deep neural networks: Verification, testing, ad- versarial attack and defence, and interpretability.Comput

    [Huanget al., 2020 ] Xiaowei Huang, Daniel Kroening, Wenjie Ruan, James Sharp, Youcheng Sun, Emese Thamo, Min Wu, and Xinping Yi. A survey of safety and trustwor- thiness of deep neural networks: Verification, testing, ad- versarial attack and defence, and interpretability.Comput. Sci. Rev., 37:100270,

    2020

  8. [8]

    [Jia and Rinard, 2021] Kai Jia and Martin C. Rinard. Ex- ploiting verified neural networks via floating point nu- merical error. In Cezara Dragoi, Suvam Mukherjee, and Kedar S. Namjoshi, editors,Static Analysis - 28th Interna- tional Symposium, SAS 2021, Chicago, IL, USA, October 17-19, 2021, Proceedings, volume 12913 ofLecture Notes in Computer Science, ...

    2021

  9. [9]

    Barrett, David L

    [Katzet al., 2017 ] Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural net- works. In Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verification - 29th International Confer- ence, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, vol...

    2017

  10. [10]

    Barrett, David L

    [Katzet al., 2022 ] Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: a calculus for reasoning about deep neural networks.For- mal Methods Syst. Des., 60(1):87–116,

    2022

  11. [11]

    Combinatorial Optimization: Theory and Algorithms

    [Korte and Vygen, 2018] Bernhard Korte and Jens Vygen. Combinatorial Optimization: Theory and Algorithms. Number 21 in Algorithms and Combinatorics. Springer Berlin Heidelberg, Berlin, Heidelberg,

    2018

  12. [12]

    2018 edi- tion,

    6th ed. 2018 edi- tion,

    2018

  13. [13]

    Complexity of fixed-size bit-vector logics.Theory Comput

    [Kovásznaiet al., 2016 ] Gergely Kovásznai, Andreas Fröh- lich, and Armin Biere. Complexity of fixed-size bit-vector logics.Theory Comput. Syst., 59(2):323–376,

    2016

  14. [14]

    Reachability analysis of deep neural net- works with provable guarantees

    [Ruanet al., 2018 ] Wenjie Ruan, Xiaowei Huang, and Marta Kwiatkowska. Reachability analysis of deep neural net- works with provable guarantees. In Jérôme Lang, edi- tor,Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13- 19, 2018, Stockholm, Sweden, pages 2651–2659. ijcai.org,

    2018

  15. [15]

    Reachability is NP-complete even for the simplest neu- ral networks

    [Sälzer and Lange, 2021] Marco Sälzer and Martin Lange. Reachability is NP-complete even for the simplest neu- ral networks. InReachability Problems: 15th Interna- tional Conference, RP 2021, Liverpool, UK, October 25– 27, 2021, Proceedings, pages 149–164, Berlin, Heidel- berg,

    2021

  16. [16]

    [Sälzer and Lange, 2022] Marco Sälzer and Martin Lange

    Springer-Verlag. [Sälzer and Lange, 2022] Marco Sälzer and Martin Lange. Reachability in simple neural networks.Fundam. Infor- maticae, 189(3-4):241–259,

    2022

  17. [17]

    Verifying and interpreting neu- ral networks using finite automata

    [Sälzeret al., 2024 ] Marco Sälzer, Eric Alsmann, Florian Bruse, and Martin Lange. Verifying and interpreting neu- ral networks using finite automata. In Joel D. Day and Florin Manea, editors,Developments in Language Theory, pages 266–281, Cham,

    2024

  18. [18]

    [Vaswaniet al., 2017 ] Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N

    Springer Nature Switzer- land. [Vaswaniet al., 2017 ] Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V . N. Vish- wanathan, and Roman Garnett, editors,Advances in Neu...

    2017

  19. [19]

    On the construction of automata from linear arithmetic constraints

    [Wolper and Boigelot, 2000] Pierre Wolper and Bernard Boigelot. On the construction of automata from linear arithmetic constraints. In Susanne Graf and Michael I. Schwartzbach, editors,Tools and Algorithms for Con- struction and Analysis of Systems, 6th International Con- ference, TACAS 2000, Held as Part of the European Joint Conferences on the Theory an...

    2000

  20. [20]

    Complexity of reachability problems in neural networks

    [Wurm, 2023] Adrian Wurm. Complexity of reachability problems in neural networks. In Olivier Bournez, Enrico Formenti, and Igor Potapov, editors,Reachability Prob- lems - 17th International Conference, RP 2023, Nice, France, October 11-13, 2023, Proceedings, volume 14235 ofLecture Notes in Computer Science, pages 15–27. Springer,

    2023