# Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems

arXiv: https://arxiv.org/abs/2312.10842 · HTML: https://mlsanity.com/paper/2312.10842/

## 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 (most cited first, 21 of 21)

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [A Dual Approach to Scalable Verification of Deep Networks](https://mlsanity.com/paper/1803.06567/) (2018)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [Verifying Properties of Binarized Deep Neural Networks](https://mlsanity.com/paper/1709.06662/) (2017)
- [POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems](https://mlsanity.com/paper/2106.13867/) (2021)
- [Towards Scalable Verification of Deep Reinforcement Learning](https://mlsanity.com/paper/2105.11931/) (2021)
- [JuliaReach: a Toolbox for Set-Based Reachability](https://mlsanity.com/paper/1901.10736/) (2019)
- [Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes](https://mlsanity.com/paper/2112.09197/) (2021)
- [CLN2INV: Learning Loop Invariants with Continuous Logic Networks](https://mlsanity.com/paper/1909.11542/) (2019)
- [Testing and verification of neural-network-based safety-critical control software: A systematic literature review](https://mlsanity.com/paper/1910.06715/) (2019)
- [On Neural Network Equivalence Checking using SMT Solvers](https://mlsanity.com/paper/2203.11629/) (2022)
- [Parallel and Multi-Objective Falsification with Scenic and VerifAI](https://mlsanity.com/paper/2107.04164/) (2021)
- [NeuralExplorer: State Space Exploration of Closed Loop Control Systems Using Neural Networks](https://mlsanity.com/paper/2007.05685/) (2020)
- [On Symmetry and Quantification: A New Approach to Verify Distributed Protocols](https://mlsanity.com/paper/2103.14831/) (2021)
- [Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming](https://mlsanity.com/paper/2105.14311/) (2021)
- [Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+](https://mlsanity.com/paper/2205.06360/) (2022)

## 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.