Robustness analysis of continuous-depth neural networks

Abstract

The main focus of this thesis is the development of a theory and associated algorithmsand tools, for the deterministic and statistical reachability analysis, of cyber-physicalsystems controlled by continuous-depth neural networks (CDNNs). We assume that the dynamics of the closed-system’s states is given by a set of ordinary differential equations(ODEs), and the output is a function of the solution of the ODEs at a given time.The primary motivation for this work is the huge potential of CDNNs in the design and implementation of safety-critical applications which are required to solve difficult tasks.So the main question of the thesis is: How to provide safety-guarantees, predictable behaviour, strong assurances, and thus trustworthiness, such that the use of CDNN controllers becomes a feasible strategy for safety-critical applications, too? In this thesis, we improve and extend state-of-the-art with two complementary approaches. The first, introduces a set of conservative, symbolic techniques and an algorithm, LRTNG, for the reachability analysis of nonlinear ODEs. This uses for the first time ananalytically computed metric for the ball enclosing the propagated reachable states, which is proven to minimize the ball’s volume. The second, first discusses a purely theoretical framework and shows that Neural-ODEs, an emerging class of CDNNs, can be verifiedby solving a set of global-optimization problems. It then introduces a new statistical verification algorithm, GoTube, that formally quantifies the behavioural robustness of anytime-continuous process formulated as a CDNN model, by computing statistical upperbounds of local Lipschitz constants. LRT-NG received the Outstanding Student-Paper Award from the IEEE CPS-DES TC, and GoTube won the Scientia Prize. We experimentally demonstrate that LRT-NG, our conservative algorithm, is the only symbolic tool capable of handling CDNNs, compared to the state-of-the-art tools such as LRT, CAPD and Flow*. Moreover, our experiments on a comprehensive set of ODE benchmarks, including two Neural ODEs, demonstrates LRT-NG’s superior performance. Compared to advanced reachability analysis tools for time-continuous neural networks, our statistical theory, and algorithm GoTube, does not accumulate over-approximation errors between time steps and avoids the infamous wrapping effect inherent in symbolic techniques. We show that GoTube substantially outperforms state-of-the-art verification tools in terms of the size of the initial ball, speed, time-horizon, task completion, and scalability on a large set of experiments. Our tools, LRT-NG and GoTube, are freely available on GitHub: https://github.com/DatenVorsprung.