La sémantique, c’est romantique

Piste verte 8 juin 2014  - Ecrit par  Pierre Pansu Voir les commentaires (1)

Le 22 avril 2014, c’était la journée de lancement du trimestre Sémantique des preuves et des programmes et mathématiques certifiées.

Les organisateurs Pierre-Louis Curien, Hugo Herbelin, Paul-André Melliès [1] proposent, lors de cette après-midi, une sorte de mise en bouche, une bande-annonce de ce dont il va être question jusqu’au mois de juillet à l’IHP.

JPEG - 40.6 ko
Pierre-Louis Curien

De quoi s’agit-il ? Aïe, la sémantique, ça évoque la linguistique, la logique, c’est très loin de moi, tout ça. Me voilà dans la position d’un journaliste qui s’efforce de retranscrire ce qu’il a capté de conférences bien trop savantes pour lui. Heureusement, IdM a déjà publié 2 articles sur le sujet, dont je recommande la lecture, [2], [3].

Formalisation du théorème de Feit Thompson
Pourquoi y a-t-il mathématiques certifiées dans le titre ? Justement, Georges Gonthier (Microsoft Cambridge et centre de recherche commun Inria-Microsoft) explique en quoi un théorème de mathématiques peut être certifié. Il s’agit d’apporter la démonstration que la démonstration du théorème est correcte. En théorie, c’est toujours possible, et cela peut même se faire en un temps raisonnable. Entre la théorie et la mise en pratique sur des démonstrations substantielles, il s’est écoulé plus de 50 ans. Il a fallu mettre au point ce qu’on appelle des assistants de preuve. Il s’agit de logiciels, un peu comme des langages de programmation mais spécialement conçus pour coder les différentes étapes d’une
démonstration mathématique ou d’un programme informatique. Une fois la
démonstration écrite dans un tel langage, on peut lancer un programme
qui vérifie qu’elle est correcte, c’est-à-dire que chaque énoncé intermédiaire
résulte des précédents par application des règles élémentaires du
raisonnement. Les plus connus actuellement s’appellent Agda, Coq,
HOL-Light, Isabelle et Mizar.

Par substantielle, je veux dire, une démonstration tellement longue et complexe que les spécialistes ont des doutes, de sorte que cela vaut le coup de suer pendant plusieurs années pour la certifier. Avec son équipe, Gonthier s’est d’abord attaqué au théorème des 4 couleurs, de nature combinatoire, et dont la preuve utilise lourdement l’ordinateur. Ensuite, il a choisi un sujet plus central dans les mathématiques, le

théorème de Feit Thompson

Ce théorème appartient à la théorie des groupes finis, c’est-à-dire, des symétries des figures comportant un nombre fini d’éléments, (comme les polyèdres réguliers). Il affirme que si le groupe a un nombre impair d’éléments, il est forcément résoluble, c’est-à-dire, il est construit à partir de groupes abéliens plus petits.

JPEG - 28.1 ko
Georges Gonthier

qui constitue la première grosse brique de la classification des groupes finis simples [4]. Pour ce faire, Gonthier et ses collaborateurs ont dû alimenter Coq avec les rudiments de l’algèbre, une tâche considérable, mais qui n’exigeait pas une expertise particulière en algèbre. Il y a un point sur lequel l’équipe a dû développer un bout de théorie mathématique nouvelle. La démonstration classique s’appuie sur les nombres complexes, et sur le fameux

théorème de d’Alembert-Gauss

qui affirme que tout polynôme possède au moins une racine complexe.

Cette construction incorpore une forme de raisonnement par l’absurde qui, pour des raisons historiques, n’est pas autorisée par le langage Coq. Gonthier conclut que l’assistant de preuve apporte une aide considérable au débutant qui cherche à comprendre, et que la formalisation fait progresser le sujet sur le fond.

JPEG - 33.8 ko
Hugo Herbelin et Tom Hales

Vers une formalisation de la solution de la conjecture de Kepler ?
Il semble que la formule $\frac{n(n+1)(n+2)}{6}$ pour le nombre d’oranges dans un empilement de hauteur $n$ est connue depuis plus de 2000 ans.

JPEG - 45.7 ko

Pourtant, c’est seulement en 1611, sous la plume de Johannes Kepler, qu’on voit posée la question de savoir si la disposition usuelle des oranges est la meilleure possible, c’est-à-dire qu’on met ainsi le plus d’oranges possible dans un volume donné. La réponse, positive, donnée par Tom Hales et son élève Sam Ferguson (université de Pittsburgh) en 1999 remplit un livre de 300 pages particulièrement aride, avec du logiciel pour traiter plus de 100000 configurations particulières. Bien qu’elle ait été publiée en 2006, personne n’a pu la vérifier entièrement. Depuis le début des années 2000, Hales élabore progressivement une démonstration certifiée, écrite dans le langage HOL-Light. Il a choisi ce langage en raison de sa simplicité : le coeur du logiciel tient en 3 pages, et le langage lui-même a été certifié. Le message de Hales est que, maintenant qu’on dispose d’assistants de preuve, on ne devrait plus considérer la longueur des démonstrations comme un obstacle aux avancées de l’esprit humain. C’est une belle façon de mettre fin à la querelle sur la validité des démonstrations assistées par ordinateur.

Assistants de preuve dans la recherche en informatique
Les assistants de preuve ont-ils atteint un degré de maturité qui les rend capables de satisfaire le besoin de la société pour des logiciels certifiés ? C’est-à-dire, des programmes d’ordinateurs dont on peut démontrer qu’ils font exactement ce qu’on pense qu’ils font. Dans ce domaine, il y a encore pas mal de travail à faire. En effet, c’est bien de certifier le programme. Encore faut-il que l’ordinateur sur lequel il tourne fonctionne comme on l’attend. Or il existe une batterie de tests qui vérifie l’arithmétique de base (les 4 opérations) des compilateurs. Aucun des compilateurs commercialisés ne passe la totalité des tests. La raison est que ces compilateurs incorporent d’innombrables astuces accélérant le calcul, c’est là que des erreurs ont été introduites.

JPEG - 35.2 ko
Xavier Leroy

Xavier Leroy (INRIA Rocquencourt) et ses collaborateurs ont écrit un nouveau compilateur pour microprocesseurs de la gamme x86, certifié au moyen de Coq. Il passe tous les tests avec succès. Avec 100000 lignes de code, c’est un travail considérable. Il ne faut pas s’arrêter là : les systèmes d’exploitation eux-mêmes ont besoin d’être certifiés. Une équipe australienne, NICTA, a élaboré une version certifiée d’un micro-système d’exploitation, seL4, qui conserve 80% de la puissance de l’original. Les applications industrielles du logiciel certifié ont fait l’objet d’une journée le 28 avril, mais je n’y étais pas.

JPEG - 33.6 ko
Paul-André Melliès

Fondements des mathématiques
Pour le lien entre certification et fondements des mathématiques, via la toute nouvelle théorie homotopique des types, je renvoie à l’article d’Antoine Chambert-Loir. Vladimir Voevodsky (IAS Princeton), l’un des principaux acteurs de cette théorie, nous dit où il en est. Son objectif à long terme est de bâtir des assistants de preuve que le mathématicien pourrait utiliser, non pas après coup, pour s’assurer que l’enchaînement des raisonnements est correct, mais au fur et à mesure de la création de la démonstration, comme un guide. Cela passe par une refondation formelle des mathématiques, dans laquelle les ensembles sont remplacés par les types, et un axiome d’univalence (mystérieux pour moi) joue un rôle crucial. Cette construction est en cours, certaines bibliothèques écrites en Coq, HoTT et UniMath, en exploitent déjà les idées. Une des difficultés rencontrées est la cohérence. Du point de vue mathématique, on aurait besoin de parler du $\infty$-groupoïde de tous les $\infty$-groupoïdes, qui ne peut exister. Du point de vue informatique, cette impossibilité signifie qu’il doit exister des démonstrations correctes que l’assistant de preuve ne peut vérifier (en revanche, on tient à ce que toutes les démonstrations certifiées par l’assistant de preuve soient correctes). L’opinion de Voevodsky est qu’on doit accepter l’incohérence, quitte à rechercher plusieurs niveaux de qualité pour les assistants de preuve (des versions rapides mais très peu cohérentes, des versions plus lentes mais qui parviennent à traiter davantage de démonstrations).

JPEG - 28.5 ko
Vladimir Voevodsky

Ce qui m’a frappé dans l’exposé de Voevodsky, c’est sa façon spontanée de s’adresser aux informaticiens, comme si la distance (et le décalage dans le temps) entre la conception d’une théorie très abstraite et la mise en service opérationnelle de langages de programmation qui s’en inspirent était abolie. Comme le montre la parution immédiate du livre issu de la période spéciale consacrée au sujet l’an dernier à Princeton, il semble bien que le temps s’accélère.

A quand une rubrique Images des Mathématiques Certifiées ?

La journée a été filmée, les vidéos devraient bientôt être disponibles sur le site de l’IHP.

Post-scriptum :

L’auteur remercie les relecteurs Claude Animo et Jean-Romain pour leurs critiques.

Article édité par Pierre Pansu

Notes

[1chercheurs au laboratoire PPS, CNRS et Université Paris 7

[2L’article de Jérôme Germoni

[3et celui d’Antoine Chambert-Loir

[4En rapport avec les groupes finis simples, on peut recommander le livre La symétrie ou les maths au clair de lune, de Marcus du Sautoy
Editions Héloïse d’Ormesson, 2012

Partager cet article

Pour citer cet article :

Pierre Pansu — «La sémantique, c’est romantique» — Images des Mathématiques, CNRS, 2014

Crédits image :

Image à la une - Curien/Herbelin/Melliès
affiche semantics - Curien/Herbelin/Mellies
Pierre-Louis Curien - Pansu
Georges Gonthier - Pansu
Hugo Herbelin et Tom Hales - Pansu
Xavier Leroy - Pansu
Paul-André Melliès - Pansu
Vladimir Voevodsky - Pansu

Commentaire sur l'article

  • La sémantique, c’est romantique

    le 8 juin 2014 à 08:59, par Michèle Audin

    Enfin des hommes, que des hommes, romantiques !

    Répondre à ce message

Laisser un commentaire

Forum sur abonnement

Pour participer à ce forum, vous devez vous enregistrer au préalable. Merci d’indiquer ci-dessous l’identifiant personnel qui vous a été fourni. Si vous n’êtes pas enregistré, vous devez vous inscrire.

Connexions’inscriremot de passe oublié ?

Suivre IDM