While neural networks (NNs) have a large potential as goal-oriented
controllers for Cyber-Physical Systems, verifying the safety of neural network
based control systems (NNCSs) poses significant challenges for the practical
use of NNs -- especially when safety is needed for unbounded time horizons. One
reason for this is the intractability of NN and hybrid system analysis. We
introduce VerSAILLE (Verifiably Safe AI via Logically Linked Envelopes): The
first approach for the combination of differential dynamic logic (dL) and NN
verification. By joining forces, we can exploit the efficiency of NN
verification tools while retaining the rigor of dL. We reflect a safety proof
for a controller envelope in an NN to prove the safety of concrete NNCS on an
infinite-time horizon. The NN verification properties resulting from VerSAILLE
typically require nonlinear arithmetic while efficient NN verification tools
merely support linear arithmetic. To overcome this divide, we present Mosaic:
The first sound and complete verification approach for polynomial real
arithmetic properties on piece-wise linear NNs. Mosaic lifts off-the-shelf
tools for linear properties to the nonlinear setting. An evaluation on case
studies, including adaptive cruise control and airborne collision avoidance,
demonstrates the versatility of VerSAILLE and Mosaic: It supports the
certification of infinite-time horizon safety and the exhaustive enumeration of
counterexample regions while significantly outperforming State-of-the-Art tools
in closed-loop NNV.

通过使用差分动态逻辑（dL）和神经网络验证相结合的方法，我们引入了 VerSAILLE（通过逻辑链接的包络来确保安全的人工智能）来解决神经网络控制系统（NNCS）的安全性验证问题，同时提出了 Mosaic 来处理多项式实数算术性质在分段线性神经网络上的验证问题。我们的方法支持无限时间范围的安全性认证以及详尽枚举反例区域，并且在关闭环路的 NNV 中明显胜过现有的工具。