# Using Z3 for Formal Modeling and Verification of FNN Global Robustness

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 14 of its 27 references that are in the map.
- First posted on arXiv 20 Apr 2023.

## Builds on (most cited first, 14 of 14)

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Fashion-MNIST: a Novel Image Dataset for Benchmarking Machine Learning Algorithms](https://mlsanity.com/paper/1708.07747/) (2017)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Towards Stable and Efficient Training of Verifiably Robust Neural Networks](https://mlsanity.com/paper/1906.06316/) (2019)
- [Abduction-Based Explanations for Machine Learning Models](https://mlsanity.com/paper/1811.10656/) (2018)
- [A Symbolic Approach to Explaining Bayesian Network Classifiers](https://mlsanity.com/paper/1805.03364/) (2018)
- [Verification for Machine Learning, Autonomy, and Neural Networks Survey](https://mlsanity.com/paper/1810.01989/) (2018)
- [Extracting Weighted Finite Automata from Recurrent Neural Networks for Natural Languages](https://mlsanity.com/paper/2206.14621/) (2022)
- [Provably Tightest Linear Approximation for Robustness Verification of Sigmoid-like Neural Networks](https://mlsanity.com/paper/2208.09872/) (2022)

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

- [Sharpness-Aware Minimization Alone can Improve Adversarial Robustness](https://mlsanity.com/paper/2305.05392/) (2023)
- [Tight Verification of Probabilistic Robustness in Bayesian Neural Networks](https://mlsanity.com/paper/2401.11627/) (2024)
- [A Survey of Neural Network Robustness Assessment in Image Recognition](https://mlsanity.com/paper/2404.08285/) (2024)
- [Neuro-Symbolic AI for Cybersecurity: State of the Art, Challenges, and Opportunities](https://mlsanity.com/paper/2509.06921/) (2025)
- [Enhancing Adversarial Attacks: The Similar Target Method](https://mlsanity.com/paper/2308.10743/) (2023)

## Abstract (arXiv)

While Feedforward Neural Networks (FNNs) have achieved remarkable success in various tasks, they are vulnerable to adversarial examples. Several techniques have been developed to verify the adversarial robustness of FNNs, but most of them focus on robustness verification against the local perturbation neighborhood of a single data point. There is still a large research gap in global robustness analysis. The global-robustness verifiable framework DeepGlobal has been proposed to identify textitall possible Adversarial Dangerous Regions (ADRs) of FNNs, not limited to data samples in a test set. In this paper, we propose a complete specification and implementation of DeepGlobal utilizing the SMT solver Z3 for more explicit definition, and propose several improvements to DeepGlobal for more efficient verification. To evaluate the effectiveness of our implementation and improvements, we conduct extensive experiments on a set of benchmark datasets. Visualization of our experiment results shows the validity and effectiveness of the approach.