Scalable Parallel Verification of Quantized Neural Networks via MIQCP Optimization Encoding

Abstract

Quantized Neural Networks are widely used in safety-critical systems due to their efficiency, yet they remain vulnerable to adversarial perturbations. Existing verification approaches based on the Big-<inline-formula> <tex-math notation="LaTeX">$M$ </tex-math></inline-formula> Mixed-Integer Linear Programming (MILP) suffer from loose relaxations and high computational cost. To address these issues, we propose a compact Mixed-Integer Quadratic Constrained Programming (MIQCP) encoding that introduces quadratic constraints to tighten feasible regions and reduce spurious branching. We further integrate DeepPoly-based symbolic interval analysis, which refines variable bounds and reduces the number of quadratic constraints. To enhance scalability, we design a sub-model decomposition and parallel verification framework, enabling efficient verification of large networks. We implement these techniques in PIQV, a parallel verifier for integer quantized networks. Experiments show that PIQV substantially outperforms a controlled Big-<inline-formula> <tex-math notation="LaTeX">$M$ </tex-math></inline-formula> MILP baseline (EQV*) built on the same abstract domain, resolving more instances in 11 of 12 large-perturbation settings (91.7%) with an average runtime reduction of 49.7% and up to a <inline-formula> <tex-math notation="LaTeX">$12\times $ </tex-math></inline-formula> speedup on deeper networks; the advantage further generalizes from fully connected to convolutional INT8 models and from MNIST to Fashion-MNIST.