Qui sommes-nous ?
Espace utilisateur
Formation continue
Credit : L. Godart/CEA
D’un jour à plusieurs semaines, nos formations permettent une montée en compétence dans votre emploi ou accompagnent vers le retour à l’emploi. 
Conseil et accompagnement
Crédit : vgajic
Fort de plus de 60 ans d’expériences, l’INSTN accompagne les entreprises et organismes à différents stades de leurs projets de développement du capital humain.
Thèses
Accueil   /   Thèses   /   Réduire la fracture entre spécification expressive et vérification efficace pour l'apprentissage automatique

Réduire la fracture entre spécification expressive et vérification efficace pour l'apprentissage automatique

Data intelligence dont Intelligence Artificielle Défis technologiques Informatique et logiciels Sciences pour l’ingénieur

Résumé du sujet

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.

Laboratoire

Département Ingénierie Logiciels et Systèmes (LIST)
LSL (DILS)
Laboratoire pour la Sûreté du Logiciel
Top envelopegraduation-hatlicensebookuserusersmap-markercalendar-fullbubblecrossmenuarrow-down