Attia, Ahmed Aziz
(2025).
« Les grands modèles de langage peuvent-ils comprendre les automates? » Mémoire.
Montréal (Québec, Canada), Université du Québec à Montréal, Maîtrise en informatique.
Fichier(s) associé(s) à ce document :
Résumé
L’émergence récente des modèles de langage de très grande taille (LLM) tels que GPT-4, DeepSeek, Claude 3, Gemini ou LLaMA 3 bouleverse l’automatisation des activités de production logicielle, depuis la rédaction de spécifications jusqu’aux étapes de vérification et de test. Dans ce contexte, les automates finis demeurent un formalisme central : ils décrivent les comportements séquentiels de nombreux composants logiciels, et ramènent les tests fonctionnels à la simple vérification de l’acceptation d’une chaîne d’entrée. Cette étude interroge les capacités de ces modèles à raisonner symboliquement sur des automates finis. Deux problèmes fondamentaux sont évalués : (i) la vérification d’acceptation, consistant à déterminer si un automate accepte une chaîne donnée; (ii) la génération d’une séquence acceptante minimale, qui requiert la production d’une chaîne de longueur minimale menant vers un état d’acceptation. Nous combinons pour cela cinq formats de représentation (Liste de transitions, Liste d’adjacence, DOT, Langage naturel contrôlé, et un format hybride) avec quatre stratégies de prompting (Question fermée, Approche normale, Approche assistée et Approche générique), explorant l’effet de ces choix sur les performances des LLM. Trois axes complémentaires structurent notre analyse expérimentale : la complexité structurelle des automates (Nombre d’états), la richesse de leur alphabet, et la longueur des chaînes d’entrée à traiter. Cette combinaison permet d’évaluer la robustesse des modèles face à des variations de structure, de contenu symbolique et de profondeur séquentielle, dans des conditions proches des applications réelles. Les résultats font apparaître des tendances robustes : les formats textuels, en particulier ceux encadrés par une approche assistée, obtiennent la meilleure précision pour la vérification d’acceptation. En revanche, la génération de la chaîne minimale reste extrêmement dépendante de la stratégie de prompt adopté. On observe que certains modèles, bien qu’ayant correctement identifié les transitions intermédiaires, échouent à synthétiser une réponse minimale, révélant une difficulté persistante dans le suivi des dépendances longues et la planification séquentielle. En termes de temps de calcul, la vérification d’acceptation nécessite entre 9 et 10 heures selon le nombre d’états, et entre 15 et 16 heures pour les alphabets élargis. La génération de séquences minimales dure de 12 à 13 heures sur les automates de tailles croissantes, et jusqu’à 20 heures avec de grands alphabets. Le benchmark sur la longueur des chaînes présente un coût supplémentaire, entre 11 et 13 heures, la complexité augmentant proportionnellement avec la longueur des séquences à traiter. En synthèse, nos observations offrent une cartographie fine des capacités et limites actuelles des LLMs dans des tâches formelles impliquant des automates finis, et fournissent des repères méthodologiques pour sélectionner un format de représentation et une stratégie de prompt engineering adaptés aux exigences de la vérification logicielle.
_____________________________________________________________________________
MOTS-CLÉS DE L’AUTEUR : Grands modèles de langage (LLMs), Théorie des automates, Vérification formelle, Génération de séquences, Ingénierie des prompts, Raisonnement symbolique, Représentations structurées.
| Type: |
Mémoire accepté
|
| Informations complémentaires: |
Fichier numérique reçu et enrichi en format PDF/A. |
|
Directeur de thèse: |
Avellaneda, Florent |
| Mots-clés ou Sujets: |
Grands modèles de langage / Théorie des automates / Automates finis / Rédactique |
| Unité d'appartenance: |
Faculté des sciences > Département d'informatique |
| Déposé par: |
Service des bibliothèques
|
| Date de dépôt: |
09 oct. 2025 12:23 |
| Dernière modification: |
09 oct. 2025 12:23 |
| Adresse URL : |
http://archipel.uqam.ca/id/eprint/19158 |
RECHERCHER
PARCOURIR
LIBRE ACCÈS
