GoTube: Scalable Stochastic Verification of Continuous-Depth Models
This addresses the challenge of scalable formal verification for continuous-depth neural networks, which is crucial for safety-critical applications in domains like autonomous systems, but it is incremental as it builds on existing reachability analysis methods.
The paper tackles the problem of verifying the behavioral robustness of continuous-depth models by introducing GoTube, a stochastic verification algorithm that constructs tight enclosures of process executions from initial state balls, showing it substantially outperforms state-of-the-art tools in terms of initial ball size, speed, time-horizon, task completion, and scalability.
We introduce a new stochastic verification algorithm that formally quantifies the behavioral robustness of any time-continuous process formulated as a continuous-depth model. Our algorithm solves a set of global optimization (Go) problems over a given time horizon to construct a tight enclosure (Tube) of the set of all process executions starting from a ball of initial states. We call our algorithm GoTube. Through its construction, GoTube ensures that the bounding tube is conservative up to a desired probability and up to a desired tightness. GoTube is implemented in JAX and optimized to scale to complex continuous-depth neural network models. Compared to advanced reachability analysis tools for time-continuous neural networks, GoTube does not accumulate overapproximation 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. GoTube is stable and sets the state-of-the-art in terms of its ability to scale to time horizons well beyond what has been previously possible.