Using Z3 for Formal Modeling and Verification of FNN Global Robustness

TL;DR

This paper presents an enhanced framework using Z3 SMT solver for comprehensive global robustness verification of FNNs, identifying all potential adversarial regions beyond test data samples.

Contribution

It provides a complete specification and implementation of DeepGlobal with improvements for more efficient global robustness verification of FNNs using Z3.

Findings

Effective identification of all adversarial regions

Improved verification efficiency

Validation on benchmark datasets

Abstract

While Feedforward Neural Networks (FNNs) have achieved remarkable success in various tasks, they are vulnerable to adversarial examples. Several techniques have been developed to verify the adversarial robustness of FNNs, but most of them focus on robustness verification against the local perturbation neighborhood of a single data point. There is still a large research gap in global robustness analysis. The global-robustness verifiable framework DeepGlobal has been proposed to identify \textit{all} possible Adversarial Dangerous Regions (ADRs) of FNNs, not limited to data samples in a test set. In this paper, we propose a complete specification and implementation of DeepGlobal utilizing the SMT solver Z3 for more explicit definition, and propose several improvements to DeepGlobal for more efficient verification. To evaluate the effectiveness of our implementation and improvements, we conduct extensive experiments on a set of benchmark datasets. Visualization of our experiment results shows the validity and effectiveness of the approach.