  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.
