Scalable certification of Deep Neural Networks

<pre style="font-size: 11pt; overflow-wrap: break-word; font-family: &quot;Segoe UI&quot;, Consolas, Monaco, &quot;Courier New&quot;, Courier, monospace; color: rgb(0, 0, 0);">Looking for PhD candidates for a PhD in France and/or in Singapore: “Certification of Deep Neural Networks”
 
The candidate should have a background in Formal Methods and/or Artificial Intelligence/Machine Learning.
 
Possible advisors: Blaise Genest (DR CNRS, IRISA, Rennes) and Kuldeep S. Meel, Professor, NUS, Singapore.
 
Topic: Scalable certification of Deep Neural Networks
 
Description: Deep Neural Networks (DNNs) are able to achieve human-level accuracy in several challenging tasks, in domains with the potential for long-term impact on human society. Their large-scale adoption has however highlighted the brittleness of these systems to small perturbations [GSS15], in particular adversarial ones. To safely use them in a defense context, they need to be certified to be safe in all circumstances. The main issue to do that is that they are very hard to analyse, because of their size, and because they appear to be black box systems that work very well in practice, but with no provided rationale.
Several recent works [KBD+17, SGP+19, BFG19] show that certifying formally robustness of Deep Neural Networks should be feasible. There are however two main challenges to overcome if we want to certify large scale DNNs that are efficient in practice (~10^7 neurons): scalability, as current tools cannot handle more than ~10^5 neurons [SGP+19], and precision as well, as we have full precision only for DNNS with &lt;10^4 neurons [KBD+17], and obtain usually around 20-80% coverage for larger networks [SGP+19]. The aim of the thesis is to improve on both these dimensions for assessing and certifying robustness of larger DNNs against adversarial attacks.
The aim of the thesis is to develop a scalable fully automatic verification methodology for rigorous testing and certification of deep neural networks. We propose to use abstraction techniques, automatically refined guided by counter examples, following the highly efficient CEGAR framework.To do so, we porpose to reason about neurons nuclei, that is groups of neurons, rather than reason on individual neurons, which is usually done in the current tools [KBD+17, SGP+19]. This is related to partitioning into clusters, as used in [SGPV19] with some success. We have however some evidence that partitioning neurons still incurs a large loss of precision that cannot be recovered. Instead, we propose to consider non-disjoint nuclei, similarly as we have done successfully for the analysis of other kinds of networks (Dynamic Bayesian Networks) in [PPFG19]. This poses several challenges: how to deal mathematically with non-disjoint nuclei, and how to efficiently find nuclei that are necessary to consider. To automatically refine this choice where necessary, we will follow the highly efficient Counter-Example Guided Abstraction-Refinement (CEGAR) framework, which has been used successfully to speed-up complete but slow analysis of DNNS [EGK19].
 

</pre>