PARALLEL SMT-BASED VERIFICATION OF NEURAL NETWORKS BEFORE AND AFTER QUANTIZATION.

Abstract

The critical role of artificial neural networks (ANNs) in modern AI is counterbalanced by their inherent lack of transparency, often resulting in unexpected failures. To mitigate this risk, formal verification of neural network properties is essential, yet computationally intensive. Our work focuses on verifying ANNs both before and after quantization, examining the impact of quantization as an optimization technique to accelerate the verification process. We introduce a verification methodology for quantized neural networks (QNNs) that employs rational approximations of the network function, combined with set-based theory and interval arithmetic. To further enhance efficiency, we partition the primary verification property into sub-properties that can be verified in parallel. The approach is empirically evaluated on the Iris and highwayenv benchmarks using Marabou verification framework, demon- strating its efficacy for scalable and robust neural network verification.