建立神经ODE与ResNet间误差界，实现安全验证的双向互换。
Bridging Neural ODE and ResNet: A Formal Error Bound for Safety Verification
- 通过形式化误差界连接神经ODE与ResNet模型
- 误差界内输出集满足安全性质则另一模型也满足
- 适用于需要高效安全验证的深度学习系统
神经常微分方程（neural ODE）可视为残差网络（ResNet）在连续深度下的推广，而ResNet则是神经ODE的欧拉离散化。本文建立了二者间的正式误差关系，给出了近似误差的上界。该误差界使一个模型可作为另一个模型的安全验证代理：若在误差界内，某模型的可达输出集满足安全性质，则另一模型同样满足。该方法具有可逆性，安全验证可任选其一进行。实验以固定点吸引子系统为例，验证了该方法的有效性。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。