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.

翻译：尽管神经网络作为信息物理系统的目标导向控制器具有巨大潜力，但验证基于神经网络的控制系统（NNCS）的安全性对神经网络的实际应用提出了重大挑战——特别是当需要无限时间域内的安全性时。其原因之一是神经网络与混合系统分析的难解性。我们提出VerSAILLE（通过逻辑关联包络实现可验证安全人工智能）：首个将微分动态逻辑（dL）与神经网络验证相结合的方法。通过协同作用，我们既可利用神经网络验证工具的高效性，又能保持dL的严格性。我们将控制器包络的安全证明映射到神经网络中，从而在无限时间域上证明具体NNCS的安全性。VerSAILLE产生的神经网络验证属性通常需要非线性算术，而高效的神经网络验证工具仅支持线性算术。为弥合这一鸿沟，我们提出Mosaic：首个针对分段线性神经网络上多项式实算术属性的完备可验证方法。Mosaic将线性属性的现成验证工具提升至非线性场景。对自适应巡航控制与空中碰撞避免等案例的评估表明，VerSAILLE与Mosaic具有多功能性：它们支持无限时间域安全认证与反例区域的穷举枚举，同时在闭环神经网络验证中显著超越现有最新工具。