Gaëtan SERRÉ : Soutenance de thèse

Gaëtan SERRÉ

Avancées méthodologiques et formalisation en optimisation globale

Résumé 

Les algorithmes d'optimisation globale sont nombreux et variés, mais sous leur surface résident des structures mathématiques partagées qui peuvent être identifiées et exploitées. Cette thèse fait progresser le domaine en reconnaissant ces structures sous-jacentes, en organisant les algorithmes en familles, en développant des avancées méthodologiques enracinées dans cette perspective, et en établissant des fondations formelles par le biais de cadres mathématiques rigoureux.

Parmi les algorithmes d'optimisation globale, deux familles se distinguent particulièrement: les approches à base de décision et les approches basées sur les dynamiques de McKean-Vlasov. Ces familles partagent des structures mathématiques profondes qui permettent le raisonnement et le transfert de résultats entre algorithmes. Dans ce cadre familial, cette thèse développe deux contributions méthodologiques majeures: i) l'introduction de Stein Boltzmann Sampling, un nouvel algorithme basé sur des dynamiques de McKean-Vlasov; ii) une approche modulaire pour ajouter du bruit commun dans les dynamiques de McKean-Vlasov, améliorant l'exploration tout en préservant la stochasticité en limite champ-moyen. L'approche du bruit commun exemplifie la puissance du raisonnement par famille: c'est un module unique applicable uniformément à toute une famille d'algorithmes. Cette thèse valide également cette perspective centrée sur les familles par une bibliothèque Python/C++ qui exploite la structure partagée pour maximiser la réutilisation du code et déployer des modules applicables à tous les algorithmes au sein d'une famille.

Ce raisonnement centré sur les familles motive naturellement l'étude de ce qui unifie les algorithmes d'optimisation à une échelle plus large. La seconde partie développe un cadre mathématique abstrait unifiant tous les algorithmes d'optimisation, incluant ceux des deux familles distinguées, dans un langage commun. Ce cadre unifié permet le raisonnement sur tous les algorithmes simultanément. Une application cruciale de ce cadre est l'établissement de fondations rigoureuses pour la recherche en optimisation globale par les méthodes formelles. Spécifiquement, cette thèse développe des contributions en L∀∃N qui formalisent des résultats clés sur les noyaux de Markov, et implémente à la fois le cadre unificateur et des algorithmes d'optimisation concrets, construisant une bibliothèque formelle fonctionnelle. Cela permet à la fois le raisonnement rigoureux sur la théorie des algorithmes d'optimisation et les développements formels réutilisables, ouvrant des possibilités pour la vérification mécanisée et l'intégration avec des outils émergents comme les modèles de langage.

Directeurs de thèse 

• Nicolas VAYATIS
• Argyris KALOGERATOS

Membres du Jury

• Gérard BIAU, Full professor, Sorbonne Université, Rapporteur
• Massimiliano PONTIL, Professor, Italian Institute of Technology, Rapporteur
• Gabriel PEYRE, Directeur de recherche, École Normale Supérieure, Examinateur
• Alain TROUVE, Professeure des universités, École Normale Supérieure Paris-Saclay, Examinateur
• Sylvie BOLDO, Directrice de recherche, Inria Saclay, Examinateur
• Anna KORBA, Professeure, ENSAE, Examinateur

Membre du jury invité

• Rémy Degenne, researcher, Inria Lille

Mots clés

Optimisation globale, McKean-Vlasov, Formalisation, McKean-Vlasov

Publications