Moteur de recherche d'offres d'emploi CEA

Efficient Formal Verification of Neural Networks H/F

Vacancy details

General information


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



Description de l'unité

The French Alternative Energies and Atomic Energy Commission (CEA) is a
key player in research, development, and innovation. Drawing on the widely
acknowledged expertise gained by its 16,000 staff spanned over 9 research centers
with a budget of 4.1 billion Euros, CEA actively participates in more than
400 European collaborative projects with numerous academic (notably as a
member of Paris-Saclay University) and industrial partners. Within the CEA
Technological Research Division, the #CEA-List institute addresses the challenges
coming from smart digital systems.
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.
The lab recently extended its activities on the topic of AI trustworthiness
and gave birth to a new research group: AISER (Artificial Intelligence Safety,
Explainability and Robustness).

Position description


Mathematics, information, scientific, software



Job title

Efficient Formal Verification of Neural Networks H/F


Formal verification of neural network is a very active field, using techniques
ranging from abstract interpretation (Singh et al. 2019), interval bound prop-
agation (Wang et al. 2021), Mixed Integer Linear Programming (Wong and
Kolter 2017) or Satisfaction Modulo Theory (SMT) calculus (Katz et al. 2019).
SMT-based approach are of particular interest, because neural networks have a
conceptually simple structure: no loops and almost linear arithmetic. The main
obstacle is computing non-linear activation functions, which has exponential
complexity. (Katz et al. 2019) approach uses temporary bound relaxations to
reduce the search space. Preliminary experiments in our lab showed another
promising venue: using Fourier-Motzkin variable elimination within the MCSAT
framework, along with activation pattern learning.

Contract duration (months)

4 to 6 month

Job description

The aim of this internship is to study the applicability of variable substitutions
to accelerate SMT solvers on neural network formal verification. To do so, the
intern will use the CAISAR open-source platform to manipulate the neural
networks control flow as logical formulaes. A suggested SMT solver to test
along CAISAR is Yices, as it has a native OCaml API, which is incidentally the
language CAISAR is written in.
The broad internship goals are:
• familiarization with the state-of-the-art on neural network verification
• implementation of a prototype variable elimination heuristic within the
CAISAR platform
• benchmark on selected datasets and verification problems

Methods / Means

Keywords: Formal Verification, Neural Network, Why3, CAISAR, Yices

Applicant Profile

The candidate will work at the crossroads of formal verification and artificial
intelligence. As it is not realistic to be expert in both fields, we encourage candi-
dates that do not meet the full qualification requirements to apply nonetheless.
We strive to provide an inclusive and enjoyable workplace. We are aware of
discriminations based on gender (especially prevalent on our fields), race or
disability, we are doing our best to fight them.
• Minimal
– Master student or equivalent (2nd/3rd engineering school year) in
computer science
– knowledge of OCaml
– knowledge of SMT solving, First Order Logic
– ability to work in a team, some knowledge of version control
• Preferred
– notions of AI and neural networks
– knowledge of Why3

Position location



Job location

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



Candidate criteria


  • English (Fluent)
  • French (Fluent)

Prepared diploma

Bac+5 - Master 2

PhD opportunity



Position start date