Poste de doctorat F/M Apprentissage automatique fiable : Analyse et vérification des automates logiciel

Type de contrat : Contrat à durée déterminée Niveau de qualification requis : Diplôme de troisième cycle ou équivalent Fonction : Poste de doctorat Niveau d’expérience : Récemment diplômé Emplacement et environnement : Le doctorat aura lieu à l’INRIA Rennes (Bretagne, France). Sujet : L’apprentissage des automates à partir de leurs traces a longtemps été abordé d’un point de vue purement logique (par exemple l’algorithme L* d’Angluin), jusqu’à ce que les architectures neuronales offrent une alternative étonnante : des performances révolutionnaires, l’invocation de modèles à la frontière entre le monde continu et le monde discret, l’utilisation d’approches probabilistes... mais sans aucune garantie sur les modèles produits par les algorithmes d’apprentissage ! L’objectif de cette thèse est de mettre en lumière les propriétés de ces « automates souples », basés sur les réseaux de neurones, en croisant des perspectives issues de la théorie des systèmes, des statistiques, de l’optimisation et des méthodes formelles afin de fournir des garanties sur ces systèmes dynamiques, de comprendre leur expressivité, leur robustesse au bruit et aux attaques, ainsi que leur sensibilité à la qualité des données. La thèse examinera différentes architectures, allant des réseaux de neurones récurrents simples aux mécanismes de gating et d’attention, jusqu’aux architectures plus récentes comme les modèles d’espaces d’états ou Mamba. La conception de nouvelles architectures neuronales avec de meilleures propriétés, ainsi que la conception d’attaques de jailbreak et d’empoisonnement pour ces modèles sont également dans le champ d’application. Plus de détails ci-dessous. L’adaptation des techniques de vérification aux réseaux de neurones (NN) s’est (avec succès) concentrée sur un sujet assez restreint : quelle est la robustesse de la sortie d’un NN face aux perturbations sur l’entrée. Les approches standard sont empruntées à l’analyse statique et réalisent des raisonnements à l’échelle des neurones individuels. Outre les problèmes de scalabilité, ces méthodes sont orientées vers les classificateurs et s’adaptent à peine aux modèles de systèmes dynamiques. Pour la plupart, ils ont mis de côté l’énorme effort d’ingénierie qui a conduit à des architectures neuronales haute performance. Voici l’angle adopté ici : exploiter cette architecture pour adapter les approches de vérification. De nombreuses architectures neuronales ont été conçues pour identifier les systèmes dynamiques à partir de leurs traces. Nous nous concentrons ici sur l’apprentissage des automates à partir d’une partie de leur langage. Ces modèles sont entraînés comme prédicteurs du futur, uniquement à partir d’exemples positifs, et non comme classificateurs (décidant si un mot d’entrée est dans la langue ou non). Cela en fait des modèles génératifs, qui pourraient être utilisés comme substituts des automates, d’où le nom générique de « soft automata » puisque ces modèles calculent avec des nombres réels. Les réseaux neuronaux récurrents (RNN) sont l’architecture neuronale la plus naturelle qui vient à l’esprit lorsqu’on veut apprendre un automate. Bien qu’entraînés avec la descente de gradient, ces objets ont montré qu’ils convergent vers des comportements discrets : leur espace d’états tend à former des groupes dont la structure et les propriétés sont encore en cours d’étude. Des comportements similaires apparaissent avec des variantes comme LSTM ou GRU, qui introduisent des mécanismes de verrouillage afin d’empêcher la décroissance rapide de la mémoire du RNN simple. Ces propriétés émergentes suggèrent que comprendre la structuration de l’espace d’états de ces modèles est essentiel pour répondre à des questions telles que leur robustesse au bruit, à la qualité des données et aux attaques. De manière indépendante, le succès des transformers dans la modélisation/génération de texte a motivé leur adaptation au domaine plus large de l’analyse des séries temporelles. Il n’est pas encore clair si des modèles de fondation pourraient émerger dans ce domaine, mais des tentatives réussies ont été rapportées avec des architectures assez simples. Le plus simple est probablement PatchTST, dont les capacités d’apprentissage des automates restent à explorer (en prenant des mots dans la langue comme des séries temporelles). Une piste de recherche possible pourrait être d’identifier comment le mécanisme d’attention et le croquis des patchs dans une série temporelle se combinent pour identifier les caractéristiques d’une séquence, et de structurer en outre l’espace d’états de ces modèles. Toujours dans le but d’évaluer leurs capacités de généralisation et leur robustesse au bruit ou aux attaques. Plus récemment, d’autres architectures ont été introduites sous le terme générique de « modèles d’espace d’états », comme HiPPO ou S4, et plus tard Mamba. Bien qu’ils abordent à l’origine deux limitations des transformateurs, un contexte de fenêtre finie et un coût computationnel quadratique dans la taille de cette fenêtre, ils s’inspirent de modèles linéaires bien connus en théorie des systèmes, et ouvrent la voie à un espace d’états plus interprétable. Une orientation possible de la thèse pourrait donc être d’explorer la pertinence de ces modèles en tant qu’automates de substitution, et de reprendre leur structure interne pour concevoir des techniques d’analyse et de vérification. Les 3 axes de recherche mentionnées ci-dessus ne seront pas toutes explorées au même niveau. Le sujet sera adapté au candidat. Le candidat idéal doit avoir une solide formation en mathématiques, un goût pour les méthodes formelles et des compétences pour le travail expérimental utilisant des bibliothèques standard d’apprentissage automatique.