We present the first automated verification technique for confidence-based 2-safety properties, such as global robustness and global fairness, in deep neural networks (DNNs). Our approach combines self-composition to leverage existing reachability analysis techniques and a novel abstraction of the softmax function, which is amenable to automated verification. We characterize and prove the soundness of our static analysis technique. Furthermore, we implement it on top of Marabou, a safety analysis tool for neural networks, conducting a performance evaluation on several publicly available benchmarks for DNN verification.

翻译：我们提出了首个针对深度神经网络（DNN）中基于置信度的双安全属性（如全局鲁棒性与全局公平性）的自动化验证技术。该方法通过自组合机制利用现有的可达性分析技术，并结合一种适用于自动化验证的新型softmax函数抽象。我们对该静态分析技术的可靠性进行了理论刻画与证明。此外，我们在神经网络安全分析工具Marabou上实现了该技术，并在多个公开可用的DNN验证基准数据集上进行了性能评估。