# Verifying Global Two-Safety Properties in Neural Networks with Confidence

arXiv: https://arxiv.org/abs/2405.14400 · HTML: https://mlsanity.com/paper/2405.14400/

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 23 May 2024.

## Built on by (most cited first, 8 of 8)

- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [Revisiting Differential Verification: Equivalence Verification with Confidence](https://mlsanity.com/paper/2410.20207/) (2024)
- [Logic Gate Neural Networks are Good for Verification](https://mlsanity.com/paper/2505.19932/) (2025)
- [VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification](https://mlsanity.com/paper/2605.07451/) (2026)
- [The CAISAR Platform: Extending the Reach of Machine Learning Specification and Verification](https://mlsanity.com/paper/2506.12084/) (2025)
- [Probably Approximately Global Robustness Certification](https://mlsanity.com/paper/2511.06495/) (2025)
- [Formal Reasoning About Confidence and Automated Verification of Neural Networks](https://mlsanity.com/paper/2511.07293/) (2025)
- [Quantifying Sensitivity for Tree Ensembles: A symbolic and compositional approach](https://mlsanity.com/paper/2605.13830/) (2026)

## Abstract (arXiv)

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.