Réduire la fracture entre spécification expressive et vérification efficace pour l'apprentissage automatique // Bridging the embedding gap between expressive specification and efficient verification of machine learning

La vérification formelle de réseaux de neurones se heurte à une double tension entre d’une part,
la capacité à exprimer des spécifications compactes, expressives et décrivant des
propriétés de haut-niveau de systèmes comprenants des composants IA et, d’autre part, la possibilité
effective de traduire ces spécifications aux prouveurs états de l’art.

L'état de l'art présente un ensemble de propriétés dites « globales » qui décrivent des comportements généraux sur le composant IA.
Ces propriétés sont partiellement formalisées mais ne sont à l'heure actuelle pas exprimables dans les langages de spécification standards au sein de la communauté. Elles restent donc pour la plupart théoriques.

Cette thèse se propose de réduire cette tension en proposant une formalisation au sein du langage WhyML de ces propriétés. La compilation efficace de ces propriétés via des techniques de réécriture de graphe automatique seront ensuite investiguées, exploitant des encodages avancés de réseaux de neurones pour la vérification. L'état de l'art n'offrant à l'heure actuelle que peu de travaux sur la comparaison des performances de prouveurs, cette thèse investiguera également ce volet, en s'inspirant des approches de portfolio de prouveurs.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Formal verification of neural networks is facing a double-faceted issue. The expressiveness of specifications (as in: compact and close to human understanding) is apparently clashing with their efficient translation to state-of-the-art prover, who only support a fragment of arithmetic without quantifiers.

This thesis will investigate "global" properties. Such class of properties describe generic behaviours of neural networks, beyond the level of local samples. Such properties are currently partially specified and most of them cannot be soundly derived into standard prover queries. Using the expressive power of the WhyML specification langage, this thesis will strive to propose a common encoding for global properties and investigate their efficient compilation to prover queries thanks to automated graph editing techniques.

This thesis will also investigate the comparison of provers performance, in particular drawing inspiration from portfolio approaches.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Pôle fr : Direction de la Recherche Technologique
Pôle en : Technological Research
Département : Département Ingénierie Logiciels et Systèmes (LIST)
Service : LSL (DILS)
Laboratoire : Laboratoire pour la Sûreté du Logiciel
Date de début souhaitée : 01-11-2025
Ecole doctorale : Sciences et Technologies de l’Information et de la Communication (STIC)
Directeur de thèse : MRAIDHA Chokri
Organisme : CEA
Laboratoire : DRT/DILS//LSEA
URL : https://julien.girard-satabin.fr

Public/private mixed funding

Pôle fr : Direction de la Recherche Technologique
Pôle en : Technological Research
Département : Département Ingénierie Logiciels et Systèmes (LIST)
Service : LSL (DILS)