Le sens mathématique de l’informatique

L’IRIF (Institut de recherche en informatique fondamentale) transforme programmes informatiques en démonstrations mathématiques : un moyen efficace de s’assurer qu’ils ne contiennent aucune erreur. Son expertise, reconnue internationalement, pourrait un jour permettre d’améliorer également le "machine learning".

L’accident mortel survenu en Arizona le 19 mars dernier incite plus que jamais à la prudence. « Les voitures autonomes ont un taux d’erreur très faible… mais il est quand même possible de les tromper : une simple feuille de papier peut leur faire prendre un « Stop » pour un autre panneau par exemple », illustre Yann Régis Gianas, chercheur en informatique à l’Institut de recherche en informatique fondamentale (IRIF). "Or dans ces systèmes, la fiabilité de l’intelligence artificielle est critique, c’est-à-dire que la vie humaine en dépend." La question qui se pose est donc de savoir comment rendre ces programmes sans erreur en toutes situations ? La réponse selon l’IRIF sera de donner du sens mathématique à l’informatique.

L’obstacle du machine learning

« N’importe quel programme peut être transformé en une démonstration mathématique, explique le chercheur. Or ces démonstrations s’appuient sur des théorèmes dont les preuves sont construites et vérifiés sur ordinateur, ce qui garantit un programme sans erreur. » L’IRIF, en partenariat avec l’Inria, dispose justement d’une expertise reconnue internationalement dans le domaine grâce au logiciel COQ, lauréat du ACM Software System Award en 2013. Celui-ci permet en effet de s’assurer mathématiquement qu’il n’existe pas d’erreur dans un programme. « Cependant, personne n’a pour le moment réussi à prouver mathématiquement un algorithme de machine learning », rappelle Yann Régis Gianas. L’IRIF y travaille…