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进行完整的形式化定义与实现，并针对该框架提出多项改进以提升验证效率。为评估实现方案与改进措施的有效性，我们在多个基准数据集上开展了广泛实验。实验结果的可视化展示了该方法的有效性与正确性。