  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.
