Using Z3 for Formal Modeling and Verification of FNN Global Robustness

Autor:	Zhang, Yihao, Wei, Zeming, Zhang, Xiyue, Sun, Meng
Rok vydání:	2023
Předmět:	Computer Science - Machine Learning Computer Science - Artificial Intelligence Computer Science - Logic in Computer Science
Druh dokumentu:	Working Paper
Popis:	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. Comment: Accepted By SEKE 2023
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2304.10558 Zobrazit plný text záznamu View this record from Arxiv