Patricia Bouyer-Decitre, architecte de la fiabilité des programmes
Directrice de recherche CNRS au Laboratoire méthodes formelles (LMF - CNRS/ENS Paris-Saclay/Université Paris-Saclay), Patricia Bouyer-Decitre développe des modèles mathématiques pour garantir la fiabilité des systèmes informatiques, des plus critiques aux plus complexes. Elle est récompensée par la médaille d’argent du CNRS.
En classe préparatoire, Patricia Bouyer-Decitre se destinait aux mathématiques et ne voulait surtout pas faire d’informatique. À l’ENS Cachan, des cours intégrés à son cursus en mathématiques sèment pourtant une graine qui germe lors d’un stage au Danemark. « J’ai découvert les méthodes formelles que je ne connaissais pas du tout et ça m’a émerveillée », confie-t-elle. Un domaine dont elle ne sortira plus.
Ses recherches se situent en amont des logiciels. L’enjeu n’est pas de corriger des bugs, mais d’empêcher qu’ils existent. « Le but ultime des méthodes formelles, c’est d’augmenter la fiabilité des systèmes informatiques », explique-t-elle. Pour cela, elle construit des modèles mathématiques abstraits – des automates – et cherche à prouver qu’un programme respectera certaines propriétés. Non pas souvent, mais toujours. « On ne veut pas qu’une voiture autonome renverse rarement un piéton, mais que cela n’arrive jamais », illustre-t-elle.
Au fil de sa carrière, Patricia Bouyer-Decitre travaille avec de nombreux collaborateurs et collaboratrices, en France et à l’étranger. Cette dynamique collective n’a eu de cesse de l’encourager à faire évoluer ses modèles à mesure qu’ils atteignent leurs limites. Elle s’intéresse d’abord au temps : certaines propriétés n’ont de sens que si elles sont respectées dans un délai précis. Puis aux ressources, comme l’énergie, qu’il faut optimiser sans compromettre le fonctionnement. Elle regarde enfin l’environnement. « Un système ne fonctionne pas seul. Il faut alors intégrer l’incertitude, les interactions avec ce qui l’entoure et qui peut entraîner des comportements imprévisibles », décrit-elle.
C’est cette même logique qui la conduit vers la théorie des jeux au cœur de sa recherche depuis dix ans. Lorsque plusieurs systèmes interagissent, il ne suffit plus de vérifier un comportement isolé, mais de raisonner en termes de stratégies. Chaque agent agit en fonction des autres. En méthodes formelles, une stratégie gagnante est un contrôleur : un programme capable de prendre la bonne décision et de garantir l’atteinte d’un objectif précis, quoi qu’il arrive.
Ces travaux rejoignent aujourd’hui une question centrale d’un pan de l’intelligence artificielle : comment s’assurer qu’un système prend de bonnes décisions et surtout, comment l’expliquer ? Les méthodes formelles qu’elle développe permettent de construire des stratégies dotées de propriétés formellement prouvées et recherchées par ceux qui construisent des IA explicables.
Tout au long de sa carrière, Patricia Bouyer-Decitre a poursuivi une même exigence : « Bien que mes recherches soient très en amont, il y a toujours un lien avec des problèmes concrets. Et en vingt-cinq ans de carrière, je ne me suis jamais épuisée à aller l’explorer ».