Pause
Lecture
Moteur de recherche d'offres d'emploi CEA

Extending neural network support of artificial intelligence verification tool (PyRAT) H/F


Vacancy details

General information

Organisation

The French Alternative Energies and Atomic Energy Commission (CEA) is a key player in research, development and innovation in four main areas :
• defence and security,
• nuclear energy (fission and fusion),
• technological research for industry,
• fundamental research in the physical sciences and life sciences.

Drawing on its widely acknowledged expertise, and thanks to its 16000 technicians, engineers, researchers and staff, the CEA actively participates in collaborative projects with a large number of academic and industrial partners.

The CEA is established in ten centers spread throughout France
  

Reference

2021-18418  

Description de l'unité

Among other activities, CEA List's Software Safety and Security
Laboratory (LSL) research teams design and implement automated
analysis in order to make software systems more trustworthy, to
exhaustively detect their vulnerabilities, to guarantee conformity to
their specifications, and to accelerate their certification. Recently the field of activity of the laboratory has been extended to artificial intelligence safety and security verification. In particular, PyRAT and CAISAR are two tools developed in that context to verify safety properties on neural networks using abstract interpretation techniques.

Position description

Category

Information system

Contract

Internship

Job title

Extending neural network support of artificial intelligence verification tool (PyRAT) H/F

Subject

This internship will focus on implementing new types of neural networks such as recurrent neural network in the PyRAT tool which serves to verify safety properties on artificial intelligence systems.

Contract duration (months)

5-6

Job description


PyRAT is a tool that leverages the principles of abstract interpretation to propagate abstract domains (input) through abstract operations representing the layers of the neural network and in order to assess the reachable states (output). In comparison to classical software verification, PyRAT works directly on the weights, biases, and parameters of a neural network model thus making PyRAT lighter and faster to use for neural network analyses.
PyRAT is developed in Python as it is a widely used language for neural network frameworks such as Keras, Pytorch or Tensorflow. As of now, the primary use of PyRAT is to assess robustness w.r.t. some perturbation around inputs on small neural networks. However, on larger neural networks or on larger inputs a simple pass with PyRAT will lack precision.

To compensate the loss of precision in such cases, we introduced a domain splitting approach inside PyRAT. This iterative approach splits the input domain into smaller ones until PyRAT can prove the property on them or find a counterexample. This also allows to use PyRAT to also prove some safety properties, i.e. bigger intervals of input on certain neural networks.


In this internship, we aim to focus on exploring and understanding new types of neural network that are not currently supported by PyRAT such as Recurrent Neural Networks or Transformers. The former are of especially great interest as they are often found in use cases focusing on time series by our industrial partners. The layers and function of the network should be already available for the most part in PyRAT but the crux of the problem will be to modify the propagation in PyRAT to suit this kind of networks.
https://arxiv.org/pdf/2005.13300.pdf, https://arxiv.org/abs/2007.10135, https://arxiv.org/pdf/1905.07387.pdf

Methods / Means

Python, Tensorflow/Pytorch/Keras

Position location

Site

Saclay

Job location

France, Ile-de-France, Essonne (91)

Location

Palaiseau

Candidate criteria

Languages

  • English (Intermediate)
  • French (Intermediate)

PhD opportunity

Oui