# Verifying Global Neural Network Specifications using Hyperproperties

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 24 of its 36 references that are in the map.
- First posted on arXiv 21 Jun 2023.

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

- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Identity Mappings in Deep Residual Networks](https://mlsanity.com/paper/1603.05027/) (2016)
- [Spectrally-normalized margin bounds for neural networks](https://mlsanity.com/paper/1706.08498/) (2017)
- [Parseval Networks: Improving Robustness to Adversarial Examples](https://mlsanity.com/paper/1704.08847/) (2017)
- [Large image datasets: A pyrrhic win for computer vision?](https://mlsanity.com/paper/2006.16923/) (2020)
- [GPTs are GPTs: An Early Look at the Labor Market Impact Potential of Large Language Models](https://mlsanity.com/paper/2303.10130/) (2023)
- [Deep ReLU Networks Have Surprisingly Few Activation Patterns](https://mlsanity.com/paper/1906.00904/) (2019)
- [Fairness Testing: Testing Software for Discrimination](https://mlsanity.com/paper/1709.03221/) (2017)
- [Globally-Robust Neural Networks](https://mlsanity.com/paper/2102.08452/) (2021)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Reachability Analysis of Deep Neural Networks with Provable Guarantees](https://mlsanity.com/paper/1805.02242/) (2018)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results](https://mlsanity.com/paper/2109.00498/) (2021)
- [Perfectly Parallel Fairness Certification of Neural Networks](https://mlsanity.com/paper/1912.02499/) (2019)
- [The Third International Verification of Neural Networks Competition (VNN-COMP 2022): Summary and Results](https://mlsanity.com/paper/2212.10376/) (2022)
- [Counterexample-Guided Learning of Monotonic Neural Networks](https://mlsanity.com/paper/2006.08852/) (2020)
- [ReluDiff: Differential Verification of Deep Neural Networks](https://mlsanity.com/paper/2001.03662/) (2020)
- [How Good is your Explanation? Algorithmic Stability Measures to Assess the Quality of Explanations for Deep Neural Networks](https://mlsanity.com/paper/2009.04521/) (2020)
- [Towards Proving the Adversarial Robustness of Deep Neural Networks](https://mlsanity.com/paper/1709.02802/) (2017)
- [CertiFair: A Framework for Certified Global Fairness of Neural Networks](https://mlsanity.com/paper/2205.09927/) (2022)
- [LipBaB: Computing exact Lipschitz constant of ReLU networks](https://mlsanity.com/paper/2105.05495/) (2021)
- [Efficient Global Robustness Certification of Neural Networks via Interleaving Twin-Network Encoding](https://mlsanity.com/paper/2203.14141/) (2022)
- [SpecRepair: Counter-Example Guided Safety Repair of Deep Neural Networks](https://mlsanity.com/paper/2106.01917/) (2021)

## Abstract (arXiv)

Current approaches to neural network verification focus on specifications that target small regions around known input data points, such as local robustness. Thus, using these approaches, we can not obtain guarantees for inputs that are not close to known inputs. Yet, it is highly likely that a neural network will encounter such truly unseen inputs during its application. We study global specifications that - when satisfied - provide guarantees for all potential inputs. We introduce a hyperproperty formalism that allows for expressing global specifications such as monotonicity, Lipschitz continuity, global robustness, and dependency fairness. Our formalism enables verifying global specifications using existing neural network verification approaches by leveraging capabilities for verifying general computational graphs. Thereby, we extend the scope of guarantees that can be provided using existing methods. Recent success in verifying specific global specifications shows that attaining strong guarantees for all potential data points is feasible.