We present an Ising-compatible framework for formal neural-network robustness verification under bounded input perturbations. For piecewise activations (both continuous piecewise-linear and discrete piecewise-constant), the Exact Logarithmic Piecewise Model (Log-PW) provides an exact, sound, and complete formulation with a state-optimal logarithmic encoding, reducing the binary variables per neuron from linear O(κ) to information-theoretically minimal logarithmic complexity O(⌈log2κ⌉) via logarithmic SOS2 (Log-PWL) and SOS1 (Log-PWC) constraints. For general element-wise activations, the Asymptotic Step-Envelope Model (Step-Env) leverages Log-PWC to construct sound, refinable endpoint enclosures. An exact monotonic reduction based on Jordan decomposition further extends this framework to arbitrary non-monotonic activations. We further develop a hybrid Benders solver with output-sensitive iteration bounds, leveraging a Helly-based conflict compression theory to avoid generic exponential cut explosion. In particular, for shallow networks with fixed input dimension, this establishes an unconditionally polynomial Benders iteration complexity in network size. Interval pruning, certificate transfer for pruned networks, and layerwise classical--Ising partitioning further reduce spin requirements. Experiments demonstrate exact certification fidelity for piecewise-linear networks and near-reference accuracy for non-linear activations under compact spin budgets. On MNIST benchmarks, Log-PW halves binary decision spins over One-Hot formulations, while Helly-based cuts achieve up to a 13.41× speedup and an 87.6% reduction in master queries over standard baselines.
Figures & tables
Figure 1: Illustration of adversarial vulnerability in traffic sign recognition. Small, imperceptible perturbations can cause a neural network to misclassify a stop sign, highlighting the need for robust verification.
Figure 2: Overview of the proposed Ising-compatible robustness verification framework. The end-to-end pipeline links network specification, logarithmic encoding, Step-Envelope construction, and hybrid Benders optimization for Ising solvers.
Model Formulation
Activation Functions
Sound
Guarantee
Exact Log-PW (Log-PWL / Log-PWC)
Piecewise (PWL / PWC)
✓
Exact and complete
Step-Envelope (Step-Env via Log-PWC)
General locally Lipschitz
✓
Complete for strict margins as Δ→0
Table 1: Summary of the proposed verification models in this paper
Figure 3: Step-envelope enclosure of a general activation. Lower and upper step functions approximates the activation with discrete segment-selection states. Refining the partition reduces the activation-envelope error at the cost of Ising-spin budget.
Model Formulation
Constraints
Binary Vars
Continuous Vars
Non-Zeros (NZs)
One-Hot
Log
One-Hot
Log
One-Hot
Log
One-Hot
Log
Exact MILP
1,364
596
192
96
1,188
1,284
55,550
53,822
Table 2: MILP formulation parameters for 784-64-32-10 ReLU network verification.
Model Formulation
Constraints
Binary Vars
Continuous Vars
Non-Zeros (NZs)
One-Hot
Log
One-Hot
Log
One-Hot
Log
One-Hot
Log
Step-Env ( κ=2 )
250
346
96
48
112
208
930
1,122
Step-Env ( κ=4 )
250
442
192
96
112
304
1,314
1,890
Step-Env ( κ=8 )
250
538
384
144
112
496
2,082
3,522
Step-Env ( κ=16 )
250
634
768
192
112
880
3,618
7,074
Step-Env ( κ=32 )
250
730
1,536
240
112
1,648
6,690
14,850
Table 3: Step-Env formulation parameters for 784-64-32-10 sigmoid network verification.
Figure 4: Asymptotic completeness of the Step-Env model on the 784-64-32-10 sigmoid MNIST classifier across perturbation radii ε from 0.02 to 0.18, step size 0.02. As segment count κ increases from 2 to 64 (decreasing maximal width Δ ), certification success rates uniformly converge toward 100% across all radii.
Figure 5: Certified accuracy of the hybrid Benders verifier on make_moons ( Pedregosa et al., 2011 ) . Benders coincides with exact MIP across all budgets for ReLU and Hardtanh, and differs by at most 1% for Sigmoid.
Perturbation
Verification Outcome
Mean CIM Master Calls / Sample ↓
Mean Solve Time / Sample (s) ↓
Efficiency Gains vs. Farkas ↑
Budget ϵ
Robust (%)
Inconclusive (%)
Farkas (B1)
Helly (B3)
Hybrid (B4)
Farkas (B1)
Helly (B3)
Hybrid (B4)
Query Reduction
Time Speedup
0.02
93.0
0.00
53
3
3
0.198
0.012
0.013
94.3%
16.50×
0.04
78.0
0.00
214
23
22
1.082
0.084
0.090
89.7%
12.88×
0.06
55.0
0.00
483
55
52
2.421
0.217
0.335
89.2%
11.16×
0.08
31.0
0.00
809
100
94
5.434
0.451
0.938
88.4%
12.05×
0.10
14.0
0.00
1,195
169
157
11.124
0.891
1.430
86.9%
12.48×
Table 4: Complete performance comparison of Benders decomposition cut strategies on the 4-8-8-8-1 Banknotes network (100 test samples). Certified robustness decisions are 100% identical across all methods with 0.00% inconclusive rates, confirming exactness preservation. Contextual Helly cuts achieve the fastest wall-clock execution ( 13.41× overall acceleration), while Hybrid cuts achieve the most aggressive master query compression (87.6% total reduction).
Figure 6: Empirical evaluation of Benders cut mechanisms on the 4-8-8-8-1 Banknotes network (24 ReLU neurons, 24 binary spins) across 100 test samples. (a) Average CIM master queries per sample versus perturbation budget ϵ (log scale). Standard Farkas cuts suffer severe combinatorial explosion up to 1,578 calls at ϵ=0.120 , whereas Contextual Helly and Hybrid cuts enforce compact polynomial scaling (up to 87.6% reduction). (b) Single-sample wall-clock solving time (seconds) across ϵ . Helly cuts eliminate master query bottlenecks with minimal subproblem extraction overhead, achieving the fastest wall-clock performance across all budgets ( 1.39 s vs 20.56 s at ϵ=0.120 ).
Figure 7: Monolithic QUBO verification fidelity across activation functions. For ReLU, both QUBO solvers identically match the exact MIP reference at all budgets. For Sigmoid, Step-Env tracks MIP almost exactly (with only a 1-sample deviation at ϵ=0.8 ).
Appendix figures & tables6 assets
Supplementary material from the paper’s appendix.
Appendix
Model Formulation
Binary Variables / Neuron
Constraints / Neuron
Aux. Vars ui Needed?
Big-M Bounds Needed?
Coupling Constraints
LP Relaxation Tightness
Standard One-Hot (Big-M)
κ (Linear)
O(κ) ( 4κ+3 )
Yes ( κ continuous)
Yes ( [Lj,Uj] )
Bilinear Big-M
Weak (bounds dependent)
Multiple-Choice (MC)
κ (Linear)
O(κ) ( 3κ+3 )
No
No
Local Linear Disjunctive
Tight (Convex Hull)
Special Ordered Set (SOS2)
κ (Linear)
O(κ) ( κ+4 )
No
No
Linear Grid Weight Coupling
Tight (Convex Hull)
Exact Log-PW (Log-PWL)
⌈log2κ⌉ ( Logarithmic )
O(logκ) ( 2⌈log2κ⌉ )
No
No
Linear Vielma–Nemhauser
Tight (Convex Hull)
Appendix
Table 5: Comparison of MILP formulations for piecewise-linear verification with κ segments per neuron. Log-PW generalizes this logarithmic compactness to both PWL (SOS2) and PWC (SOS1) activations.
Method
Activation
Sound
Complete
Optimization-Based Verifiers
BaB [ Bunel et al., 2018 ]
ReLU
✓
✓
ConvDual [ Wong and Kolter, 2018 ]
ReLU
✓
×
Duality [ Dvijotham et al., 2018 ]
monotonic
✓
×
NSVerify [ Lomuscio and Maganti, 2017 ]
ReLU
✓
✓
Reluplex [ Katz et al., 2017 ]
ReLU
✓
✓
Appendix
Table 6: Comparison of Verification Methods
Figure 8: Empirical experimental results on the Iris binary classification benchmark using a ReLU network under ℓ∞ perturbation ( ε=0.5 ). Panels (a, c): original clean data in sepal space (length vs. width) and petal space (length vs. width), with the 6 samples susceptible to adversarial attack highlighted by bold black circles. Panels (b, d): the same data after ε=0.5 perturbation. Six samples flip their classification predictions and are marked as squares with opposite-class borders (blue with orange border for true label −1 and predicted +1 ; orange with blue border for true label +1 and predicted −1 ). The ReLU network achieves 100% accuracy on clean data and 94% under perturbation.
Perturbation Budget ϵ
0.1
0.2
0.3
0.4
0.5
0.6
Vulnerable Samples ↑
AI2 [ Gehr et al., 2018 ]
0
0
0
3
6
12
DLV [ Huang et al., 2017 ]
0
0
0
2
6
12
ExactReach [ Xiang et al., 2017 ]
0
0
0
2
6
12
MaxSens [ Xiang et al., 2018 ]
0
0
0
3
6
12
Neurify [ Wang et al., 2018a ]
0
0
0
2
6
12
BaB [ Bunel et al., 2018 ]
0
0
0
2
6
12
Appendix
Table 7: Complete Numerical Verification Results for the ReLU Network
Perturbation Budget ϵ
0.1
0.2
0.3
0.4
0.5
0.6
0.7
0.8
0.9
1.0
Vulnerable Samples ↑
Duality [ Dvijotham et al., 2018 ]
0
0
0
2
5
10
26
53
67
79
MaxSens [ Xiang et al., 2018 ]
0
0
0
2
5
10
26
53
67
79
MIP-Gurobi
0
0
0
2
5
10
26
53
67
79
QUBO-Gurobi
0
0
0
2
5
10
26
53
67
79
QUBO-CIM
0
0
0
2
5
10
26
52
67
79
Time (ms) ↓
MIP-Gurobi
0.983
0.885
1.000
0.927
1.179
1.034
1.104
1.169
1.066
1.227
Appendix
Table 8: Complete Numerical Verification Results for the Sigmoid Network
Certified Accuracy (%) ↑
Perturbation Budget ϵ
0.05
0.1
0.15
0.2
0.25
0.3
0.35
0.4
0.45
0.5
ReLU
AI2 [ Gehr et al., 2018 ]
99
98
97
95
93
89
70
46
30
25
FastLin [ Weng et al., 2018 ]
99
98
97
95
93
89
70
46
30
25
FastLip [ Weng et al., 2018 ]
99
98
97
95
93
89
70
46
30
25
MaxSens [ Xiang et al., 2018 ]
98
89
64
37
15
9
6
2
0
0
Neurify [ Wang et al., 2018a ]
100
99
97
97
95
92
85
69
49
36
Appendix
Table 9: Complete Numerical Verification Results of Benders Algorithm
This paper investigates the computational complexity of verification problems for Binarized Neural Networks (BNNs), in which activations and weights are binary. Specifically, we study three verification problems. First, we prove that checking the satisfiability of a linear property for a BNN is NP-complete via a reduction from the Boolean Satisfiability (SAT) problem. Second, we show that verifying robustness under non-uniform image occlusion is NP-complete through a reduction from SAT. Finally, we demonstrate that uniform occlusion induces a piecewise-constant structure in the network output, which enables the design of a polynomial-time algorithm for robustness verification.
Neural network verification has become a key tool for providing formal guarantees on the behaviour of neural networks. However, many verification problems remain computationally intractable in the worst case: even for common adversarial robustness specifications, verification is NP-complete. Here, we explore the application of solver-level warmstarting for neural network verification to exploit information from previous solutions. We study the effect on running time as several properties are modified, including perturbation radii, input data and the networks themselves, using a pipeline that is generalisable and potentially adaptable to state-of-the-art verifiers. Our results show that warmstarting can significantly reduce verification time in most cases. Moreover, warmstarting enables the successful verification of instances that could not be solved from scratch within the given time limit.
Annelot Bosman, Minghao Liu, Marta Kwiatkowska +2
Leiden Institute of Advanced Computer Science, Leiden · University of Oxford, United Kingdom · Chair for AI Methodology, RWTH Aachen University, Germany +1
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.
Adrian Wurm
BTU Cottbus–Senftenberg, Lehrstuhl Theoretische Informatik Platz der Deutschen Einheit 1, 03046 Cottbus, Germany