Newer
Older
<section class="section main-page">
<div class="container">
<!-- <h6><a href="/news/">All news</a></h6> -->
<div class="columns">
{% assign news = site.news | sort: 'date' | reverse %}
{% for new in news limit:3 %}
<div class="column is-on-third">
<div class="columns is-mobile">
<div class="column is-one-third has-text-centered">
<img class="image-news" src="{{ new.logo }}" style="max-height: 100px;">
</div>
<div class="column">
{{ new.title | truncatewords : 9 }}<br>
<strong><span id="{{ new.id }}"></span><script>var d = new Date({{ new.date | date: "%s000" }});
document.getElementById("{{ new.id }}").innerHTML = d.toLocaleString([], {year: 'numeric', month: 'numeric', day: 'numeric', hour: '2-digit', minute:'2-digit'});</script></strong><br>
<a href="{{ new.url | relative_url }}">More >></a>
</div>
</div>
</div>
{% if forloop.last == false %}
<div class="vl"></div>
{% endif %}
{% endfor %}
</div>
</div>
<div class="small-section">
<h1 class="title">PyRAT sails in to verify your neural networks</h1>
<h2 class="subtitle">Performing formal verification of mission-critical software</h2>
<div class="column is-two-third">
<p>
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 <strong>mission-critical software</strong>, 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 envisioned 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 <strong>main-streaming of safety practices</strong> in the development process can only be beneficial to neural network and AI systems as a whole and can increase our trust in them.
</p>
</div>
<div class="column is-one-third has-text-centered">
<img style="max-height: 350px" src="{{ '/assets/images/neural_network.png' | relative_url }}">
<div class="small-section">
<h1 class="title">Catching the winds of abstract interpretation</h1>
<h2 class="subtitle">Adapting state of the art approaches to tensor operations</h2>
<!-- <h1 class="title">Abstract interpretation ahoy!</h1> -->
<div class="column is-half">
<p>
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.
</p>
<p>
To do so, it propagates different types of abstract domains along the different layers of the neural network up until the output layer. This approach will overapproximate some of the operations of the layers 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.
<div class="column is-half has-text-centered">
<img style="max-height: 350px; width: 90%" src="{{ '/assets/images/abstract.png' | relative_url }}">
</div>
<div class="small-section">
<!-- <h1 class="title">Scouring the seven seas</h1> -->
<h1 class="title">Through plunder or pillage</h1>
<h1 class="subtitle">What do we verify?</h1>
<div class="columns is-multiline verify">
<div class="column is-half">
<div class="card">
<div class="card-header">
</div>
<div class="card-image">
<figure class="image is-2by1">
<img src="{{ '/assets/images/local-rob.png' | relative_url }}">
</figure>
</div>
<div class="card-content">
<p>
For all the points of a dataset, we verify their neighbourhood parametrized by a distance ε.
</p>
<p>
Here we can formally prove that for any perturbation inferior to ε the classification remains the same, i.e. the neural network is <strong>robust</strong> around this point.
If a counter-example is found the neighbourhood is proven to also be <strong>unsafe</strong>.
</p>
</div>
</div>
</div>
<div class="column is-half">
<div class="card">
<div class="card-header">
</div>
<div class="card-image">
<figure class="image is-2by1">
<img style="padding-bottom: 1.5em; padding-top:1em;" src="{{ '/assets/images/safety.png' | relative_url }}">
</figure>
</div>
<div class="card-content">
<p>
On the other hand we can prove more <strong>general safety properties</strong>, like here on the public ACAS-XU dataset and neural networks.
In a setting of <strong>critical system of aircraft collision avoidance</strong>, we aim to prove that for certain configurations of the two planes the neural network will answer as expected.<br>
For example, we could aim to prove:<br>
<div class="has-text-centered">
\forall \theta \in [0, \frac{\pi}{2}], v_{int}, v_{own}, \rho, \psi \implies \text{Neural network says turn left}
</div>
</p>
</div>
</div>
</div>
</div>
</div>
<div class="small-section">
<h1 class="title">PyRAT from bow to stern</h1>
<div class="key">
<div class="columns is-multiline">
<div class="column is-two-third">
<h2 class="subtitle">Wide support and state of the art performances</h2>
Due to an approach tailor made to neural networks and their high dimensionality, PyRAT is able to apply abstract interpretation techniques while fully leveraging tensor operations. <br>
A wide range of neural networks and their layers are already support in such forms in PyRAT with possibilities ranging from simple and small tabular problems and networks, to complex architectures with convolutional layers and skip connections.
Thanks to this, PyRAT is able to show comparable result to state of the art verification tools and even outperforming some on certain benchmarks.
</p>
</div>
<div class="column is-one-third has-text-centered">
<img src="{{ '/assets/images/time-pyrat.png' | relative_url }}">
</div>
</div>
<div class="columns is-multiline">
<div class="column is-one-third has-text-centered is-hidden-mobile">
<img src="{{ '/assets/images/visualising.png' | relative_url }}">
</div>
<div class="column is-two-third">
<h2 class="subtitle">Specifying the property and visualising the result</h2>
Through its own expressive property language or the VNNLib format, PyRAT allows to specify safety properties to verify over a neural network.<br>
Following its specification, one can visualise with PyRAT the result of an analysis with modulable precision on this property. This visualisation will show the safe, unknown and unsafe spaces corresponding to this property. In turn, this will allow to either refine the property or identify the gaps in the neural network training.
<div class="column is-one-third has-text-centered is-hidden-tablet">
<img src="{{ '/assets/images/visualising.png' | relative_url }}">
</div>
</div>
<div class="columns is-multiline">
<div class="column is-two-third">
Another key aspect of PyRAT lies in the input partitioning mechanisms that it employs. For lower dimensionality inputs, PyRAT is able to use input partitioning as a mean to increase the precision of the analysis and prove a wider range of property. This partitioning is reinforced by heuristics tailored to the abstract domains we use which allows a significant boost in precision on such networks<br>
As an example on the widely used and public benchmark ACAS-XU, PyRAT proves all the defined properties in 292s while state of the art tools such as nnenum takes 319s and neurify 1265s.
</p>
</div>
<div class="column is-one-third has-text-centered">
<img src="{{ '/assets/images/input-split.png' | relative_url }}">
</div>
</div>