PyRAT sails out of the blue to verify your neural networks

Formal verification of safety properties

Machine learning, especially through artificial neural networks, is currently undergoing an impressive expansion, penetrating fields ranging from driving assistance to legal or medical assistance. While seemingly beneficial, this revolution is causing concern as it approaches real-world application in mission-critical softwares, as the fragility of these learning techniques is increasingly exposed, particularly in the face of malicious disruption. Some work is already underway to adapt formal methods, used for decades in the field of critical software, to these new technologies.

This is what is envisionned with PyRAT, a neural network verification tool developed at CEA. Its development was motivated by the difficulty we found in linking some tools with our neural networks but also with the aim of facilitating the integration of verification process in the whole neural network development process. Our belief is that the mainstreaming of safety practices in the development process can only be beneficial to neural network and AI systems as a whole and can increase our trust in them.

An abstract interpretation based tool

PyRAT stands for Python Reachability Assessment Tool and is based on abstract interpretation techniques with the aim of determining whether in a given neural network a certain state can be reach by the network from some initial parameters.

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 will overapproximate some of the operation of the layer and thus the output space reached will always be bigger than the exact output space. 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.

What do we verify?

Local robustess

For all the points of a dataset, we verify their neighbourhood parametrized by a distance ε.
Here we can formally prove that for any perturbation inferion to ε the classification remains the same, i.e. the neural network is robust around this point. If a counter-example is found the neighbourhood is proven to also be unsafe.

Safety properties

On the other hand we can prove more general safety properties, like here on the public ACAS-XU dataset and neural networks. In a setting of critical system of aircraft collision avoidance, we aim to prove that for certain configurations of the two planes the neural network will answer as expected.
For example, we could aim to prove:

PyRAT Key features

State of the art fast

Visualising the proof

Input partionning