The integration of neural networks into safety-critical systems has shown great potential in recent years. However, the challenge of effectively verifying the safety of Neural Network Controlled Systems (NNCS) persists. This paper introduces a novel approach to NNCS safety verification, leveraging the inductive invariant method. Verifying the inductiveness of a candidate inductive invariant in the context of NNCS is hard because of the scale and nonlinearity of neural networks. Our compositional method makes this verification process manageable by decomposing the inductiveness proof obligation into smaller, more tractable subproblems. Alongside the high-level method, we present an algorithm capable of automatically verifying the inductiveness of given candidates by automatically inferring the necessary decomposition predicates. The algorithm significantly outperforms the baseline method and shows remarkable reductions in execution time in our case studies, shortening the verification time from hours (or timeout) to seconds.

翻译：将神经网络集成到安全关键系统中近年来展现出巨大潜力，然而，有效验证神经网络控制系统（NNCS）安全性的挑战依然存在。本文提出了一种新颖的NNCS安全性验证方法，利用了归纳不变量技术。由于神经网络规模庞大且具有非线性特性，在NNCS背景下验证候选归纳不变量的归纳性十分困难。我们的组合方法通过将归纳性证明义务分解为更小、更易处理的子问题，使这一验证过程变得可控。除高层方法外，我们还提出了一种算法，该算法能够通过自动推断必要的分解谓词，自动验证给定候选不变量的归纳性。该算法显著优于基线方法，并在我们的案例研究中展现出执行时间的显著缩减，将验证时间从数小时（或超时）缩短至秒级。