Les jeux pour la synthèse, une perspective commune – G4S
G4S : Unifier la Logique, l’Optimisation et l’IA pour la Synthèse de Contrôleurs.
Le projet G4S propose une vision unifiée des jeux sur graphes en croisant les méthodes de la logique, de l’optimisation et de l’apprentissage par renforcement. L'objectif est de transformer automatiquement des spécifications complexes en programmes (contrôleurs) qui soient non seulement corrects, mais aussi simples, explicables et performants.
Défis technologiques et synergie interdisciplinaire pour la synthèse automatique.
- La synthèse de contrôleurs : Le défi est de construire automatiquement un programme capable de choisir des actions pour satisfaire une spécification donnée au sein d'un environnement (robotique, circuits, etc.). - Convergence de trois domaines : Le projet part du constat que l’automatique/logique, l’optimisation et l’apprentissage par renforcement (RL) étudient les mêmes modèles de jeux mais avec des cultures différentes. - Réconciliation des critères : L'enjeu est d'allier l'obsession de la correction propre aux méthodes formelles avec l'efficacité algorithmique de l'optimisation et la capacité d'adaptation en environnement inconnu du RL. - Objectifs principaux : Développer des algorithmes pour synthétiser des stratégies optimales, interprétables et vérifiables, tout en proposant des analyses de complexité plus fines (algorithmes "anytime").
- Représentation des stratégies : Utilisation de structures plus succinctes et lisibles que les réseaux de neurones classiques, telles que les arbres de décision, les formules logiques et les arbres de syntaxe abstraite (AST).
- Algorithmes "Anytime" : Modularisation des algorithmes de point fixe (itération de valeur et de politique) pour garantir des solutions approchées même en cas d'arrêt prématuré du calcul.
- Au-delà des récompenses numériques : Développement de nouvelles méthodes pour l’apprentissage par renforcement n'utilisant pas uniquement des scores numériques, notamment par le monitoring de formules LTL (Linear Temporal Logic).
- Communication et collaboration : Exploration des représentations basées sur la connaissance pour encourager la collaboration entre agents dans des jeux à information imparfaite.
- Avancées théoriques : Introduction des concepts d'arbres et de graphes universels, ayant permis d'améliorer les meilleurs algorithmes pour résoudre les jeux de parité.
- Interdisciplinarité réussie : Publication de résultats majeurs à l'intersection de l'IA et des méthodes formelles, notamment sur la synthèse de contrôleurs pour des spécifications de type "assume-guarantee".
- Algorithmes optimisés : Amélioration des performances pour les jeux stochastiques via une analyse fine des phases d'initialisation.
- Impact éducatif : Création d'un cours en ligne de 20 heures sur l'apprentissage par renforcement avec l'Alan Turing Institute.
- Intégration Deep Learning et Méthodes Formelles : Poursuite des travaux sur le projet DeepSynth pour utiliser l'apprentissage automatique dans la synthèse de programmes.
- Robotique : Application des méthodes de synthèse LTL aux problèmes de planification de trajectoires pour la robotique en environnement inconnu.
- Émergence de la communication : Étude de la collaboration entre agents dans des contextes complexes comme le jeu Hanabi.
L'objectif du projet G4S est d'étudier la synthèse de contrôleur, traditionnellement et indépendamment étudiée par trois domaines de l'informatique : automate et logique, apprentissage par récompense, et optimisation. Dans ce cadre un agent évolue dans un environnement dont certaines actions sont contrôlables et d'autres pas. Il s'agit de construire un programme choisissant les actions contrôlables de manière à satisfaire une spécification donnée. Les trois domaines contribuent chacun à l'étude de modèles de jeux pertinents pour la synthèse de contrôleur en posant des questions similaires, mais en utilisant des techniques différentes et avec des critères d'évaluation différents. L'ambition du projet G4S est d'unifier ces approches : d'une part de mieux comprendre et d'analyser les algorithmes existants à la lumière de critères issus d'autres domaines, et d'autre part de construire de nouveaux algorithmes combinant les techniques et qualités des trois domaines.
Coordination du projet
Nathanaël Fijalkow (Laboratoire Bordelais de Recherche en Informatique)
L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.
Partenariat
LaBRI Laboratoire Bordelais de Recherche en Informatique
Aide de l'ANR 139 145 euros
Début et durée du projet scientifique :
décembre 2021
- 36 Mois
