TNODEV：首个支持迭代输入集细化的神经常微分方程形式化验证工具

研究团队发布 TNODEV，这是首个集成证伪检查器、基于连续时间混合单调性的快速区间可达性后端及验证细化循环的形式化验证器。 工具支持对纯神经 ODE、与神经网络控制器闭环连接的神经 ODE 以及通用神经 ODE（GNODE）进行安全集包含验证，安全集可通过区间或目标分类标签诱导的半空间交来表示。