GoTube: Scalable Stochastic Verification of Continuous-Depth Models

Understand

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.