Neural Network Verification with PyRAT
Not on the map. Why?
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.
Key facts. Cited by 9 papers in the map (data through 7 Oct 2026). Builds on 22 of its 61 references that are in the map. First posted on arXiv 31 Oct 2024.
Builds on
22 of 61 references.
References · 22
- 2014Adam: A Method for Stochastic Optimizationcited by 36,960
- 2013Intriguing properties of neural networkscited by 5,114
- 2017Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networkscited by 739
- 2018Efficient Neural Network Robustness Certification with General Activation Functionscited by 439
- 2016Safety Verification of Deep Neural Networkscited by 262
- 2018Formal Security Analysis of Neural Networks using Symbolic Intervalscited by 185
- 2020Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifierscited by 183
- 2019Branch and Bound for Piecewise Linear Neural Network Verificationcited by 138
- 2020NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systemscited by 128
- 2022Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Boundcited by 92
- 2019Perfectly Parallel Fairness Certification of Neural Networkscited by 42
- 2023The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Resultscited by 38
10 more
- 2021A Review of Formal Methods applied to Machine Learningcited by 33
- 2017Output Range Analysis for Deep Neural Networkscited by 30
- 2019Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verificationcited by 28
- 2019Robustness Verification of Support Vector Machinescited by 9
- 2022CAISAR: A platform for Characterizing Artificial Intelligence Safety and Robustnesscited by 9
- 2021Hybrid zonotopes: a new set representation for reachability analysis of mixed logical dynamical systemscited by 6
- 2019A Provable Defense for Deep Residual Networkscited by 5
- 2023Backward Reachability Analysis of Neural Feedback Systems Using Hybrid Zonotopescited by 4
- 2023Hybrid Zonotopes Exactly Represent ReLU Neural Networkscited by 4
- 2019CAMUS: A Framework to Build Formal Specifications for Deep Perception Systems Using Simulatorscited by 2
Built on by
Citing papers per year: 2024: 1; 2025: 3; 2026: 5.
9 papers.
- 2025Out of the Shadows: Exploring a Latent Space for Neural Network Verificationcited by 6
- 2024SoundnessBench: A Soundness Benchmark for Neural Network Verifierscited by 5
- 2026IoUCert: Robustness Verification for Anchor-based Object Detectorscited by 1
- 2025Efficient Certified Reasoning for Binarized Neural Networkscited by 0
- 2025Formal Verification of Local Robustness of a Classification Algorithm for a Spatial Use Casecited by 0
- 2026Lipschitz-Based Robustness Certification Under Floating-Point Executioncited by 0
- 2026The Luna Bound Propagator for Formal Analysis of Neural Networkscited by 0
- 2026Quantitative Linear Logic for Neuro-Symbolic Learning and Verificationcited by 0
- 2026A Survey on the Verification of Reinforcement Learning Policiescited by 0
- 2026A Survey on the Verification of Reinforcement Learning Policies14 May 2026
- 2026Quantitative Linear Logic for Neuro-Symbolic Learning and Verification13 May 2026
- 2026The Luna Bound Propagator for Formal Analysis of Neural Networks25 Mar 2026
- 2026Lipschitz-Based Robustness Certification Under Floating-Point Execution6 Mar 2026
- 2026IoUCert: Robustness Verification for Anchor-based Object Detectors3 Mar 2026
- 2025Formal Verification of Local Robustness of a Classification Algorithm for a Spatial Use Case4 Sep 2025
- 2025Efficient Certified Reasoning for Binarized Neural Networks25 Jun 2025
- 2025Out of the Shadows: Exploring a Latent Space for Neural Network Verification23 May 2025
- 2024SoundnessBench: A Soundness Benchmark for Neural Network Verifiers4 Dec 2024