ML Security PapersExact and Asymptotically Complete Robust Verifications of Neural Networks via Quantum Optimization
Wenxin Li 1,2, Wenchao Liu 1, Chuan Wang 2, Qi Gao 1, Yin Ma 1,2, Hai Wei 1, Kai Wen 1
Published on arXiv
2603.00408
Input Manipulation Attack
OWASP ML Top 10 — ML01
Key Finding
Experiments on robustness benchmarks demonstrate high certification accuracy, indicating quantum optimization is a principled primitive for robustness guarantees in networks with complex activations
Quantum Benders Decomposition for NN Verification
Novel technique introduced
Deep neural networks (DNNs) enable high performance across domains but remain vulnerable to adversarial perturbations, limiting their use in safety-critical settings. Here, we introduce two quantum-optimization-based models for robust verification that reduce the combinatorial burden of certification under bounded input perturbations. For piecewise-linear activations (e.g., ReLU and hardtanh), our first model yields an exact formulation that is sound and complete, enabling precise identification of adversarial examples. For general activations (including sigmoid and tanh), our second model constructs scalable over-approximations via piecewise-constant bounds and is asymptotically complete, with approximation error vanishing as the segmentation is refined. We further integrate Quantum Benders Decomposition with interval arithmetic to accelerate solving, and propose certificate-transfer bounds that relate robustness guarantees of pruned networks to those of the original model. Finally, a layerwise partitioning strategy supports a quantum--classical hybrid workflow by coupling subproblems across depth. Experiments on robustness benchmarks show high certification accuracy, indicating that quantum optimization can serve as a principled primitive for robustness guarantees in neural networks with complex activations.
Key Contributions
- Exact sound-and-complete quantum optimization formulation for robust verification of ReLU/hardtanh networks that enables precise adversarial example identification
- Asymptotically complete over-approximation model for general activations (sigmoid, tanh) via piecewise-constant bounds with vanishing approximation error under segmentation refinement
- Quantum Benders Decomposition with interval arithmetic for accelerated solving, plus certificate-transfer bounds for pruned networks and a layerwise partitioning strategy for hybrid quantum-classical execution
🛡️ Threat Analysis
Paper directly addresses certified robustness against adversarial perturbations (bounded ℓ_p input perturbations causing misclassification) — certified robustness and formal verification are explicitly listed defenses under ML01. The method determines whether adversarial examples exist within a perturbation region, providing sound-and-complete guarantees.