On The Verification of Neural ODEs with Stochastic Guarantees

TL;DR

This paper introduces Stochastic Lagrangian Reachability (SLR), a novel verification method for Neural ODEs that provides probabilistic guarantees and efficiently computes safe state over-approximations without the wrapping effect.

Contribution

The paper presents SLR, a new abstraction-based verification technique for Neural ODEs that offers stochastic guarantees and improves over deterministic methods by avoiding the wrapping effect.

Findings

SLR constructs tight Reachtubes with stochastic confidence intervals.

SLR avoids the wrapping effect through local optimization steps.

A novel forward-mode adjoint sensitivity method accelerates gradient computations.

Abstract

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.