MALINCA, ou comment vérifier automatiquement les théorèmes sans avoir à les réécrire
Des scientifiques de l’Institut de recherche en informatique fondamentale (IRIF - CNRS/Université Paris Cité), du Laboratoire lorrain de recherche en informatique et ses applications (LORIA - CNRS/Université de Lorraine) et du Laboratoire Jean-Alexandre Dieudonné (LJAD - CNRS/Université Côte d’Azur) ont obtenu un financement ERC Synergy pour combler l’écart entre une démonstration mathématique et les logiciels d’assistance à la preuve. Il s’agit de permettre à ces derniers de comprendre directement des textes, par exemple d’algèbre, tels qu’on les trouve dans les ouvrages académiques.
Construire un pont linguistique entre le mathématicien et la machine, tel est le sous-titre de MALINCA. Ce projet est soutenu par une bourse du Conseil européen de la recherche ERC Synergy qui, contrairement aux financements ERC classiques, est destinée à toute une équipe de scientifiques. MALINCA vise à élargir l’usage des mathématiques vérifiées par ordinateur, en faisant notamment fonctionner divers outils de vérification et de preuves mathématiques avec le langage naturel. Une démonstration mathématique pourrait alors être directement et automatiquement vérifiée par ordinateur, sans avoir à être traduite en code. Cela aiderait à gérer le flux grandissant de publications en mathématiques qui sortent chaque mois.
Les quatre responsables de MALINCA sont Hugo Herbelin, directeur de recherche Inria à l’IRIF, Paul-André Melliès, directeur de recherche CNRS à l’IRIF, Philippe de Groote, directeur de recherche Inria au LORIA et Carlos Simpson, directeur de recherche CNRS au LJAD.
Hugo Herbelin et Paul-André Melliès travaillent dans le même laboratoire, l’IRIF, au point de rencontre entre théorie de la démonstration et étude mathématique des langages de programmation. D’un côté, Hugo Herbelin se concentre sur le transfert de concepts entre ces deux disciplines, en s’appuyant sur une correspondance importante entre preuves et programmes, dite de Curry-Howard. Il a de plus une longue expérience du développement de l’assistant à la preuve Coq, un des principaux logiciels de vérification de preuves mathématiques et qui vient tout juste de changer de nom et s’appelle désormais Rocq.
De son côté, Paul-André Melliès travaille à dégager les briques de base du raisonnement mathématique et de la programmation, au moyen d’outils provenant de la logique linéaire, de la sémantique des jeux, de la théorie des nœuds et des catégories de petite dimension. Il s’intéresse de plus aux liens entre théorie des types et théorie des automates, avec une forte curiosité pour la linguistique formelle des langues naturelles. C’est cette expertise croisée et complémentaire qui a amené Hugo Herbelin et Paul-André Melliès à concevoir le projet MALINCA aux côtés de Philippe de Groote et Carlos Simpson.
« Les outils de preuve mathématique sont capables de comprendre ce que l’on appelle le langage naturel contrôlé, où les phrases doivent rester dans un langage très simple avec quelques dizaines de mots de vocabulaire, explique Hugo Herbelin. Cela permet déjà de manipuler des définitions, des axiomes et des théorèmes, mais il faut tout de même réécrire la plupart des théorèmes et des démonstrations tels qu’on les trouve dans les articles de mathématiques et d’informatique fondamentale. Avec le projet MALINCA, nous voulons nous approcher davantage de la manière de penser et d’écrire de l’humain ».
Il y a une quinzaine d’années, une équipe réunie autour du chercheur canadien Georges Gonthier a mené un travail historique en mettant six ans à traduire deux livres de 300 pages sur le théorème de Feit-Thompson, selon lequel tout groupe fini d’ordre impair est résoluble, pour que Coq puisse les vérifier intégralement. L’équipe de MALINCA souhaite automatiser ce processus de vérification en s’appuyant sur l’idée que le code mathématique réside dans la langue naturelle. Il s’agit donc d’analyser cette langue propre aux mathématiques en utilisant des outils de linguistique formelle, en partant d’un certain nombre de textes de référence.
« Nous avons choisi de commencer par travailler avec Philippe de Groote sur le Traité d’Algèbre de Roger Godement, précise Paul-André Melliès. C’est un cours de licence bien connu, rédigé avec soin, et qui offre un point de départ idéal pour notre projet. Il contient une variété extraordinaire d’éléments linguistiques que nous voulons collecter et étudier de manière exhaustive, afin qu’ils nourrissent nos réflexions sur le fonctionnement de la langue mathématique telle qu’elle se pratique au quotidien. Cet examen linguistique des mathématiques nous apprendra beaucoup sur la nature du raisonnement et la manière de le partager et de construire un sens commun dans le langage naturel ».
Les chercheurs développeront pour cela un langage formel intermédiaire, capable de prendre en compte le discours mathématique dans sa variété de styles, et la structure d’une démonstration en langue naturelle. Pour y parvenir, les quatre porteurs du projet seront épaulés par trois chercheurs associés et pas moins de douze doctorants, dix postdoctorants et trois ingénieurs qui joindront leurs forces au projet.
« Les textes mathématiques ne sont pas seulement symboliques, ils s’inscrivent dans la langue naturelle, et possèdent une narration et des figures de style qui donnent des indications précieuses sur la manière de concevoir une définition ou une preuve, disent d’une même voix les deux chercheurs. Le choix du vocabulaire est fait avec soin et a un impact décisif sur l’imaginaire et les représentations mentales à l’œuvre dans les mathématiques. Partir du langage naturel plutôt que de la logique formelle nous permettra de conserver cette richesse et de l’interroger, avec de nouvelles formes de création et d’exploration mathématique que nous souhaitons faire émerger avec Carlos Simpson ».