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）安全验证的新方法，利用归纳不动点方法，并配合自动推断必要的分解谓词的算法，将验证过程从数小时（甚至超时）缩短至几秒钟，在案例研究中显著提高了验证性能。