We study the verification problem for closed-loop dynamical systems with neural-network controllers (NNCS). This problem is commonly reduced to computing the set of reachable states. When considering dynamical systems and neural networks in isolation, there exist precise approaches for that task based on set representations respectively called Taylor models and zonotopes. However, the combination of these approaches to NNCS is non-trivial because, when converting between the set representations, dependency information gets lost in each control cycle and the accumulated approximation error quickly renders the result useless. We present an algorithm to chain approaches based on Taylor models and zonotopes, yielding a precise reachability algorithm for NNCS. Because the algorithm only acts at the interface of the isolated approaches, it is applicable to general dynamical systems and neural networks and can benefit from future advances in these areas. Our implementation delivers state-of-the-art performance and is the first to successfully analyze all benchmark problems of an annual reachability competition for NNCS.
翻译:我们用神经网络控制器研究闭环动态系统(NNCS)的核查问题。 这个问题通常被简化为计算一组可达状态。 在孤立地考虑动态系统和神经网络时,根据分别称为泰勒模型和zonotoopes的设定表示,对这项任务有精确的方法。 然而,这些对NNCS的办法是非三边的,因为当设定表示法转换时,每个控制周期都失去依赖性信息,而累积的近似误差很快使结果变得毫无用处。 我们对基于Taylor模型和zonootos的链式方法提出算法,为NNCS提供精确的可达性算法。由于算法只对孤立方法的界面起作用,所以它适用于一般的动态系统和神经网络,并且能够从这些领域的未来进展中受益。 我们的实施提供了最新的业绩,并且是第一个成功分析NCS年度可达性竞争所有基准问题的算法。