Forward invariance is a long-studied property in control theory that is used to certify that a dynamical system stays within some pre-specified set of states for all time, and also admits robustness guarantees (e.g., the certificate holds under perturbations). We propose a general framework for training and provably certifying robust forward invariance in Neural ODEs. We apply this framework to provide certified safety in robust continuous control. To our knowledge, this is the first instance of training Neural ODE policies with such non-vacuous certified guarantees. In addition, we explore the generality of our framework by using it to certify adversarial robustness for image classification.

翻译：前向不变性是控制理论中研究已久的一个性质，用于证明动力系统始终保持在某个预设的状态集合内，并且具有鲁棒性保证（例如，该性质在扰动下依然成立）。我们提出一个通用框架，用于训练并可证明地验证神经ODE中的鲁棒前向不变性。我们将该框架应用于鲁棒连续控制中的可证安全性。据我们所知，这是首次训练神经ODE策略并给出非平凡可证保证的工作。此外，我们通过将该框架用于图像分类的对抗鲁棒性验证，探索了其通用性。