Exact and Asymptotically Complete Robust Verifications of Neural Networks via Ising Solvers
Not on the map. Why?
Abstract (arXiv)
We present an Ising-compatible framework for formal neural-network robustness verification under bounded input perturbations. For piecewise-linear activations, the Exact Logarithmic PWL Model (Log-PWL) provides an exact, sound, and complete formulation with a state-optimal logarithmic encoding, reducing the binary variables per neuron from linear to information-theoretically minimal logarithmic complexity. For general bounded element-wise activations, the Asymptotic Step-Envelope Model (Step-Env) uses sound piecewise-constant envelopes whose lower and upper neuron states remain decision variables coupled to a common adversarial input. We prove that its globally optimized output bounds converge uniformly to the true network extrema as the segment width vanishes, yielding asymptotic completeness of verification. 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. Interval pruning, certificate transfer for pruned networks, and layerwise classical--Ising partitioning further reduce spin requirements. Experiments show exact certification fidelity for piecewise-linear networks and near-reference accuracy for sigmoid networks with compact spin budgets.
Key facts. No citing papers in the map yet (data through 14 Oct 2026). Builds on 28 of its 56 references that are in the map. First posted on arXiv 28 Feb 2026.
Builds on
28 of 56 references.
References · 28
- 2017Attention Is All You Needcited by 60,361
- 2015Deep Residual Learning for Image Recognitioncited by 52,096
- 2018BERT: Pre-training of Deep Bidirectional Transformers for Language Understandingcited by 40,399
- 2014Explaining and Harnessing Adversarial Examplescited by 7,364
- 2017Towards Deep Learning Models Resistant to Adversarial Attackscited by 6,415
- 2013Intriguing properties of neural networkscited by 5,155
- 2019Certified Adversarial Robustness via Randomized Smoothingcited by 1,340
- 2016End to End Learning for Self-Driving Carscited by 1,009
- 2017Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networkscited by 744
- 2017Provable defenses against adversarial examples via the convex outer adversarial polytopecited by 567
- 2018Efficient Neural Network Robustness Certification with General Activation Functionscited by 445
- 2014On the Number of Linear Regions of Deep Neural Networkscited by 381
16 more
- 2016Safety Verification of Deep Neural Networkscited by 263
- 2018Towards Fast Computation of Certified Robustness for ReLU Networkscited by 255
- 2019Algorithms for Verifying Deep Neural Networkscited by 221
- 2018Formal Security Analysis of Neural Networks using Symbolic Intervalscited by 185
- 2018Efficient Formal Safety Analysis of Neural Networkscited by 165
- 2017Bounding and Counting Linear Regions of Deep Neural Networkscited by 161
- 2019Deep ReLU Networks Have Surprisingly Few Activation Patternscited by 161
- 2017An approach to reachability analysis for feed-forward ReLU neural networkscited by 127
- 2018A Dual Approach to Scalable Verification of Deep Networkscited by 125
- 2016Measuring Neural Net Robustness with Constraintscited by 90
- 2024Neural Network Verification with Branch-and-Bound for General Nonlinearitiescited by 47
- 2017Output Range Analysis for Deep Neural Networkscited by 30
- 2017Reachable Set Computation and Safety Verification for Neural Networks with ReLU Activationscited by 22
- 2022QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networkscited by 12
- 2023Efficient MILP Decomposition in Quantum Computing for ReLU Network Robustnesscited by 4
- 2023Training Multi-layer Neural Networks on Ising Machinecited by 3
Built on by
Not cited yet.