Neural Network Verification with PyRAT

2024/10/31 by Augustin Lemesle, Lemesle, Augustin, Julien Lehmann +2 · 5 citations
Computer Science · Engineering · #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Fault Detection and Control Systems #Machine Learning (cs.LG) #Neural Networks and Applications

paper · pdf · doi:10.48550/arxiv.2410.23903

openalex publication_date 2024/10/31 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/30

Abstract

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.

Cited by

• Passive Learning of Lattice Automata from Recurrent Neural Networks
• Formal Verification of Local Robustness of a Classification Algorithm for a Spatial Use Case
• Efficient Certified Reasoning for Binarized Neural Networks
• Out of the Shadows: Exploring a Latent Space for Neural Network Verification
• The Luna Bound Propagator for Formal Analysis of Neural Networks

Related

• NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems
• Efficient Formal Safety Analysis of Neural Networks
• Towards Repairing Neural Networks Correctly
• Safety Verification of Neural Network Controlled Systems
• Formal Reasoning About Confidence and Automated Verification of Neural Networks