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.

翻译：尽管前馈神经网络（FNN）在各种任务中取得了显著成功，但它们容易受到对抗样本的攻击。目前已有多种技术被开发用于验证FNN的对抗鲁棒性，但大多数方法仅针对单个数据点的局部扰动邻域进行鲁棒性验证，全局鲁棒性分析仍存在较大研究空白。全局鲁棒性可验证框架DeepGlobal已被提出，用于识别FNN中所有可能的对抗危险区域（ADR），而不仅限于测试集中的数据样本。本文提出一种利用SMT求解器Z3对DeepGlobal进行完整规范定义与实现的方案，以提供更明确的定义，并对其提出若干改进以实现更高效的验证。为评估所提实现方案及改进的有效性，我们在若干基准数据集上开展了大规模实验。实验结果的直观展示验证了该方法的有效性与可行性。