Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Exact and Asymptotically Complete Robust Verifications of Neural Networks via Quantum Optimization

Wenxin Li, Wenchao Liu, Chuan Wang, Qi Gao, Yin Ma, Hai Wei, Kai Wen

TL;DR

Two quantum-optimization-based models for robust verification that reduce the combinatorial burden of certification under bounded input perturbations are introduced and demonstrate high certification accuracy, indicating that quantum optimization can serve as a principled primitive for robustness guarantees in neural networks with complex activations.

Abstract

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.

Exact and Asymptotically Complete Robust Verifications of Neural Networks via Quantum Optimization

TL;DR

Two quantum-optimization-based models for robust verification that reduce the combinatorial burden of certification under bounded input perturbations are introduced and demonstrate high certification accuracy, indicating that quantum optimization can serve as a principled primitive for robustness guarantees in neural networks with complex activations.

Abstract

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.
Paper Structure (28 sections, 2 theorems, 94 equations, 3 figures, 6 tables, 1 algorithm)

This paper contains 28 sections, 2 theorems, 94 equations, 3 figures, 6 tables, 1 algorithm.

Table of Contents

  1. Uniform pruning error in the perturbation ball.
  2. Consequences for dataset-level certification.
  3. Network and pruning model.
  4. Setup.
  5. Suffix-side QUBO on the CIM.
  6. Datasets and Networks.
  7. Verification Methods.
  8. Evaluation Metrics.
  9. Experimental Environment and Hardware Configuration.
  10. ReLU networks.
  11. Hardtanh networks.
  12. Sigmoid Network.
  13. Binary encoding of continuous variables.
  14. Slack variables for inequality constraints and their binary encoding.
  15. Unified binary vector.
  16. ...and 13 more sections

Key Result

Theorem 1

Let $f(\mathbf{x})$ be the output of a DNN with an arbitrary activation function $\sigma(z)$, and let $L$ be the global Lipschitz constant of the network, defined as $L = \sup_{\mathbf{x}, \mathbf{x}' \in \mathcal{X}} \frac{\|f(\mathbf{x}) - f(\mathbf{x}')\|}{\|\mathbf{x} - \mathbf{x}'\|}$, where $\

Figures (3)

  • 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 quantum-amenable robustness verification workflow. The framework formulates the verification problem for an activation function as an optimization task, and solves it using an Ising solver.
  • Figure 3: Illustration of the piecewise constant approximation for arbitrary non-linear activation functions. The non-linear function is bounded by upper and lower step functions, enabling verification with asymptotic completeness using Ising solver.

Theorems & Definitions (3)

  • Theorem 1: Convergence to Exact Bounds
  • Theorem 2: Pruning-induced robustness transfer
  • proof