Neural Network Verification with PyRAT

TL;DR

PyRAT is a tool utilizing abstract interpretation to verify neural network safety and robustness efficiently, demonstrating competitive performance in safety guarantees and robustness analysis.

Contribution

The paper introduces PyRAT, a novel verification tool that employs multiple abstractions for fast and accurate neural network safety analysis.

Findings

PyRAT achieved second place at VNN-Comp 2024.

It effectively verifies safety and robustness of neural networks.

The tool supports various abstractions for comprehensive analysis.

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.