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.

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