@inproceedings{c752d2b030614daa838cd5491c23b934,
title = "nnenum: Verification of ReLU Neural Networks with Optimized Abstraction Refinement",
abstract = "The surge of interest in applications of deep neural networks has led to a surge of interest in verification methods for such architectures. In summer 2020, the first international competition on neural network verification was held. This paper presents and evaluates the main optimizations used in the nnenum tool, which outperformed all other tools in the ACAS Xu benchmark category, sometimes by orders of magnitude. The method uses fast abstractions for speed, combined with refinement through ReLU splitting to increase accuracy when properties cannot be proven. Although the abstraction refinement process is a classic approach in formal methods, directly applying it to the neural network verification problem actually reduces performance, due to a cascade of overapproxmation error when using abstraction. This makes optimizations and their systematic evaluation essential for high performance.",
keywords = "ACAS Xu, Neural network verification, ReLU",
author = "Stanley Bak",
note = "Publisher Copyright: {\textcopyright} 2021, Springer Nature Switzerland AG.; 13th International Symposium on NASA Formal Methods, NFM 2021 ; Conference date: 24-05-2021 Through 28-05-2021",
year = "2021",
doi = "10.1007/978-3-030-76384-8\_2",
language = "English",
isbn = "9783030763831",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "19--36",
editor = "Aaron Dutle and Mu{\~n}oz, \{C{\'e}sar A.\} and Moscato, \{Mariano M.\} and Laura Titolo and Ivan Perez",
booktitle = "NASA Formal Methods - 13th International Symposium, NFM 2021, Proceedings",
}