Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems
This addresses safety verification for neural network-controlled systems, which is critical for safety-critical applications, representing an incremental improvement over existing methods.
The paper tackles the challenge of verifying safety in Neural Network Controlled Systems (NNCS) by introducing a compositional inductive invariant method, which reduces verification time from hours or timeouts to seconds in case studies.
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.