PyRAT

The Python Reachability Analysis Tool (PyRAT) is a neural network verification tool developed internally at CEA. It is based on the technique called abstract interpretation.

PyRAT aims to determine whether a certain state can be reached in a given neural network. To do so, it propagates different types of abstract domains along the different layers of the neural network up until the output layer. This technique overapproximates some of the layer’s operations, thus the output space reached will always be bigger than the exact output space, providing sound reasoning. If the output space reached is inside a certain space defining the property we want, then we can say that the property is verified. Otherwise, we cannot conclude.

PyRAT leverages state-of-the-art machine learning frameworks to efficiently compute high-dimensional data, and supports a vast range of neural network architectures.

PyRAT is one of the verifier CAISAR uses to compute local robustness properties or safety properties.

See the official PyRAT website for more details.