Deep learning methods can be used to produce control policies, but certifying
their safety is challenging. The resulting networks are nonlinear and often
very large. In response to this challenge, we present OVERT: a sound algorithm
for safety verification of nonlinear discrete-time closed loop dynamical
systems with neural network control policies. The novelty of OVERT lies in
combining ideas from the classical formal methods literature with ideas from
the newer neural network verification literature. The central concept of OVERT
is to abstract nonlinear functions with a set of optimally tight piecewise
linear bounds. Such piecewise linear bounds are designed for seamless
integration into ReLU neural network verification tools. OVERT can be used to
prove bounded-time safety properties by either computing reachable sets or
solving feasibility queries directly. We demonstrate various examples of safety
verification for several classical benchmark examples. OVERT compares favorably
to existing methods both in computation time and in tightness of the reachable
set.

使用 OVERT 算法结合经典形式化方法和新型神经网络验证方法，为验证深度学习控制策略的非线性闭环离散动态系统提供了一种确定性算法。该方法通过计算可达集或直接解决可行性查询来实现有界时间安全性证明，并在计算时间和可达集的精度方面优于现有的方法。