连接神经 ODE 与 ResNet：用于安全性验证的形式化误差界
机器学习
2025-10-14 v2 人工智能
摘要
神经常微分方程（neural ODE）是一种机器学习模型，通常被描述为具有单个残差块的残差网络（ResNet）的连续深度推广，反之，ResNet 也可被视为神经 ODE 的 Euler 离散化。因此，这两个模型密切相关，任一模型的行为均被视为对另一模型行为的近似。在本工作中，我们通过界定两个相关模型之间的近似误差，建立了这两个模型之间更形式化的关系。所得的误差界使我们能够将其中一个模型作为另一个模型的验证代理，而无需运行两次验证工具：如果扩展了误差界的可达输出集在其中一个模型上满足安全性属性，则该安全性属性在另一模型上也得到保证。此特性是完全可逆的，初始安全性验证可在两个模型中的任一个上无差别地运行。通过将不动点吸引子系统建模为神经 ODE 的数值示例，展示了这一新颖方法。
引用
@article{arxiv.2506.03227,
title = {Bridging Neural ODE and ResNet: A Formal Error Bound for Safety Verification},
author = {Abdelrahman Sayed Sayed and Pierre-Jean Meyer and Mohamed Ghazel},
journal= {arXiv preprint arXiv:2506.03227},
year = {2025}
}
备注
18 pages, 5 figures, Accepted for publication in the proceedings of the 8th International Symposium on AI Verification SAIV 2025