body.html

<section class="section main-page">
	<div class="container">
		<h1 class="title">PyRAT sails out of the blue to verify your neural networks</h1>
		<h2 class="subtitle">Formal verification of safety properties</h2>
		<div class="columns is-multiline is-mobile">
			<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 softwares</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. 
			</p>
			<p>
			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 <strong>mainstreaming 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>
		</div>
		
		<h1 class="title">An abstract interpretation based tool</h1>
		<div class="columns is-multiline is-mobile">
			<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 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.
			</p>
			</div>
			
			<div class="column is-half">
			<img style="max-height: 350px" src="{{ '/assets/images/abstract.png' | relative_url }}">
			
			</div>			
		</div>		
		
		
		<h1 class="title">What do we verify?</h1>
		<div class="columns is-multiline is-mobile verify">
			<div class="column is-half">
				<div class="card">
					<div class="card-header">
						<h1 class="title">Local robustess</h1>
					</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 &epsilon;. 
						<br>Here we can formally prove that for any perturbation inferion to &epsilon; 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">
						<h1 class="title">Safety properties</h1>
					</div>
					<div class="card-image">				
						<figure class="image is-2by1">
							<img 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">
						<img src="{{ '/assets/images/safety-example.png' | relative_url }}">
						</div>
						</p>
					</div>
				</div>
			</div>
		</div>
		
		<h1 class="title">PyRAT Key features</h1>
		<div class="columns is-multiline is-mobile">
		</div>
	</div>
</section>


<!-- what to verify -->
<!-- key features -->