神经 ODE 的混合单调性可达性分析：紧致性与效率之间的权衡

神经常微分方程（neural ODE）是描绘复杂 dynamical 系统行为的强大连续时间机器学习模型，但由于缺乏针对它们的可达性分析工具，其验证仍面临挑战。我们提出一种新型基于区间的可达性方法，利用连续时间混合单调性技术来计算神经 ODE 可达集的超近似。通过利用完全初始集及其边界的几何结构中的单调性特性，我们的方法确保了高效的边界传递。通过将神经 ODE 动力学嵌入混合单调系统，我们的区间方法在 TIRA 中实现，采用单步、递增与边界方法，提供相对于 CORA 的 zonotope 与 NNV2.0 star set 表示的 sound 且计算高效的超近似，同时在紧致性与效率之间进行权衡。这一权衡使该方法特别适用于高维、实时且安全关键的应用场景。将混合单调性应用于神经 ODE 可达性分析，为轻量级形式化分析开辟了新途径，利用单调嵌入的对称结构以及区间盒的几何简单性，实现可扩展的验证。本新方法通过螺旋系统与固定点吸引子系统这两个数值示例进行了说明，这两个系统均建模为神经 ODE。