How to act in a given situation? To answer this question, the use of neural networks (NNs) to analyse different parameters (inputs) and inferring recommendations (outputs) is becoming increasingly important.

Lighter, less energy-consuming, or better generalising on high-dimensional problems such as images, NNs have many advantages over classical systems for solving the problems they are given. As a result, they are increasingly being used in many fields, such as avoiding collisions between autonomous vehicles, detecting signs of disease in medical images, or monitoring the correct anchoring of oil platforms in real time.

By construction, a NN is a sequence of layers, sometimes non-linear, and neurons that use matrix operations to calculate an output from the provided inputs.

These networks are then trained using a training algorithm, which allows them to "learn" from known examples given as input and then generalise to new unknown inputs.

Nevertheless, their complexity makes them difficult to understand for users, who may see them as "black boxes": a system that can be used but whose inner workings are not understood.

The accuracy and results of NNs are getting closer to achieving acceptable performance in an industrial environment. However, as many academic studies have shown, NNs are still very sensitive to disturbances on their inputs. These can be unintentional (image compression, inaccuracy of source sensors) or malicious (adversarial attack).

NNs can therefore be compared to chaotic systems: a minimal variation on the input can radically affect the expected result. To guard against this, tools must be used to check their behaviour in the face of these potential variations!

This is the purpose of PyRAT: to establish zones of safety, by checking the decisions of the NN according to the possible variations in a given situation.

The operation of PyRAT is based on formal methods, in particular abstract interpretation, which consists in over-approximating the behaviour of a program (and its non-linear functions) in order to obtain the reachable set of its outputs.

The orange beam in front of the plane represents all the directions in which the plane can fly w.r.t. an intruder, and for which we want to prove that the NN always behaves in the desired way. The width of the orange beam together the distance to the intruder can be represented in a 2D space as an orange rectangle. If several input parameters vary the possible input space for the plane will be represented by a hyper-rectangle.

From this initial rectangle, PyRAT will test a safety property on the NN, i.e. whether the transformation by the model of the initial rectangle fits into the expected output (represented by another rectangle in the output space). Here, we want the avoidance system to never decide to turn towards the intruder for all given directions.

To increase the accuracy of the analysis, PyRAT will recursively subdivide the input space into smaller subspaces where the analysis will be more accurate. The precision here will therefore correspond to the allowed depth of this subdivision. Choosing a higher precision or different methods of subdividing the space (e.g. along width or height) will allow a more precise analysis. However, the overall analysis time will increase in proportion to the number of subdivisions made.

When verifying a safety property with PyRAT on a model, three outputs are possible. If PyRAT has shown the existence of a counterexample to the property, then the property is false. If PyRAT manages to show that all the spaces reached by all subdivision respect the property, then the property is globally verified. Otherwise, the result is unknown, i.e. we do not know whether the property is true or false.

This analysis of a NN with PyRAT can be done on an ad hoc basis, for example to certify the robustness of a system to a regulatory body. It can also be integrated directly into the training process of the NN, to improve the AI until a satisfactory level of robustness is achieved, making it tolerant to input variations.

In this 2D cross-section of the input space, we represent in blue the areas of the space where the property is correct and in grey the points where the property is false, the rest being unknown. In the green areas, it has been formally proven that no action other than the desired one is possible.

How to act in a given situation? To answer this question, the use of neural networks (NNs) to analyse different parameters (inputs) and inferring recommendations (outputs) is becoming increasingly important.

Lighter, less energy-consuming, or better generalising on high-dimensional problems such as images, NNs have many advantages over classical systems for solving the problems they are given. As a result, they are increasingly being used in many fields, such as avoiding collisions between autonomous vehicles, detecting signs of disease in medical images, or monitoring the correct anchoring of oil platforms in real time.

By construction, a NN is a sequence of layers, sometimes non-linear, and neurons that use matrix operations to calculate an output from the provided inputs.

These networks are then trained using a training algorithm, which allows them to "learn" from known examples given as input and then generalise to new unknown inputs.

Nevertheless, their complexity makes them difficult to understand for users, who may see them as "black boxes": a system that can be used but whose inner workings are not understood.

The accuracy and results of NNs are getting closer to achieving acceptable performance in an industrial environment. However, as many academic studies have shown, NNs are still very sensitive to disturbances on their inputs. These can be unintentional (image compression, inaccuracy of source sensors) or malicious (adversarial attack).

NNs can therefore be compared to chaotic systems: a minimal variation on the input can radically affect the expected result. To guard against this, tools must be used to check their behaviour in the face of these potential variations!

This is the purpose of PyRAT: to establish zones of safety, by checking the decisions of the NN according to the possible variations in a given situation.

The operation of PyRAT is based on formal methods, in particular abstract interpretation, which consists in over-approximating the behaviour of a program (and its non-linear functions) in order to obtain the reachable set of its outputs.

The three cubes R, G, and B represent the possible variations on each pixel of the input image and thus the whole space in which the analysed image may vary in case of perturbations. In this case, we want to prove that the DNN always gives the same decision for this whole space.

Therefore, PyRAT will only evaluate the local robustness of the NN to an image, ensuring that the output does not change for a small neighbourhood around the image. More generally, we will study this local robustness around a large number of images representative of the situation (a test set), which will then give us an estimate of the robustness of the model.

Here, due to the high dimensionality of the images, the recursive splitting used in scenario one is not possible. Therefore, another way to increase the accuracy of the analysis in PyRAT is to make the shape of the subspaces used in the analysis more complex. In a 2-dimensional input space, the analysis starts with a simple rectangle. Each non-linearity and layer of the network then adds a side to this rectangle until we reach a final shape for the output.

The more sides the shape of the subspace has, the more complex it is and thus the more accurate the analysis will be. However, the more sides there are, the longer the analysis will take.

When verifying a safety property with PyRAT on a model, three outputs are possible. If PyRAT has shown the existence of a counterexample to the property, then the property is false. If PyRAT manages to show that all the spaces reached by all subdivision respect the property, then the property is globally verified. Otherwise, the result is unknown, i.e. we do not know whether the property is true or false.

Here we represent in blue the number of images where the local robustness property is verified, i.e. it does not change the classification for our analysis margin and in grey the one which does not respect this property. The validity of the property on the other images is unknown due to lack of precision.

In the blue images, we prove that all possible variations in the analysis margin cannot lead to a different classification. Thus, it is impossible for a sensor error or an adversarial attack in this margin to affect the classification of the image.