Abstraction based Output Range Analysis for Neural Networks
This addresses the NP-hard computational bottleneck in verifying neural network safety for applications like autonomous systems, though it is an incremental improvement over existing satisfiability and optimization methods.
The paper tackles the computational complexity of output range analysis for ReLU neural networks by introducing an abstraction technique that constructs a simpler interval neural network (INN) to over-approximate the output range, reducing the problem to mixed integer linear programming and showing a trade-off between computation time and precision in experiments.
In this paper, we consider the problem of output range analysis for feed-forward neural networks with ReLU activation functions. The existing approaches reduce the output range analysis problem to satisfiability and optimization solving, which are NP-hard problems, and whose computational complexity increases with the number of neurons in the network. To tackle the computational complexity, we present a novel abstraction technique that constructs a simpler neural network with fewer neurons, albeit with interval weights called interval neural network (INN), which over-approximates the output range of the given neural network. We reduce the output range analysis on the INNs to solving a mixed integer linear programming problem. Our experimental results highlight the trade-off between the computation time and the precision of the computed output range.