# Neural Network Verification with PyRAT

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

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- Builds on 22 of its 61 references that are in the map.
- First posted on arXiv 31 Oct 2024.

## Builds on (most cited first, 22 of 22)

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [Perfectly Parallel Fairness Certification of Neural Networks](https://mlsanity.com/paper/1912.02499/) (2019)
- [The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results](https://mlsanity.com/paper/2312.16760/) (2023)
- [A Review of Formal Methods applied to Machine Learning](https://mlsanity.com/paper/2104.02466/) (2021)
- [Output Range Analysis for Deep Neural Networks](https://mlsanity.com/paper/1709.09130/) (2017)
- [Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification](https://mlsanity.com/paper/1902.09866/) (2019)
- [Robustness Verification of Support Vector Machines](https://mlsanity.com/paper/1904.11803/) (2019)
- [CAISAR: A platform for Characterizing Artificial Intelligence Safety and Robustness](https://mlsanity.com/paper/2206.03044/) (2022)
- [Hybrid zonotopes: a new set representation for reachability analysis of mixed logical dynamical systems](https://mlsanity.com/paper/2106.14831/) (2021)
- [A Provable Defense for Deep Residual Networks](https://mlsanity.com/paper/1903.12519/) (2019)
- [Backward Reachability Analysis of Neural Feedback Systems Using Hybrid Zonotopes](https://mlsanity.com/paper/2303.10513/) (2023)
- [Hybrid Zonotopes Exactly Represent ReLU Neural Networks](https://mlsanity.com/paper/2304.02755/) (2023)
- [CAMUS: A Framework to Build Formal Specifications for Deep Perception Systems Using Simulators](https://mlsanity.com/paper/1911.10735/) (2019)

## Built on by (most cited first, 9 of 9)

- [Out of the Shadows: Exploring a Latent Space for Neural Network Verification](https://mlsanity.com/paper/2505.17854/) (2025)
- [SoundnessBench: A Soundness Benchmark for Neural Network Verifiers](https://mlsanity.com/paper/2412.03154/) (2024)
- [IoUCert: Robustness Verification for Anchor-based Object Detectors](https://mlsanity.com/paper/2603.03043/) (2026)
- [Efficient Certified Reasoning for Binarized Neural Networks](https://mlsanity.com/paper/2507.02916/) (2025)
- [Formal Verification of Local Robustness of a Classification Algorithm for a Spatial Use Case](https://mlsanity.com/paper/2509.03948/) (2025)
- [Lipschitz-Based Robustness Certification Under Floating-Point Execution](https://mlsanity.com/paper/2603.13334/) (2026)
- [The Luna Bound Propagator for Formal Analysis of Neural Networks](https://mlsanity.com/paper/2603.23878/) (2026)
- [Quantitative Linear Logic for Neuro-Symbolic Learning and Verification](https://mlsanity.com/paper/2605.13845/) (2026)
- [A Survey on the Verification of Reinforcement Learning Policies](https://mlsanity.com/paper/2607.16210/) (2026)

## Abstract (arXiv)

As AI systems are becoming more and more popular and used in various critical domains (health, transport, energy, ...), the need to provide guarantees and trust of their safety is undeniable. To this end, we present PyRAT, a tool based on abstract interpretation to verify the safety and the robustness of neural networks. In this paper, we describe the different abstractions used by PyRAT to find the reachable states of a neural network starting from its input as well as the main features of the tool to provide fast and accurate analysis of neural networks. PyRAT has already been used in several collaborations to ensure safety guarantees, with its second place at the VNN-Comp 2024 showcasing its performance.