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

Splitting approach and noise reduction for artificial intelligence verification tool 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-18419  

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

Splitting approach and noise reduction for artificial intelligence verification tool H/F

Subject

This internship's goal is to to explore and implement different heuristics and approaches for the propagation of noise symbols in a neural network using the PyRAT tool.

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.

For this internship, we focus on the noise introduced during a PyRAT analysis. Noise is introduced by PyRAT during its propagation through the network when it encounters non-linear functions. In neural networks such functions can be ReLUs, sigmoid... In such cases, PyRAT will overapproximate the function with a linear function and add some noise which in turn decreases the precision. To counter this, a first path to explore is to develop a splitting mechanism on certain function which are linear by pieces to avoid adding noise and handle them linearly in parallel. However, such splitting is exponential so a careful study of when to use it should be made. Additionally, this approach on domains such as the zonotopes that we are using in PyRAT will entail to add constraints on the zonotopes complexifying their concretization. A second idea to develop in this internship in order to prevent the number of noises to slow down processing, is to reduce periodically the number of noises. Here heuristics need to be planned to understand when the best timing to reduce the noise symbols is during propagation.

Methods / Means

Python, Tensorflow/Pytorch/Keras, Abstract Interpretation

Position location

Site

Saclay

Job location

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

Location

Palaiseau

Candidate criteria

Languages

  • French (Intermediate)
  • English (Intermediate)

PhD opportunity

Oui