Advances in verification of ReLU neural networks

dc.contributor.authorRössig, Ansgar
dc.contributor.authorPetkovic, Milena
dc.date.accessioned2023-07-18T11:42:57Z
dc.date.available2023-07-18T11:42:57Z
dc.date.issued2020-10-27
dc.date.updated2023-06-15T14:14:25Z
dc.description.abstractWe 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 behaviour 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 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. The results indicate that our approach is very competitive with others, i.e. it outperforms the solvers of Bunel et al. (in: Bengio, Wallach, Larochelle, Grauman, Cesa-Bianchi, Garnett (eds) Advances in neural information processing systems (NIPS 2018), 2018) and Reluplex (Katz et al. in: Computer aided verification—29th international conference, CAV 2017, Heidelberg, Germany, July 24–28, 2017, Proceedings, 2017). In comparison to the solvers ReluVal (Wang et al. in: 27th USENIX security symposium (USENIX Security 18), USENIX Association, Baltimore, 2018a) and Neurify (Wang et al. in: 32nd Conference on neural information processing systems (NIPS), Montreal, 2018b), the number of necessary branchings is much smaller. Our solver is publicly available and able to solve the verification problem for instances which do not have independent bounds for each input neuron.en
dc.identifier.eissn1573-2916
dc.identifier.issn0925-5001
dc.identifier.urihttps://depositonce.tu-berlin.de/handle/11303/19293
dc.identifier.urihttps://doi.org/10.14279/depositonce-18089
dc.language.isoen
dc.rights.urihttps://creativecommons.org/licenses/by/4.0/
dc.subject.ddc500 Naturwissenschaften und Mathematik::510 Mathematik::510 Mathematik
dc.subject.otherneural networks verificationen
dc.subject.otherReLUen
dc.subject.otherMIPen
dc.titleAdvances in verification of ReLU neural networksen
dc.typeArticle
dc.type.versionpublishedVersion
dcterms.bibliographicCitation.doi10.1007/s10898-020-00949-1
dcterms.bibliographicCitation.issue1
dcterms.bibliographicCitation.journaltitleJournal of Global Optimization
dcterms.bibliographicCitation.originalpublishernameSpringer
dcterms.bibliographicCitation.originalpublisherplaceHeidelberg
dcterms.bibliographicCitation.pageend152
dcterms.bibliographicCitation.pagestart109
dcterms.bibliographicCitation.volume81
dcterms.rightsHolder.referenceCreative-Commons-Lizenz
tub.accessrights.dnbfree
tub.affiliationFak. 2 Mathematik und Naturwissenschaften::Inst. Mathematik::FG Software und Algorithmen für die diskrete Optimierung
tub.publisher.universityorinstitutionTechnische Universität Berlin

Files

Original bundle
Now showing 1 - 1 of 1
Loading…
Thumbnail Image
Name:
s10898-020-00949-1.pdf
Size:
757.78 KB
Format:
Adobe Portable Document Format
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
4.86 KB
Format:
Item-specific license agreed upon to submission
Description:

Collections