Reachability Analysis of Deep Neural Networks with Provable Guarantees
This work addresses the problem of ensuring safety and reliability in deep neural networks for applications like autonomous systems and critical software, representing a novel method for a known bottleneck in verification.
The paper tackles the challenge of verifying correctness in deep neural networks by introducing a generic reachability problem that computes bounds on function values for given inputs, enabling safety verification, output range analysis, and robustness measures. The authors present a novel algorithm based on adaptive nested optimization, which is shown to be efficient, scalable, and capable of handling a broader class of networks than state-of-the-art methods.
Verifying correctness of deep neural networks (DNNs) is challenging. We study a generic reachability problem for feed-forward DNNs which, for a given set of inputs to the network and a Lipschitz-continuous function over its outputs, computes the lower and upper bound on the function values. Because the network and the function are Lipschitz continuous, all values in the interval between the lower and upper bound are reachable. We show how to obtain the safety verification problem, the output range analysis problem and a robustness measure by instantiating the reachability problem. We present a novel algorithm based on adaptive nested optimisation to solve the reachability problem. The technique has been implemented and evaluated on a range of DNNs, demonstrating its efficiency, scalability and ability to handle a broader class of networks than state-of-the-art verification approaches.