Bridging Neural ODE and ResNet: A Formal Error Bound for Safety Verification

TL;DR

This work formalizes the relationship between neural ODEs and ResNets by deriving a rigorous set-based bound on their output discrepancy for a given input set 𝒳_in, using a Taylor (Lagrange) remainder to express Φ(1,u) = (u + f(u)) + ε(u) and constructing an over-approximation Ω_ε(𝒳_in). The resulting bound enables a reversible verification proxy: safety verified for one model via reachability analysis can be transferred to the other model when combined with the error bound, avoiding duplicate verification runs. The approach demonstrates notably tighter, set-based error bounds compared to scalar Lipschitz-based bounds and applies the proxy to a fixed-point attractor neural ODE, illustrating practical applicability for safety verification in continuous/discrete neural architectures.

Abstract

A neural ordinary differential equation (neural ODE) is a machine learning model that is commonly described as a continuous-depth generalization of a residual network (ResNet) with a single residual block, or conversely, the ResNet can be seen as the Euler discretization of the neural ODE. These two models are therefore strongly related in a way that the behaviors of either model are considered to be an approximation of the behaviors of the other. In this work, we establish a more formal relationship between these two models by bounding the approximation error between two such related models. The obtained error bound then allows us to use one of the models as a verification proxy for the other, without running the verification tools twice: if the reachable output set expanded by the error bound satisfies a safety property on one of the models, this safety property is then guaranteed to be also satisfied on the other model. This feature is fully reversible, and the initial safety verification can be run indifferently on either of the two models. This novel approach is illustrated on a numerical example of a fixed-point attractor system modeled as a neural ODE.

Figures (1)

• Figure 1: Illustration of the proposed framework to verify Model $1$ based on the outcome of the verification of Model $2$ and a bound $\varepsilon$ on the maximal error between the models.

Theorems & Definitions (1)

• remark thmcounterremark