Doctorant (H/F) en informatique fondamentale

Sujet de thèse :
Titre : Calcul de distances entre modèles de transducteurs et application à l’apprentissage approximatif de fonctions et relations sur les mots.
Encadrants : C. Aiswarya et Benjamin Monmege
Les transductions texte-à-texte sont un objet fondamental du calcul, apparaissant dans des applications telles que la traduction de code à code, le prétraitement de texte ou les transformations syntaxiques. Leurs modèles mathématiques formels, appelés transducteurs à états finis (FSTs), étendent les automates finis en associant des chaînes d’entrée à des chaînes de sortie. Les principales questions théoriques dans ce domaine incluent l’équivalence fonctionnelle (déterminer si deux transducteurs définissent la même transformation) et la vérification de type (s’assurer qu’une transduction préserve l’appartenance à un langage formel). Ces problèmes sont particulièrement pertinents en vérification de logiciels, où il est essentiel de garantir qu’une transformation de code préserve ses propriétés syntaxiques et sémantiques.
Cependant, la vérification d’équivalence exacte est difficile d’un point de vue algorithmique, voire indécidable dans de nombreux cas, ce qui motive le recours à des formes affaiblies ou approximatives d’équivalence. Dans cette thèse, nous proposons d’étudier en profondeur une relaxation de l’équivalence fonctionnelle appelée k-équivalence, où deux transducteurs sont dits équivalents si leurs sorties peuvent être converties l’une en l’autre avec au plus k modifications, en s’inspirant de la célèbre distance d’édition. Des résultats préliminaires ont été obtenus [1] sur cette notion pour les transducteurs mot-à-mot. Notre objectif est d’examiner les propriétés théoriques de cette notion sur des formes plus générales de transducteurs, comme les transducteurs associant à des mots hiérarchiques un mot (appelés transducteurs visibly pushdown [2]), les transducteurs sur mots à hiérarchies multiples pour modéliser des systèmes à piles multiples, ou encore les transducteurs sur mots de données [8]. Nous visons également à développer des algorithmes d’apprentissage efficaces pour ces transducteurs sous k-équivalence en utilisant le cadre de Angluin L* [3], d’abord pour les transducteurs mot-à-mot, mais aussi dans des généralisations comme les mots de données [7]. Nous faisons l’hypothèse que permettre de petites erreurs dans le processus d’apprentissage pourrait mener à des modèles plus compacts et mieux généralisables.
Plusieurs travaux ont étudié la vérification d’équivalence et l’apprentissage de modèles à états finis. Le travail fondateur d’Angluin sur l’apprentissage actif [3] constitue la base de l’apprentissage d’automates finis à partir de requêtes. Plus récemment, des progrès en apprentissage approximatif ont été réalisés sur les automates probabilistes et la recherche de chaînes robustes aux erreurs [6]. La complexité de la vérification d’équivalence exacte pour différentes cla
Voir plus sur le site emploi.cnrs.fr...