Security Properties of Neural Networks as Decision Problems

Adrian Wurm

cs.LOSep 30, 2026

Security Properties of Neural Networks as Decision Problems

Authors: Adrian Wurm

Organizations: BTU Cottbus–Senftenberg, Lehrstuhl Theoretische Informatik Platz der Deutschen Einheit 1, 03046 Cottbus, Germany

Abstract

Certifying a deployed neural network raises decision problems that the verification literature has not classified: whether the model carries a backdoor planted in its training data, whether a fault in its stored parameters can drive it into an unsafe state, whether its output leaks a private part of its input. We formalise eight such problems and classify what we can. The organising observation is a logical one. The function computed by a piecewise linear network, together with all its node values, is definable by a quantifier-free formula of real addition of size linear in the network, so a property of the network is a quantifier-alternation sentence, which Sontag's 1985 theorem places in the polynomial hierarchy at the level of its prefix. Membership results are thus corollaries, and the argument makes plain what they need: that the quantified objects are inputs rather than the network's own parameters. Non-interference, monotonicity and counterfactual fairness have exactly the complexity of network equivalence and of interval verification, all co-NP- complete over ReLU. Detection of backdoor triggers from a quantised alphabet is Sigma_2^P-complete, one level above robustness certification, so it does not reduce to polynomially many robustness queries unless the hierarchy collapses. Inversion resistance is co-NP-complete for every l_p metric, p a fixed positive integer. Quantifying over parameters instead of inputs - the fault model of bit-flip attacks, radiation upsets and analog accelerators - makes verification exists-R-complete already for networks of identity nodes, for which every previously studied problem is in P, and it stays so when each parameter is confined to a box of inverse-polynomial width; the corresponding safety question is forall-R-complete for ReLU.

Figures & tables

problem	prefix	parameter	status
NNReach	$\exists x$	-	NP-complete [ 27 ]
VIP , NE	$\forall x$	-	co-NP-complete [ 42 ]
NonInt	$\forall x$	-	co-NP-complete (Prop. 4.2 )
Mono , CFair	$\forall x$	-	co-NP-complete (Prop. 4.6 , [ 44 ] )
InvRes	$\forall x\forall x^{\prime}$	-	co-NP-complete (Thm. 7.2 )
Min	$\exists N^{\prime}\forall x$	structure	in $\Pi_{2}^{\mathrm{P}}$ [ 42 ]

Table 1: The problems of this paper in the schema of Section 3 . All completeness entries are for

\mathrm{ReLU}

unless stated otherwise. Rows above the Min line are first-level; rows with a parameter-space parameter leave the polynomial hierarchy.

Explore similar work

May 28, 2026cs.CC

The Complexity of Verifying Feedforward Neural Networks in Quantised Settings

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, Marco Sälzer

University of Kassel · RPTU University Kaiserslautern-Landau

Neural Network Verification Quantum Neural Networks Formal Verification Feed-Forward

Ask PDF

Sep 26, 2025cs.CC

Parameterized Hardness of Zonotope Containment and Neural Network Verification

Neural networks with ReLU activations are a widely used model in machine learning. It is thus important to have a profound understanding of the properties of the functions computed by such networks. Recently, there has been increasing interest in the (parameterized) computational complexity of determining these properties. In this work, we close several gaps and resolve an open problem posed by Froese et al. [COLT '25] regarding the parameterized complexity of various problems related to network verification. In particular, we prove that, for all

\ell\ge 2

, deciding positivity (and thus surjectivity) of a function

f:\mathbb{R}^d\to\mathbb{R}

computed by an

\ell

-layer ReLU network is W[

\ell-1

]-hard when parameterized by the input dimension

d

. The case

\ell=2

implies that zonotope non-containment (a problem that is of independent interest in computational geometry, control theory, and robotics) is W[1]-hard with respect to the ambient dimension

d

. Moreover, we show that approximating the maximum within any multiplicative factor and computing the

L_p

-Lipschitz constant for

p\in(0,\infty]

\ell

-layer networks is NP-hard and W[

\ell-1

]-hard with respect to

d

. For

\ell\ge 3

, approximating the

L_p

-Lipschitz constant is NP- and W[

\ell-2

]-hard. We further show that the above problems are NP- and W[

t

]-hard (for all

t\ge 1

) with respect to

\ell

for constant

d

. Notably, our hardness results imply that the naive enumeration-based methods for these fundamental problems running in

n^{(\ell-1) d}\cdot\operatorname{poly}(N)

time are all essentially optimal under the Exponential Time Hypothesis.

Vincent Froese, Moritz Grillo, Christoph Hertrich +1

Technische Universität Berlin · Max Planck Institute for Mathematics in the Sciences · University of Technology Nuremberg

Rectified Linear Unit Networks Neural Network Verification Np-Hard Polytopes Lipschitz Continuity

Ask PDF

Jul 15, 2026cs.CC

Random Parameter Noise Does Not Make Exact ReLU Verification Easy

We study exact verification of ReLU networks in an adversarial smoothed model. Every network weight and bias is independently perturbed by Gaussian noise, clipped to

[-2,2]

, and rounded to the exact dyadic grid determined by the input bit complexity. We show that, under the standard assumption

\mathrm{NP}\not\subseteq\mathrm{BPP}

, there is no sound and complete verifier whose expected running time is polynomial in network size, bit complexity, and inverse noise level for every base instance. The conclusion already holds at the fixed noise level

σ_\star=2^{-11}

for one-hidden-layer networks over a unit box, with hidden fan-in at most three and base coefficients in

[-1,1]

. The proof combines an exact gap embedding with a quantitative robustness argument. For every E3SAT formula

Φ

with

m

clauses, a four-ReLU-per-clause construction satisfies

\max_{x\in[0,1]^n} g_Φ(x)=(m-\operatorname{unsat}(Φ))/3

, and coordinatewise threshold rounding never decreases the objective. A weighted parameter-sensitivity inequality and Gaussian concentration then show that a verification gap linear in

m

survives the aggregate perturbation of all coefficients with probability at least

1-e^{-m/8}

. The proof includes clipping, exact dyadic rounding, output-layer perturbations, polynomial-bit sampling of the rounded Gaussian law, and the conversion from expected smoothed running time to a BPP algorithm. Computational checks test the exact identity and illustrate the different scaling of extensive and constant gaps; they are diagnostics rather than evidence for the complexity theorem. The result concerns worst-case base networks in the stated absolute-noise model, but it shows that parameter nondegeneracy alone does not yield a universal smoothed-polynomial guarantee for exact verification.

Mojtaba Soltanalian

Department of Electrical and Computer Engineering University of Illinois Chicago

Neural Network Verification Rectified Linear Unit Networks Rectified Linear Unit Np-Hard Self-Verification Convex Relaxation+1

Ask PDF