On The Verification of Neural ODEs with Stochastic Guarantees
This work provides a method for verifying the safety and reliability of Neural ODEs, which is crucial for their deployment in safety-critical applications, by offering stochastic guarantees on their reachable states.
This paper addresses the verification of Neural ODEs by introducing Stochastic Lagrangian Reachability (SLR), a technique that constructs a tight Reachtube with stochastic guarantees in the form of confidence intervals for its bounds. SLR avoids the wrapping effect by using local optimization to expand safe regions and employs a novel forward-mode adjoint sensitivity method for efficient gradient computation.
We show that Neural ODEs, an emerging class of time-continuous neural networks, can be verified by solving a set of global-optimization problems. For this purpose, we introduce Stochastic Lagrangian Reachability (SLR), an abstraction-based technique for constructing a tight Reachtube (an over-approximation of the set of reachable states over a given time-horizon), and provide stochastic guarantees in the form of confidence intervals for the Reachtube bounds. SLR inherently avoids the infamous wrapping effect (accumulation of over-approximation errors) by performing local optimization steps to expand safe regions instead of repeatedly forward-propagating them as is done by deterministic reachability methods. To enable fast local optimizations, we introduce a novel forward-mode adjoint sensitivity method to compute gradients without the need for backpropagation. Finally, we establish asymptotic and non-asymptotic convergence rates for SLR.