7584
2020
eng
article
Springer
0
2020-10-27
--
--
Advances in Verification of ReLU Neural Networks
We consider the problem of verifying linear properties of neural networks. Despite their success in many classification and prediction tasks, neural networks may return unexpected results for certain inputs. This is highly problematic with respect to the application of neural networks for safety-critical tasks, e.g. in autonomous driving. We provide an overview of algorithmic approaches that aim to provide formal guarantees on the behavior of neural networks. Moreover, we present new theoretical results with respect to the approximation of ReLU neural networks. On the other hand, we implement a solver for verification of ReLU neural networks which combines mixed integer programming (MIP) with specialized branching and approximation techniques. To evaluate its performance, we conduct an extensive computational study. For that we use test instances based on the ACAS Xu System and the MNIST handwritten digit data set. Our solver is publicly available and able to solve the verification problem for instances which do not have independent bounds for each input neuron.
Journal of Global Optimization
10.1007/s10898-020-00949-1
urn:nbn:de:0297-zib-74174
yes
Ansgar RÃ¶ssig
Milena Petkovic
Milena Petkovic
Mathematical Optimization
MODAL-GasLab
MODAL-Gesamt
Petkovic, Milena
Applied Algorithmic Intelligence Methods
MODAL-EnergyLab
Freie UniversitÃ¤t Berlin