Florent Bréhard, analyse numérique et preuve formelle

Quel est votre domaine de recherche ?

Florent Bréhard : Le calcul numérique validé désigne un ensemble de techniques dont le but est de représenter rigoureusement en machine des objets mathématiques (nombres, fonctions, courbes, etc.) pour lesquels il n’existe pas de formule close explicite. Pensons par exemple à un satellite artificiel mis en orbite autour de la Terre et soumis à diverses forces : sa trajectoire est la solution d’une équation différentielle mais ne peut pas s’exprimer à l’aide de fonctions élémentaires. Pour autant, cette équation fonctionnelle caractérise uniquement la trajectoire, et nous pouvons l’approcher rigoureusement avec, par exemple, un polynôme assorti d’une borne d’erreur. Cela donne un « tube » autour de la vraie trajectoire et permet entre autres de garantir que le satellite n’entrera pas en collision avec d’autres objets à proximité.

Pour calculer et manipuler de telles représentations numériques ensemblistes, il est souvent nécessaire de combiner les techniques traditionnelles de l’analyse numérique avec d’autres outils issus notamment du calcul formel et de l’optimisation. De plus, la preuve formelle, via l’assistant de preuve Coq, joue un rôle clé dans la certification des méthodes que je développe, ceci afin d’offrir un niveau de confiance optimal jusqu’à l’implémentation de ces algorithmes. Cette position privilégiée à la croisée de plusieurs branches de l’informatique contribue selon moi beaucoup au charme de ce domaine en plein développement qu’est le calcul numérique validé.

Enfin, les algorithmes et implémentations développés par cette communauté intéressent un public de plus en plus large et varié, avec d’une part des ingénieurs de systèmes critiques (aéronautique, aérospatial, médical, etc.) et d’autre part un nombre croissant de mathématiciens qui utilisent le numérique comme partie intégrante de leurs preuves (comme le fit par exemple Thomas Hales pour prouver la conjecture de Kepler). Les possibilités de collaborations et d’applications ne manquent donc pas ! 

Qu’avez-vous fait avant d’entrer au CNRS ? Pourquoi avoir choisi le CNRS ?

F. B. : J’ai effectué ma thèse en codirection, entre le Laboratoire de l’Informatique du Parallélisme (LIP) à l’École normale supérieure de Lyon et le Laboratoire d’Analyse et d’Architecture des Systèmes (LAAS-CNRS), une unité propre du CNRS basée à Toulouse. J’ai été merveilleusement encadré par Nicolas Brisebarre, Mioara Joldes et Damien Pous, tous les trois chercheurs au CNRS.

Ces trois années de thèse ont été l’occasion pour moi d’avoir un aperçu approfondi de la recherche au sens large. J’ai notamment eu l’occasion de séjourner au National Institute of Aerospace aux États-Unis, où les méthodes formelles sont appliquées au domaine aérospatial, ainsi que de travailler quelques mois au CNES (Centre National d’Études Spatiales) à Toulouse sur la question brûlante de la gestion des débris spatiaux en orbite autour de la Terre.

Après cela, je me suis orienté vers un post-doc à l’Université d’Uppsala en Suède sous la direction de Warwick Tucker, dans une équipe de mathématiciens réputée pour son utilisation novatrice du calcul numérique pour prouver des théorèmes en systèmes dynamiques. J’y ai appliqué mes outils à des questions reliées au seizième problème de Hilbert, qui continue de passionner les mathématiciens plus de cent ans après avoir été formulé !

Puis vint le moment de viser un poste permanent pour poursuivre mes travaux sur le long terme. Le CNRS offre une liberté inégalée dans la recherche, et le bon aperçu que j’en ai eu durant ma thèse m’a conduit naturellement à poser ma candidature au concours des chargés de recherche.

Qu’est-ce qui vous a amené à faire de l’informatique et/ou des sciences du numérique ? 

F. B. : Je ne pense pas qu’un événement particulier m’ait orienté vers la recherche. Je pense plutôt qu’il s’agit d’un certain nombre de questionnements qui m’ont toujours habité : qu’est-ce qu’une preuve acceptable ? Comment informatiser le processus de déduction logique, qui semble à la fois très « mécanique », mais aussi profondément intuitif et humain ?

À côté de cela, la pratique même des mathématiques a toujours eu pour moi ce côté stimulant, en ce qu’un théorème est prouvable à partir d’axiomes par la seule force de l’esprit, sans reposer sur des hypothèses difficilement vérifiables ou sur des expériences coûteuses. Qui plus est, il y a tellement à apprendre que cela ne laisse pas de place à l’ennui !

Je me suis progressivement orienté vers l’informatique car je suis très sensible au fait qu’un raisonnement, une preuve ou une construction puisse se traduire en un procédé de calcul effectif pour résoudre concrètement un problème. De mon point de vue, cette discipline contribue à réduire (sans pour autant en effacer le mystère) ce paradoxe évoqué plus haut entre intelligence de l’humain et intelligence de la machine.