arXiv cs.AI· Abdelrahman Sayed Sayed, Pierre-Jean Meyer, Mohamed Ghazel·· 12 小时前AI 评分29
TNODEV：首个神经 ODE 形式化验证工具箱发布
TNODEV: Toolbox for Neural ODE Verification
AI 导读
TNODEV 是首个面向神经 ODE 的形式化验证器，将反例检查器、基于连续时间混合单调性的快速区间可达性后端、含三种输入集分割启发式的验证-精化循环与并行调度器整合为端到端流水线。
正文 · AI 翻译
摘要：神经常微分方程（neural ODE）在安全关键场景中受到关注，例如信息物理系统的连续时间控制器，以及集成到自动化决策流水线中的分类器，这引出了其行为能否被形式化验证的问题。现有的专用神经 ODE 工具仅提供单次可达性调用，没有迭代式输入集细化，因此其判定精度受限于单次可达性调用所能达到的水平。我们提出 TNODEV，这是首个神经 ODE 形式化验证器，它在单一端到端流水线中集成了反例检查器、基于连续时间混合单调性的快速区间可达性后端、带有三种输入集拆分启发式策略的验证与细化循环，以及一个并行调度器。TNODEV 支持对纯神经 ODE、与神经网络控制器闭环连接的神经 ODE 以及通用神经 ODE（GNODE）进行安全集包含验证，安全集可指定为区间，或指定为由目标分类标签诱导的半空间交集。我们在一系列基准上评估 TNODEV，涵盖安全集包含与分类鲁棒性性质，包括与 NNV 2.0 和 CORA 的直接可达性比较，以及在 MNIST 通用神经 ODE 分类器上与 NNV 2.0 的验证比较。
| Comments: | 44 页，10 幅图，已被 TMLR 2026 接收。代码见 此 https URL |
| Subjects: | 人工智能（cs.AI）；机器学习（cs.LG）；系统与控制（eess.SY）；动力系统（math.DS） |
| Cite as: | arXiv:2606.16567 [cs.AI] |
| （或使用 arXiv:2606.16567v3 [cs.AI] 查看此版本） | |
| https://doi.org/10.48550/arXiv.2606.16567 arXiv 颁发的 DOI（经 DataCite） |
Submission history
提交人：Abdelrahman Sayed Sayed [查看邮箱]
[v1]
2026 年 6 月 15 日星期一 11:09:06 UTC（1,582 KB）
[v2]
2026 年 7 月 9 日星期四 15:36:14 UTC（1,582 KB）
[v3]
2026 年 10 月 21 日星期三 12:19:35 UTC（2,006 KB）
来源：arXiv cs.AI · arxiv.org