TNODEV：神经ODE验证工具箱

摘要

本文提出了TNODEV，首个用于神经常微分方程（神经ODE）的可靠形式验证工具，集成了伪造检查、基于连续时间混合单调性的快速区间可达性后端、三种输入集分割启发式的验证与细化循环以及并行调度器。该工具支持纯神经ODE、与神经网络控制器闭环的神经ODE以及通用神经ODE的安全集包含验证，在多个基准测试中展示了其有效性。