mlsanityData to 14 Oct 2026

Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems

arXiv 2312.10842 ↗First posted 17 Dec 2023cs.LO cs.LG cs.SYcited by 0

Not on the map. Why?

Abstract (arXiv)

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.

Key facts. No citing papers in the map yet (data through 14 Oct 2026). Builds on 21 of its 48 references that are in the map. First posted on arXiv 17 Dec 2023.

Builds on

21 of 48 references.

References · 21

  1. 2019PyTorch: An Imperative Style, High-Performance Deep Learning Librarycited by 20,305
  2. 2017Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networkscited by 744
  3. 2016Safety Verification of Deep Neural Networkscited by 263
  4. 2021Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verificationcited by 228
  5. 2018Formal Security Analysis of Neural Networks using Symbolic Intervalscited by 185
  6. 2020NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systemscited by 128
  7. 2018A Dual Approach to Scalable Verification of Deep Networkscited by 125
  8. 2018Verisig: verifying safety properties of hybrid systems with neural network controllerscited by 84
  9. 2017Verifying Properties of Binarized Deep Neural Networkscited by 79
  10. 2021POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systemscited by 39
  11. 2021Towards Scalable Verification of Deep Reinforcement Learningcited by 33
  12. 2019JuliaReach: a Toolbox for Set-Based Reachabilitycited by 28
9 more
  1. 2021Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopescited by 26
  2. 2019CLN2INV: Learning Loop Invariants with Continuous Logic Networkscited by 20
  3. 2019Testing and verification of neural-network-based safety-critical control software: A systematic literature reviewcited by 12
  4. 2022On Neural Network Equivalence Checking using SMT Solverscited by 10
  5. 2021Parallel and Multi-Objective Falsification with Scenic and VerifAIcited by 8
  6. 2020NeuralExplorer: State Space Exploration of Closed Loop Control Systems Using Neural Networkscited by 2
  7. 2021On Symmetry and Quantification: A New Approach to Verify Distributed Protocolscited by 2
  8. 2021Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programmingcited by 2
  9. 2022Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+cited by 1

Built on by

Not cited yet.