Exact and Asymptotically Complete Robust Verifications of Neural Networks via Ising Solvers

Wenxin Li; Wenchao Liu; Anzhe Jiang; Weihao Li; Chuan Wang; Qi Gao; Yin Ma; Hai Wei

cs.LGFeb 28, 2026

Exact and Asymptotically Complete Robust Verifications of Neural Networks via Ising Solvers

Authors: Wenxin Li, Wenchao Liu, Anzhe Jiang, Weihao Li, Chuan Wang, Qi Gao, Yin Ma, Hai Wei,

Organizations: Beijing QBoson Quantum Technology Co., Ltd. · Tsinghua University · Beijing Normal University

Abstract

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(\lceil \log_2 κ\rceil)$ 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\times$ 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 $\Delta\to 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 ( $\kappa=2$ )	250	346	96	48	112	208	930	1,122
Step-Env ( $\kappa=4$ )	250	442	192	96	112	304	1,314	1,890
Step-Env ( $\kappa=8$ )	250	538	384	144	112	496	2,082	3,522
Step-Env ( $\kappa=16$ )	250	634	768	192	112	880	3,618	7,074
Step-Env ( $\kappa=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

\varepsilon

from 0.02 to 0.18, step size 0.02. As segment count

\kappa

increases from 2 to 64 (decreasing maximal width

\Delta

), 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 $\downarrow$			Mean Solve Time / Sample (s) $\downarrow$			Efficiency Gains vs. Farkas $\uparrow$
Budget $\epsilon$	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%	$\mathbf{16.50\times}$
0.04	78.0	0.00	214	23	22	1.082	0.084	0.090	89.7%	$12.88\times$
0.06	55.0	0.00	483	55	52	2.421	0.217	0.335	89.2%	$11.16\times$
0.08	31.0	0.00	809	100	94	5.434	0.451	0.938	88.4%	$12.05\times$
0.10	14.0	0.00	1,195	169	157	11.124	0.891	1.430	86.9%	$12.48\times$

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\times

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

\epsilon

(log scale). Standard Farkas cuts suffer severe combinatorial explosion up to 1,578 calls at

\epsilon=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

\epsilon

. 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

\epsilon=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

\epsilon=0.8

Appendix figures & tables6 assets

Supplementary material from the paper’s appendix.

Appendix

Model Formulation	Binary Variables / Neuron	Constraints / Neuron	Aux. Vars $u_{i}$ Needed?	Big-M Bounds Needed?	Coupling Constraints	LP Relaxation Tightness
Standard One-Hot (Big-M)	$\kappa$ (Linear)	$\mathcal{O}(\kappa)$ ( $4\kappa+3$ )	Yes ( $\kappa$ continuous)	Yes ( $[L_{j},U_{j}]$ )	Bilinear Big-M	Weak (bounds dependent)
Multiple-Choice (MC)	$\kappa$ (Linear)	$\mathcal{O}(\kappa)$ ( $3\kappa+3$ )	No	No	Local Linear Disjunctive	Tight (Convex Hull)
Special Ordered Set (SOS2)	$\kappa$ (Linear)	$\mathcal{O}(\kappa)$ ( $\kappa+4$ )	No	No	Linear Grid Weight Coupling	Tight (Convex Hull)
Exact Log-PW (Log-PWL)	$\lceil\log_{2}\kappa\rceil$ ( Logarithmic )	$\mathcal{O}(\log\kappa)$ ( $2\lceil\log_{2}\kappa\rceil$ )	No	No	Linear Vielma–Nemhauser	Tight (Convex Hull)

Appendix

Table 5: Comparison of MILP formulations for piecewise-linear verification with

\kappa

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	✓	$\times$
Duality [ Dvijotham et al., 2018 ]	monotonic	✓	$\times$
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

\ell_{\infty}

perturbation (

\varepsilon=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

\varepsilon=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 $\epsilon$		0.1	0.2	0.3	0.4	0.5	0.6
Vulnerable Samples $\uparrow$	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 $\epsilon$		0.1	0.2	0.3	0.4	0.5	0.6	0.7	0.8	0.9	1.0
Vulnerable Samples $\uparrow$	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) $\downarrow$	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 (%) $\uparrow$		Perturbation Budget $\epsilon$
Certified Accuracy (%) $\uparrow$		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

Neural Network Verification

Neural network verification develops methods to prove whether networks satisfy properties such as robustness, safety, and bounded output behavior.

See all 125 papers

Some Complexity Results for Robustness Verification for Binarized Neural Networks
Jun 17, 2026Harshit Goyal, Sudakshina DuttaNeural Network Verification Binary Neural Networks
Indian Institute of Technology Goa
Exploring Solver-Level Warmstarting for Neural Network Verification
Sep 22, 2026Annelot Bosman, Minghao Liu, Marta Kwiatkowska +2Neural Network Verification
Leiden Institute of Advanced Computer Science, Leiden · University of Oxford, United Kingdom · Chair for AI Methodology, RWTH Aachen University, Germany +1
Security Properties of Neural Networks as Decision Problems
Sep 30, 2026Adrian WurmNeural Network Verification Adversarial Attacks
BTU Cottbus–Senftenberg, Lehrstuhl Theoretische Informatik Platz der Deutschen Einheit 1, 03046 Cottbus, Germany

Jun 17, 2026J/K move · Enter open · S save

Some Complexity Results for Robustness Verification for Binarized Neural Networks

Harshit Goyal, Sudakshina Dutta

Indian Institute of Technology Goa

Neural Network Verification Binary Neural Networks Neural Network Robustness Certified Robustness

Open paper AskPDF arXiv

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.

Abstract

Neural Network Verification

Explore similar work

Some Complexity Results for Robustness Verification for Binarized Neural Networks

Exploring Solver-Level Warmstarting for Neural Network Verification

Security Properties of Neural Networks as Decision Problems