Les méthodes formelles ont le vent en poupe dans le domaine des assistants de preuve chargés de vérifier l’exactitude des logiciels. En revanche, il existe peu d’outils permettant aux mathématiciens de prouver des théorèmes à l’aide du calcul formel, aussi appelé calcul symbolique. Membre de l’équipe de recherche Gallinette* à Nantes, Assia Mahboubi vient de recevoir une bourse du Conseil européen de la recherche (ERC) pour faire évoluer les techniques de formalisation dans cette discipline. À la clé : une fiabilité mieux balisée.
Aviation. Nucléaire. Automobile… Dans les systèmes critiques, le bug est un danger. Pour le traquer, le développeur soumet son logiciel à des batteries de tests. Mais pour avoir une garantie ultime, il peut aller encore plus loin : vérifier formellement l’exactitude du programme. Il utilise alors ce que l’on appelle un assistant de preuve. Depuis 20 ans, ces outils enregistrent d’énormes progrès. Ils deviennent également plus faciles à utiliser et se répandent dans l’industrie. Créé en 1984 par Inria, Coq est l’un des plus connus et aussi l’un des plus performants au niveau mondial*.
Mais les méthodes formelles ne servent pas qu’à vérifier des programmes. Elles permettent aussi aux mathématiciens de prouver des théorèmes à l’aide de l’ordinateur. C’est le cas en particulier quand la masse de calculs impliqués devient hors de portée pour l’être humain. Là encore, les assistants de preuve peuvent alors vérifier ces calculs. Ainsi, en 2004, à l’aide de Coq, deux chercheurs ont prouvé formellement le théorème des quatre couleurs. Il s’agissait d’une preuve calculatoire pour laquelle la puissance de la machine était donc nécessaire.
Petit bémol cependant : les outils à la disposition des mathématiciens n’ont pas évolué à la même vitesse que ceux des programmeurs.
Assïa Mahboubi, chercheuse membre de l’équipe Gallinette
Dans les laboratoires, aujourd’hui, beaucoup de mathématiciens utilisent du calcul pour tester leurs conjectures, visualiser des phénomènes ou faire des démonstrations. Ils prennent un objet mathématique puis effectuent dessus un calcul à l’aide de la machine. Or, si dans l’aéronautique par exemple, on a quantité de méthodes formelles pour garantir les propriétés de correction sur ce qui se passe, et bien pour les programmes utilisés par les chercheurs en maths, il n’y a… quasiment rien. C’est un peu perturbant car c’est justement l’endroit où l’on s’attendrait à voir des outils formellement vérifiés.
Bornes de confiance
Cette absence entraîne un risque de dérapage calculatoire. Exemple : “quand le mathématicien effectue un calcul, son logiciel ne fournit pas forcément des résultats, ou même des bornes de confiances correctes. Le problème n’est pas tant que son outil puisse se tromper, mais plutôt qu’il n’envoie aucun message pour dire qu’il n’est pas certain de lui. Par ailleurs, les auteurs de ce logiciel, eux, ne considèrent pas forcément cela comme un bug. Ils peuvent juste voir ces problèmes comme un cas particulier qui sort du domaine d’utilisation. Ils peuvent alors simplement retirer ce cas de figure du périmètre de support. On se retrouve donc avec des programmes conçus pour être efficaces dans leur domaine de compétence. Mais c’est très difficile de documenter le cadre dans lequel, tout en restant efficaces, ils demeurent également fiables.”
Repenser l’architecture
Financé par l’ERC à hauteur de 2 millions d’euros, le projet de recherche s’appelle Fresco (Fast and Reliable Symbolic Computation). Débuté en novembre dernier, il va durer cinq ans. “Nous devons repartir du début et repenser l’architecture du logiciel de calcul utilisé par le mathématicien. Il va y avoir une phase mathématique où il faudra décrire les opérations de haut niveau, comme celles que l’on décrit dans les publications mathématiques. Pour ce faire, nous allons utiliser Coq. L’outil est bien adapté pour ce travail. Dans une deuxième phase, nous souhaitons nous interfacer avec les bibliothèques spécialisées de plus bas niveau, qui visent à l’efficacité. Cet interfaçage va nous amener à écrire un nouveau langage.”
À noter au passage que les progrès escomptés pourraient aussi engendrer indirectement des retombées industrielles. “En sécurité, par exemple, la vérification formelle permet de valider des composants de cryptologie. Difficile de faire cela avec autre chose qu’un logiciel qui parle de mathématiques.”
This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 101001995)
|
