# Specification-Guided Safety Verification for Feedforward Neural Networks

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 Dec 2018.

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

- [Robust Machine Learning Systems: Challenges, Current Trends, Perspectives, and the Road Ahead](https://mlsanity.com/paper/2101.02559/) (2021)
- [OVERT: An Algorithm for Safety Verification of Neural Network Control Policies for Nonlinear Systems](https://mlsanity.com/paper/2108.01220/) (2021)
- [Constraint-Aware Refinement for Safety Verification of Neural Feedback Loops](https://mlsanity.com/paper/2410.00145/) (2024)
- [Work In Progress: Safety and Robustness Verification of Autoencoder-Based Regression Models using the NNV Tool](https://mlsanity.com/paper/2207.06759/) (2022)

## Abstract (arXiv)

This paper presents a specification-guided safety verification method for feedforward neural networks with general activation functions. As such feedforward networks are memoryless, they can be abstractly represented as mathematical functions, and the reachability analysis of the neural network amounts to interval analysis problems. In the framework of interval analysis, a computationally efficient formula which can quickly compute the output interval sets of a neural network is developed. Then, a specification-guided reachability algorithm is developed. Specifically, the bisection process in the verification algorithm is completely guided by a given safety specification. Due to the employment of the safety specification, unnecessary computations are avoided and thus the computational cost can be reduced significantly. Experiments show that the proposed method enjoys much more efficiency in safety verification with significantly less computational cost.