Current browse context:
cs.LO
Change to browse by:
References & Citations
Computer Science > Logic in Computer Science
Title: Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems
(Submitted on 17 Dec 2023 (v1), last revised 26 Mar 2024 (this version, v2))
Abstract: 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.
Submission history
From: Yuhao Zhou [view email][v1] Sun, 17 Dec 2023 23:20:51 GMT (17kb)
[v2] Tue, 26 Mar 2024 19:45:15 GMT (250kb,D)
Link back to: arXiv, form interface, contact.