Verifying Global Two-Safety Properties in Neural Networks with Confidence

TL;DR

This paper introduces an automated verification method for confidence-based 2-safety properties in neural networks, combining self-composition and a novel softmax abstraction to improve analysis of robustness and fairness.

Contribution

It presents the first technique for verifying confidence-based 2-safety properties in DNNs, integrating a new softmax abstraction with existing reachability analysis.

Findings

Effective verification of global robustness and fairness properties.

Implementation on Marabou shows promising performance.

Soundness of the static analysis technique is proven.

Abstract

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.