Description du 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 classes de transducteurs a été explorée : voir [4] pour une synthèse, et par exemple [5] où des extensions pondérées sont considérées. D’autres modèles comme les transducteurs à registres appelés transducteurs de chaînes en flux (streaming string transducers) ont aussi été étudiés et se sont révélés décidables [9] (ils ont la particularité d’être déterministes, d’où le nom “streaming”). Toutefois, l’équivalence approximative reste largement inexplorée. Cette question est également fortement liée (et pourrait donc favoriser des avancées) à la recherche de modèles minimaux pour un langage donné ou une fonction mot-à-mot : alors que les automates finis sont minimisables, la recherche d’un tel objet minimal reste ouverte pour les transducteurs de chaînes en flux, où un compromis existe entre le nombre d’états et celui de registres.
En reliant ces domaines, cette thèse vise à développer un cadre théorique solide mais aussi applicable en pratique pour l’apprentissage de transductions approximatives.

Méthodologie
Notre approche comportera à la fois des volets théoriques et expérimentaux :
• Formalisation de la k-équivalence : Nous généraliserons la notion de k-équivalence introduite dans [1] pour les transducteurs mot-à-mot, en utilisant les distances d’édition standards (insertions, suppressions, substitutions), à divers autres modèles de transducteurs, notamment les visibly pushdown transducers, et étudierons leurs propriétés algorithmiques. Dans le cas des mots hiérarchiques (modélisant des capacités de pile), les modifications doivent être faites avec précaution car il n’est pas possible de supprimer un “push” sans également supprimer le “pop” associé.
• Conception d’algorithmes : Nous développerons des algorithmes efficaces pour vérifier la k-équivalence sur ces modèles de transducteurs plus généraux, et étudierons aussi le lien entre le problème d’équivalence approximative et celui de la minimisation, notamment pour les transducteurs de chaînes en flux.
• Apprentissage : Nous étendrons l’algorithme classique d’Angluin pour l’apprentissage des automates finis à l’équivalence approximative, en permettant à l’apprenant de tolérer de petites erreurs dans les réponses du professeur. Des extensions seront ensuite étudiées, notamment pour les mots de données.
• Évaluation empirique : Nous implémenterons et testerons nos algorithmes sur des jeux de données réels, comme des tâches de traduction de langages de programmation ou des jeux d’essai issus du traitement automatique du langage.
Nous prévoyons de publier les résultats dans les meilleures conférences et revues internationales en informatique théorique, mais aussi, en fonction des résultats empiriques, dans des lieux plus appliqués pour démontrer l'applicabilité de ces résultats théoriques à des domaines tels que les langages de programmation ou le traitement du langage naturel.
Cette proposition est ambitieuse et large, et le travail technique nécessaire sera exigeant. Toutefois, le risque relatif, lié aux questions difficiles que cette thèse soulève, est tempéré par le vaste champ de questions ouvertes, dont certaines sont à portée de main, permettant d’équilibrer les aspects à haut risque de la proposition. Il n’y a pas de point de blocage unique susceptible d’empêcher les progrès globaux.

Références
[1] C. Aiswarya, Amaldev Manuel, Saina Sunny (2024). Edit Distance of Finite State Transducers. ICALP 2024: 125:1–125:20
[2] Emmanuel Filiot, Jean-François Raskin, Pierre-Alain Reynier, Frédéric Servais, Jean-Marc Talbot (2018). Visibly pushdown transducers. Journal of Computer and System Sciences, 97, pp. 147–181
[3] Angluin, D. (1987). Learning regular sets from queries and counterexamples. Information and Computation, 75(2), 87–106
[4] Filiot, E., & Reynier, P. A. (2016). Transducers, logic and algebra for functions of finite words. Logical Methods in Computer Science, 12(3)
[5] Mohri, M. (2003). Finite-state transducers in language and speech processing. Computational Linguistics, 29(1), 23–27
[6] Balle, B., & Mohri, M. (2015). Learning weighted automata. Journal of Machine Learning Research, 16, 1625–1655
[7] B. Bollig, P. Habermehl, M. Leucker, and B. Monmege (2014). A robust class of data languages and an application to learning. Logical Methods in Computer Science, 10(4:19)
[8] Léo Exibard, Emmanuel Filiot, and Pierre-Alain Reynier (2019). Synthesis of Data Word Transducers. CONCUR 2019: LIPIcs, Volume 140
[9] R. Alur and P. Černý (2011). Streaming transducers for algorithmic verification of single-pass list-processing programs. POPL 2011, p. 599–610, ACM

Contexte de travail

La thèse se déroulera à Marseille, au Laboratoire d’Informatique et des Systèmes (LIS), au sein de l’équipe Modélisation et Vérification, dirigée par l’un des encadrants, Benjamin Monmege. L’équipe travaille sur des problématiques fondamentales liées à la vérification et à la synthèse de systèmes logiciels, en utilisant des méthodes formelles telles que le model-checking. La thèse sera co-encadrée par C. Aiswarya, maîtresse de conférences en Inde, au Chennai Mathematical Institute (CMI) : elle est membre du laboratoire de recherche international ReLaX, qui formalise la collaboration active entre la France et l’Inde en informatique théorique. La thèse se déroulera entièrement en France, mais le doctorant ou la doctorante aura la possibilité de se rendre en Inde s’il ou elle le souhaite, afin de faciliter la collaboration avec la co-encadrante.