Efficient Formal Verification of Neural Networks H/F


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

Bac+5 - Master 2

Anglais Courant,Français Courant


Contact us

We will reply as soon as possible...