La vie est mal configurée

Depuis quelques années, une partie de mes recherches porte sur la compilation certifiée, qui s’inscrit dans un but plus global de produire des logiciels dont la fiabilité puisse être justifiée pour des applications critiques (aviation, ferroviaire…). On m’a suggéré d’expliquer ce dont il s’agit.

Les développeurs de logiciels rédigent ceux-ci dans un ou plusieurs langages de programmation, en général textuels (d’où le « code » effrayant que l’on montre parfois lorsque l’on évoque ce sujet dans les médias), parfois graphiques. Le programme ainsi rédigé n’est pas directement exécutable par la machine, dont la circuiterie ne sait exécuter que des opérations très simples (une addition, un déplacement de données…). Il faut donc une étape de traduction. On distinguait naguère pour celle-ci les interpréteurs (qui traduisent les instructions au fur et à mesure) et les compilateurs (qui traduisent le programme une fois pour toutes), mais les frontières sont maintenant floues. Toujours est-il qu’on traduit, et que comme pour toute traduction, celle-ci peut être fidèle ou infidèle. Et une traduction infidèle, pour un logiciel, peut conduire à des bugs.

Remarquons le caractère particulièrement vicieux de cette infidélité. Le logiciel tel que développé peut très bien être correct, mais la phase de traduction rajouter des bugs qui ne se verront pas dans le texte du logiciel. Comme la phase de traduction est influencée par de très nombreux facteurs, il est possible que les bugs ne soient introduits que dans certaines circonstances (par exemple, seulement dans la version de production destinée aux utilisateurs) et pas dans d’autres (par exemple, dans la version instrumentée pour faire des tests).

Dans la plupart des applications, il y a bien d’autres sources de bugs que les compilateurs. Lorsque l’on parle d’applications critiques, où il faut justifier que le programme exécuté met bien en œuvre les fonctionnalités qu’il est censé mettre en œuvre, la question est différente. On peut utiliser des arguments tels que « ce compilateur a été utilisé pour de nombreuses applications critiques et on n’a pas constaté de problèmes », on peut organiser des relectures partielles de la correspondance entre le logiciel tel que rédigé et celui exécuté par la machine, mais il s’agit là de solutions très partielles. En effet, ce n’est pas parce qu’un compilateur n’a pas eu de comportement incorrect détectable sur d’autres applications qu’il n’en aura pas sur une application donnée. Quant aux relectures, elles exigent souvent qu’on demande au compilateur de faire une traduction « mot à mot » qui produit du code inefficace pour la machine.

Il faut ici évoquer la notion d’optimisation. Pour un programme rédigé par un humain donné, il existe de multiples façon de le traduire fidèlement en un programme exécutable sur la machine, fidèles au sens que le sens (on dit : la sémantique) du programme est préservé. Pourtant, toutes ne se valent pas : certaines vont mettre plus de temps que d’autres pour s’exécuter. Un compilateur optimisant va donc transformer le programme, faire une traduction moins littérale, afin de produire du code efficace. Je ne vais pas rentrer dans le détail de toutes les optimisations possibles, mais en voici quelques-unes :

1. Le programmeur a pu mettre un calcul qui se répète de façon inutile, parce qu’à chaque fois il donne le même résultat. On peut calculer celui-ci une fois pour toutes. (Le programmeur pourrait faire cette transformation lui-même, mais parfois, pour des raisons de lisibilité, ce n’est pas souhaitable.)

2. L’ordre d’exécution n’est pas forcément optimal. J’ai parlé d’opérations pour déplacer des données ; ces opérations prennent un certain temps et il vaut mieux l’anticiper. C’est un peu comme dans une bibliothèque où il faut commander des documents : si l’on a besoin de 3 documents pour travailler successivement sur chacun d’entre eux, il est plus rapide deême commander les 3 documents en une fois, plutôt que de ne commander que le premier, l’attendre, travailler dessus, le rendre, commander le suivant… Les gros processeurs pour PC ou Mac ont donc dans leur électronique des dispositifs leur permettant d’exécuter les instructions dans le désordre, et lanceront les trois commandes de données en avance ; mais ces dispositifs d’exécution dans le désordre sont complexes, parfois eux-mêmes buggués, et on les évite dans les systèmes critiques. Un compilateur optimisant va donc placer les opérations de façon à anticiper les délais d’attente.

Un compilateur optimisant est un logiciel complexe, il va donc contenir des bugs donc potentiellement introduire des bugs dans les programmes qu’il traduit ; mais sans optimisation, il va produire des programmes inefficaces, ce qui est intolérable dans de nombreuses applications.

La solution proposée par Xavier Leroy (alors directeur de recherche à l’INRIA, maintenant professeur au Collège de France) et ses collaboratrices et collaborateurs a été de démontrer mathématiquement la correction de leur compilateur CompCert.

Il convient ici de préciser certaines idées. Un compilateur est une sorte de traducteur dont on exige la fidélité, c’est-à-dire la préservation du sens du programme. Ce sens peut être défini mathématiquement, tant pour le langage de programmation manipulé par le programmeur que pour les instructions exécutables directement par la machine. Les transformations effectuées par le compilateur peuvent elles aussi être définies sous une forme mathématique. Il « suffit » alors de démontrer un théorème de préservation.

Il serait très difficile, voire impossible, de démontrer à la main (avec du papier et des crayons) un tel théorème, tant un compilateur est complexe, et évolue d’une version à l’autre. Qui plus est, les preuves à la main sont elles-mêmes sujettes à bugs — divers algorithmes de la littérature scientifique, où était publiées des démonstrations de leur correction, se sont révélés in fine incorrects. Aussi la preuve mathématique sera elle-même vérifiée par un logiciel, un assistant de preuve ; dans le cas de CompCert, il s’agit de l’assistant Coq.

La nécessité de justifier minutieusement la fidélité de chaque étape de traduction rend CompCert assez différent d’un compilateur traditionnel ; par exemple, il vaut mieux plusieurs étapes simples qu’une grosse étape complexe. L’effort de preuve est considérable, et on structure le logiciel par rapport à celui-ci : est-il rentable d’implanter une optimisation difficile à justifier rigoureusement si celle-ci ne gagne en général pas grand-chose en efficacité ?

Il faut ici relever que les preuves à rédiger sont considérablement plus délicates et minutieuses que celles que l’on donne dans les publications scientifiques en ce qui concerne les algorithmes d’optimisation. En effet, dans les preuves sur papier, on peut se permettre d’omettre certains « détails » fastidieux et s’en tenir aux grands principes ; ce n’est pas le cas ici (et heureusement, car parfois l’erreur est dans le détail fastidieux).

Depuis près de deux ans, Sylvain Boulmé, moi-même et notre doctorant Cyril Six travaillons à l’ajout d’optimisations dans CompCert, notamment afin d’adapter ce compilateur à des processeurs sans exécution dans le désordre, et en premier lieu le MPPA3 de la société Kalray.

Nous appliquons en cela une idée que nous avons mise en œuvre depuis des années dans d’autres contextes (calcul sur les polyèdres convexes, test de satisfaisabilité booléenne…) et d’ailleurs déjà mise en œuvre dans CompCert (allocation de registres) : nous décomposons notre optimisation en un oracle (un morceau de programme qui fournit un résultat sans qu’on n’ait à démontrer quoi que ce soit sur la correction de ce résultat) et un vérificateur (qui vérifie que ce qui a été fourni par l’oracle était correct), et nous ne démontrons formellement que la correction du vérificateur. Ceci offre plusieurs avantages :

1. Il est plus simple de démontrer que le vérificateur ne se trompe jamais que de démontrer que l’oracle va toujours produire une solution correcte. (Dans certains cas l’oracle met en jeu un algorithme de recherche complexe ; dans d’autres, l’argument de correction est global, tandis que la vérification de correction peut se faire localement.)

2. On peut parfois changer l’oracle sans changer le vérificateur.

3. Le même vérificateur peut parfois servir à plusieurs optimisations.

Nous utilisons notamment des vérificateurs qui vont symboliquement exécuter des fragments de programme et s’assurer que la traduction est fidèle en constatant qu’in fine les deux fragments de programme calculent la même chose.

Le problème scientifique derrière tout cela est : quelles définitions, quels invariants poser pour justifier la correction de ces transformations ? La preuve formelle nous oblige à affiner les concepts. On peut s’apercevoir que certaines hypothèses traditionnellement utilisées sont en fait inutiles (comme par exemple dans mon travail sur les opérateurs d’élargissement), ou que certains concepts sont en fait mal définis…

Quelle différence y a-t-il entre l’enseignement et la recherche en mathématiques ? Bien évidemment, il y a une différence de degré d’abstraction et de technicité entre l’enseignement, a fortiori secondaire, et la recherche. Je pense toutefois que la différence la plus importante est que lorsque l’on est élève, on sait ce que l’on doit faire, alors qu’en recherche, non.

Lorsqu’un·e enseignant·e pose un problème de mathématiques, il ou elle a en tête une façon de le résoudre en n’utilisant que les connaissances que l’étudiant·e est censé·e avoir à ce moment, et la décompose en étapes telles que chacune soit faisable sans trop de questionnements. C’est ce qui permet de poser en travaux dirigés, voire en examen, ce qui a jadis été une question de recherche. Par exemple, j’ai une feuille de travaux dirigés presque faisable en deux heures pour de bons étudiants où l’on démontre le théorème de complétude de la logique du premier ordre, lequel constituait pourtant la thèse de doctorat du célébrissime logicien Kurt Gödel.

À l’opposé, en recherche (à tout niveau), on ne sait en général pas si le résultat que l’on compte prouver est vrai, puisque c’est la démonstration que l’on cherche qui établirait cette vérité (il arrive toutefois que l’on cherche à redémontrer un théorème par une autre méthode, ce qui peut être instructif). Bien entendu, on ne va pas à l’aveuglette, on est guidé par des indices : par exemple, si des calculs numériques (approximés) semblent indiquer qu’une quantité est nulle, il est raisonnable d’essayer de le démontrer. Il est cependant périlleux de conclure que parce qu’une chose semble vraie elle l’est forcément, et plusieurs conjectures qui semblaient raisonnables ont été par la suite démontrées fausses.

Plus profondément, le mathématicien en recherche non seulement ne sait pas si le résultat qu’il cherche à démontrer est vrai ou faux, mais doit en premier lieu poser les bonnes questions, les bonnes définitions. Il ne s’agit donc pas simplement de réaliser un « tour de force » en démontrant un résultat, mais surtout de construire un édifice conceptuel (que l’on nomme souvent théorie : théorie des distributions de Laurent Schwartz, théorie de Ramsey, etc.). Pour ma part, je n’en suis pas là : je démontre modestement des petits résultats.

Quelques exemples de ce phénomène en action. Il y a quelques années, je m’étais demandé si la raison pour laquelle on avait proposé tant de méthodes partielles pour inférer ce que l’on appelle des invariants inductifs polyédraux n’était pas qu’il ne peut exister de méthode algorithmique totale. Ce problème traînait dans mon esprit. J’ai démontré un résultat plus faible que celui que j’aurais voulu ; mais peut-être est-ce que parce que le résultat plus fort serait faux ? Je n’en sais rien ! J’ai interrogé des collègues (Olivier m’a dit de demander à Joël, Joël m’a dit de demander à Olivier, etc.) ; personne ne savait comment prendre la question. De guerre lasse, plusieurs années plus tard, j’ai fini par publier mon résultat trop faible à mon goût.

Actuellement, Valentin Touzeau, doctorant, et moi-même tentons de démontrer des résultats sur la complexité de certains problèmes, c’est-à-dire leur degré de difficulté lorsqu’il s’agit de les résoudre par un algorithme (je simplifie). Avant de nous lancer là-dedans, nous ne savions pas quels résultats nous pourrions prouver (si ce n’est quelques bornes larges et évidentes pour qui connaît ce genre de questions). J’ai pu prouver qu’un des problèmes en question est NP-complet (c’est une des classes de complexité), et Valentin me dit qu’il a une idée pour montrer qu’un autre de ces problèmes est PSPACE-complet (c’est une autre classe). Je suis très excité par cette perspective, mais je reste prudent : nous ne devons pas crier victoire tant que nous n’avons pas une preuve rédigée au propre !

Si je suis excité, c’est parce que le résultat ainsi démontré correspondrait à une intuition souvent citée par les gens qui proposent des algorithmes pour résoudre partiellement les problèmes en question pour expliquer pourquoi le second est plus difficile que le premier. Mais je n'en sais toujours rien.

On sait qu’un polyèdre convexe borné peut s’exprimer aussi bien comme l’enveloppe convexe V d’une famille de points que comme l’intersection H d’une famille finie de demi-espaces. On peut donc vouloir vérifier que deux telles représentations sont équivalentes.

On montre facilement que ce problème est dans co-NP :

1. L’inclusion V ⊆ H se vérifie aisément (produit de matrices).

2. H ⊊ V si et seulement si il existe un sommet de H (choix non déterministe sur les contraintes à intersecter) qui sort de V (test par programmation linéaire sur les coordonnées barycentriques).

Apparemment, la complexité de ce problème est inconnue ! Pas d’algorithme polynomial connu, pas de preuve de complétude…

PS L'algorithme suivant (pour polyèdres bornés) ne fonctionne pas :

1. On minimise les représentations sommets et contraintes (un appel de programmation linéaire pour chaque sommet ou contrainte par rapport aux autres, soit temps polynomial).
2. On vérifie l'inclusion des sommets dans les contraintes (produit de matrices).
3. On vérifie que chaque contrainte sature au moins d sommets et chaque sommet au moins d contraintes et qu'aucune contrainte (resp. sommet) ne sature un sur-ensemble des sommets (resp. contraintes) saturés par une autre contrainte (resp. sommet).

La presse s'est faite l'écho de la publication de « la plus longue preuve des mathématiques » — attention surprenante pour un domaine, la preuve mathématique formelle assistée par ordinateur, qui n'est pas franchement grand public. Il se trouve que j'assistais à la conférence où résultat a été présenté ; j'aimerais ici en donner un résumé accessible et quelques commentaires.

Un public plus averti pourra se rapporter à l'article de recherche publié aux actes de la conférence ; mentionnons aussi la page « everything's bigger in Texas » où les auteurs ont rassemblé diverses informations et articles de presse.

Le problème du coloriage des triplets de Pythagore

Le problème qui se posait est de savoir si l'on peut colorer (disons, en bleu ou en rouge) les nombres entiers en respectant certaines règles. Par exemple, on peut imposer qu'on ne peut colorer de la même couleur les nombres 3, 4 et 5, au motif qu'il s'agit d'un « triplet de Pythagore » : 5 est la longueur du plus long côté d'un triangle rectangle dont les deux autres côtés sont de longueur 3 et 4. En d'autres termes, si on prend a=3, b=4, c=5 alors on a la relation a²+b²=c². On va s'interdire de colorer de la même couleur les triplets de Pythagore, et on va tenter de colorier les entiers 1, 2, 3… en respectant ces règles. La question est alors de savoir jusqu'à quel entier on va pouvoir colorier, ou en d'autres termes jusqu'où on pourra aller jusqu'à rencontrer une impossibilité. Bref, il s'agit de savoir à partir de quand on sera forcé d'avoir un triplet de Pythagore d'une seule couleur.

(Petite parenthèse. Je n'ai pas la moindre idée de pourquoi les gens s'intéressent à ce problème, s'il sert à quelque chose, s'il a des ramification ailleurs en mathématiques. Voir à la fin de l'article pour plus de discussion sur l'impact et la position de ce résultat.)

La force brutale ?

Une approche « par la force brutale » serait d'énumérer tous les cas de coloriage. Par exemple, si on essaye de colorier tous les entiers de 1 à 5, alors on a deux choix (bleu ou rouge)pour 1, deux choix pour 2, deux choix pour 3, deux choix pour 4, deux choix pour 5, et donc 2×2×2×2×2, soit 32, choix au total. Si on avait voulu colorier de 1 à 16, on aurait eu 2×2×2×2×2×2×2×2×2×2×2×2×2×2×2×2, soit 65 536, choix au total. Et pour 1 à 40, on aurait 1 099 511 627 776 possibilités. Le nombre de combinaisons croît vertigineusement !

Oh, certes, on peut y faire quelque chose. Un constat : si on a un coloriage en bleu et rouge, alors on en obtient un autre « opposé » en intervertissant le bleu et le rouge. On peut donc s'économiser un peu de travail en décidant qu'un nombre (par exemple 42) sera coloré en bleu, puisque s'il existe une solution où il est coloré en rouge, alors il existe la solution « opposée » où il est coloré en bleu. Ceci ne nous change cependant pas la vie, car il y a toujours un nombre vertigineux de combinaisons.

(Petite parenthèse de vocabulaire. Le nombre de coloriages possibles des entiers de 1 à n c'est 2×…×2 n fois, c'est-à-dire « 2 puissance n », noté 2ⁿ. On dit aussi « 2 exposant n », d'où le terme de « croissance exponentielle ». On entend parfois dans les médias ce terme appliqué à toute croissance rapide, mais le sens mathématique est celui que j'explique ici.)

En l’occurrence, les chercheurs cités on démontré que l'on peut colorier les nombres de 1 à 7824 avec deux couleurs de façon à ce qu'aucun triplet de Pythagore ne soit colorié d'une seule couleur, mais que cela est impossible pour 7825. Il est clair qu'il ne peut s'agir d'une preuve par la seule force brute : en effet, il faudrait alors énumérer 2⁷⁸²⁵ combinaisons, soit un nombre à 2356 chiffres. Même en employant tous les ordinateurs disponibles actuellement pendant un temps égal à l'âge de l'Univers, on est très, très loin du compte. Pareil nombre pourrait paraître « astronomique » mais est même au-delà de tout ce que l'on peut envisager dans le monde astrophysique…

Un peu plus astucieux

On peut tenter d'être plus adroit. Si l'on sait, par exemple, que l'on doit colorier 3 et 4 en bleu, alors on peut immédiatement en conclure que 5 doit être coloré en rouge. On peut ainsi propager facilement des informations… un peu comme le joueur de Sudoku qui dit « la seule possibilité pour cette case, vu les cases déjà remplies, c'est de valoir 7, mais alors je sais que cette autre case doit valoir 8… ».

Toutefois, comme le savent les joueurs de Sudoku qui s'attaquent aux grilles « difficiles », cette propagation simple ne suffit pas. Il est parfois nécessaire de faire une hypothèse (« cette case peut être 5 ou 6, alors j'essaye 5 »), et de travailler ensuite sous celle-ci. On peut alors aboutir à une contradiction : une case pourrait n'avoir aucune valeur possible ! Il faut alors rétracter l'hypothèse faite (« comme ce ne peut pas être 5, j'essaye 6 »). Dans le problème du coloriage, on va donc être amené, lorsque la simple propagation ne suffit pas, à décider d'essayer qu'un nombre soit bleu, et si on aboutit à un conflit (une propagation conclut qu'un nombre doit être colorié en bleu et une autre propagation conclut que le même nombre doit être colorié en rouge) on se dit qu'on aurait dû choisir le rouge.

On explore ainsi une sorte d'arbre de choix : de la racine partent deux branches correspondant au premier choix (p.ex. branche de gauche, « 5 est colorié en bleu », branche de droite « 5 est colorié en rouge »), puis dans la première branche on trouve deux sous-branches (p.ex. branche de gauche, « 7 est colorié en bleu », branche de droite « 7 est colorié en rouge »), dans la deuxième deux sous-branches (p.ex. branche de gauche, « 8 est colorié en bleu », branche de droite « 8 est colorié en rouge »).

Ce que je viens de décrire est l'algorithme de Davis, Putnam, Logemann & Loveland (DPLL) (par algorithme, on entend « description d'un procédé de calcul automatique »). Mais il y a mieux !

L'apprentissage

Imaginons qu'il soit impossible d'avoir à la fois 47 et 49 en rouge et 70 et 5 en bleu. Cette règle n'apparaît pas dans les règles données initialement, qui ne parlent que de triplets de Pythagore, mais en est une conséquence. Malheureusement, l'algorithme DPLL ne s'en rendra pas compte, et pourra essayer plusieurs fois des combinaisons du style « 4, 47 et 49 en rouge et 99, 70 et 5 en bleu » ou « 3, 47 et 49 en rouge et 122, 70 et 5 en bleu ».

L'algorithme DPLL rétracte sa dernière hypothèse lorsqu'il rencontre un conflit. Ce conflit peut être analysé : « si je voulais colorier 84 en rouge, c'est parce que j'ai une règle qui dit que je n'ai pas le droit de colorier le triplet de Pythagore 80, 84 et 116 de la même couleur, or j'ai déjà colorié 80 et 116 en bleu ; j'ai colorié 80 en bleu parce que j'avais fait l'hypothèse que 60 et 100 étaient rouges, or 60, 80 et 100 forment un triplet de Pythagore ; et j'ai fait l'hypothèse que 116 était bleu. Par ailleurs, j'avais fait l'hypothèse que 84 était bleu. ». Ainsi, on est arrivé au conflit en raison des hypothèses « 84, 116 sont bleus, 60 et 100 sont rouges ». On peut donc apprendre une nouvelle règle : on ne peut jamais avoir à la fois 84 et 116 en bleu, 60 et 100 en rouge. Cette règle n'était pas initialement connue, mais je l'ai obtenue en analysant un conflit.

Ici, nous avons appris une règle supplémentaire à partir seulement de quelques étapes de raisonnement, mais en général, on peut ainsi déduire des règles qui « résument » une exploration assez fastidieuse, qu'on n'aura donc pas à refaire par la suite. Ici, une fois cette règle connue, on sait, une fois avoir sélectionné 84 en bleu, 116 en bleu, 60 en rouge, que 100 doit être bleu.

Ceci est la base de l'algorithme conflict-driven clause learning (CDCL). Je n'ai d'ailleurs pas évoqué diverses subtilités, comme par exemple comment éviter d'avoir à rechercher dans toutes la listes de règles celles qu'il faut considérer…

Je n'ai pas non plus évoqué comment les auteurs de l'article cité ont décomposé leur problème d'origine en un million de sous-problèmes, chacun résolu par CDCL, et comment ils ont réparti le million de problèmes sur 800 unités de calcul (ils travaillaient sur un super-calculateur composé de milliers d'unités de calcul, dont ils n'avaient loué que 800).

La preuve

On peut objecter qu'une telle preuve « par ordinateur » n'a guère de valeur, parce que le logiciel utilisé peut contenir des bugs.

Sur l'aspect « il est possible de colorier jusqu'à 7824 », il n'y a pas de problème. En effet, le logiciel, lorsqu'il répond positivement, produit le coloriage, qu'il est alors très aisé de vérifier.

Le problème est sur « il est impossible de colorier jusqu'à 7825 ». En effet, a priori, la correction de cette réponse repose sur le fonctionnement d'un logiciel très complexe. Il arrive que des logiciels mathématiques donnent des réponses fausses ou douteuses ; par exemple j'ai eu affaire à des logiciels qui, suivant leur version et la façon dont le même problème était présenté, répondaient « vrai » ou « faux ». On peut difficilement croire sur parole un logiciel qui se contente de répondre « il n'y a pas de solution ».

C'est là qu'intervient la fameuse « plus grosse preuve des mathématiques ». En effet, l'outil utilisé note les étapes de déduction qu'il effectue. Il produit ainsi une preuve (certes très longue, encore qu'on puisse la simplifier et la compacter) que l'on peut vérifier avec un logiciel indépendant. Il semblerait assez improbable que le logiciel ayant rédigé la preuve et le logiciel de relecture (voire les logiciels de relecture) aient tous des bugs qui laissent passer cette preuve, si elle était incorrecte, tandis qu'ils ont été abondamment testés par ailleurs.

Futile ?

On peut se dire que colorier des triplets de Pythagore est bien futile. En réalité, savoir « colorier » de deux couleurs suivant des règles d'incompatibilité, c'est extrêmement utile industriellement, car cela sert notamment à la recherche de bugs dans des circuits électroniques. Un « coloriage » réussi correspond alors typiquement à des valeurs électriques dans le circuit qui font que celui-ci produit un comportement indésirable. On dit souvent qu'un bug dans un circuit découvert uniquement après réalisation d'un prototype matériel coûte de l'ordre d'un million d'euros ; et un bug découvert après livraisons chez les consommateurs peut coûter largement plus (la société Intel, en 1995, avait dû organiser un rappel de microprocesseurs défectueux au coût de 475 millions de dollars des États-Unis).

Le tour de force des chercheurs ici a été non pas de développer un nouvel algorithme ou nouveau logiciel (encore qu'il y a eu certainement des développements spécifiques liés au découpage en un million de sous-problèmes), mais de tout mettre en œuvre pour résoudre un problème mathématique existant. On pourra objecter qu'il s'agit alors d’ingénierie ou du moins de recherche technologique et non de recherche scientifique.

Est-ce que cela en valait la peine ? Des mathématiciens comme Timothy Gowers objectent que, certes, on a une preuve d'impossibilité de coloriage en deux couleurs pour 7825, mais que cette preuve ne nous apprend rien sur le problème mathématique sous-jacent. Une vision naïve des mathématiques est que les mathématiciens cherchent à démontrer des théorèmes et que ce sont ceux-ci qui sont le but final, comme une sorte de grand prix. En réalité, avec la recherche de la preuve d'un grand théorème vient toute une réflexion, une compréhension, une théorisation ; pour reprendre une analogie assez cliché, ce n'est pas le but final qui fait l'intérêt du voyage, mais le trajet. De ce point de vue, la « grosse preuve » évoquée est assez pauvre : la produire n'a nécessité aucune compréhension de la structure des triplets de Pythagore.

Bien entendu, on peut rappeler que l'objectif posé par le président Kennedy d'aller sur la Lune, peut-être futile voire puéril en lui-même (allons-y pour montrer qu'on est plus fort que les Russkis !), a eu de nombreuses retombées technologiques, qui ne seraient peut-être pas arrivées, ou du moins pas aussi vite, s'il n'y avait pas fallu répondre au défi. Un défi peut lui aussi être intéressant non tant par son objectif final que parce qu'il a fallu réfléchir à comment le surmonter.

De ce point de vue, on pourra objecter que ni les approches ni les outils logiciels mis en œuvre n'étaient vraiment nouveaux pour cette preuve. Le logiciel CDCL utilisé, Glucose, de Laurent Simon (professeur à Bordeaux-INP) et Gilles Audemard (professeur à l'Université d'Artois), préexistait ; celui-ci met en œuvre plusieurs décennies d'idées et d'algorithmes dans le domaine de la satisfiabilité propositionnelle. L'approche cube-and-conquer de division en millions de sous-problèmes préexistait également.

Je pense cependant qu'avoir un résultat défi, identifié, visible, et qui parle aux mathématiciens professionnels, est une bonne chose pour la communication entre domaines scientifiques (je suppose que l'immense majorité des mathématiciens n'ont jamais entendu parler de preuve automatique, ou ont de fausses idées dessus ; encore que ce soit moins vrai de nos jours). Par ailleurs, du point de vue des mathématiciens, il est utile de savoir si un théorème est vrai ou faux avant de tenter d'en chercher une preuve élégante.

La couverture médiatique

Il est inhabituel qu'un résultat assez technique de mathématiques ou d'informatique sorte dans les médias grand public. Il semble qu'ici, l'origine de cette attention ait été un article dans la partie magazine de la revue Nature. J'ignore pourquoi Nature s'est penché sur le sujet (un communiqué des auteurs ? du service communication de leur université ?). Le Journal du CNRS a, avec un certain retard il est vrai, lui aussi évoqué le sujet, puis l'AFP et les médias qui suivent l'AFP. On a ici une illustration du suivisme des journalistes, qui parlent d'une chose parce que d'autres en ont parlé.

Ce qui, semble-t-il, a marqué les esprits, c'est qu'il s'agisse de « la plus grosse » ou « la plus longue » preuve des mathématiques. On pourra ironiser sur l'aspect « c'est moi qui a la plus grosse » de ces titres. On pourra également rappeler comment Richard Feynman se moquait de ces journalistes qui, pour évoquer une expérience de physique des particules, se concentraient sur un détail comme le fait que l'appareillage expérimental pesait 7 tonnes plutôt que sur le fond scientifique. Bref, ici, c'est le « record » qui est le motif.

Certains médias français ont évoqué « un algorithme de conception française » au sujet du logiciel Glucose (passons sur la différence à faire entre logiciel et algorithme). L'aspect « bien que cela ait été fait en Amérique, le fond est français » est important, un peu comme on souligne que telle ou telle région vinicole dont son succès en partie à l'expertise française exportée.

La théorie

J'ai dit l'importance des problèmes de « coloriage » (en réalité, des problèmes de satisfiabilité propositionnelle) pour l'industrie. Ces problèmes sont également très importants à titre théorique.

On l'a vu, la méthode naïve pour les résoudre consiste à énumérer un nombre exponentiel de possibilités. Les méthodes que j'ai évoqué plus bas (DPLL, CDCL) ne font pas mieux dans le pire cas. Une question légitime est donc de savoir si l'on pourrait trouver une méthode dont la croissance du coût du calcul avec la taille du problème soit seulement polynomiale (je ne définirai pas ce terme ici, mais, d'une certaine façon, ça croît bien moins vite qu'un exponentielle) — ou, à l'inverse, si l'on pourrait démontrer mathématiquement que cela est impossible. Cette question n'a pour le moment pas de réponse. On conjecture qu'il n'y a pas de méthode polynomiale, mais on ne sait pas le démontrer.

Cette question, aussi connue sous le nom de « P=NP ? » est considérée comme un problème central en informatique théorique. L'Institut Clay l'a listé parmi une liste de sept grand problèmes mathématiques « du millénaire », chacun doté d'un prix d'un million de dollars.

Le problème de la satisfiabilité propositionnelle est particulièrement important parce qu'un très grand nombre de problèmes lui ont été démontrés comme étant équivalents en un certain sens — si l'on trouve un algorithme polynomial pour l'un, alors il existe un algorithme polynomial pour les autres, et vice-versa. On peut dire (même si cette formulation est très discutable et doit être prise avec un grand de sel) qu'il s'agit de séparer ce qui est infaisable dans le pire cas, car trop coûteux, de ce qui est faisable.

Ces questions sont particulièrement importantes parce qu'elles ne dépendent pas de la technologie précise de calcul (sauf d'éventuels ordinateurs quantiques) et notamment ne se démodent pas avec le temps. Contrairement à un cliché répandu, les questions de science informatique ne sont pas forcément dépendantes d'une technologie en perpétuelle évolution à court terme — je dirais même, le sont rarement.

Suite à la publication d'un billet où j'évoquais des mystifications autour des théorèmes d'incomplétude de Gödel, on m'a demandé si je pouvais écrire une présentation « grand public » de ceux-ci. C'est ce que je vais tenter ici, en utilisant le moins possible de notations et de jargon mathématiques.

Malheureusement, c'est un sujet qui demande, pour être compris sans contresens, des explications assez conséquentes, et je m'excuse donc d'avance de la longueur de ce billet.

TL;DR : Comprendre ce que disent les théorèmes d'incomplétude de Gödel demande certaines bases exposées dans cet article, et si vous n'avez pas fait un minimum d'effort pour les acquérir vous ne comprendrez pas ce qu'ils disent. Ce n'est pas un drame, on vit très bien sans.

Comme le savent sans doute déjà certains de mes lecteurs, j'enseigne parfois la logique. Je trouve la logique du premier ordre difficile à enseigner non pas tant techniquement que conceptuellement : j'entends par là que la difficulté n'est pas dans la connaissance de théorèmes compliqués, d'astuces de démonstration ou de calcul, mais dans la compréhension des définitions que l'on utilise. Expérimentalement, dans un cours où figurent logique, calculabilité, et complexité, c'est la partie qui suscite le plus d'incompréhension.

J'ai donc voulu chercher comment les autres expliquaient les bases de ce sujet. J'ai bien entendu des ouvrages de logique mathématique (par exemple le Cori-Lascar, dont je déteste malheureusement la typographie) mais je voulais voir s'il y avait une façon différente d'exposer, peut-être moins « technique ». La logique étant enseignée, selon des divisions quelque peu administratives et artificielles, à la fois en informatique, mathématique et philosophie, il m'a paru intéressant de regarder un cours de logique de philosophe. Par ailleurs, bien conscient de mes lacunes en épistémologie, j'ai voulu améliorer mes connaissance sur ce sujet.

J'ai donc emprunté le Concept de Modèle, par Alain Badiou (un petit ouvrage publié en 1968 chez Maspéro dans la série « théorie — cours de philosophie pour scientifiques », collection dirigée par Louis Althusser, mais il y a une réédition récente).

Alain Badiou oppose dans cet ouvrage deux sens scientifiques du mot « modèle » (j'espère ne pas faire de contre-sens en résumant son propos avec mes propres mots et exemples) :

1. D'une part, en sciences expérimentales, le modèle est l'appareil mathématique qui est censé refléter la réalité expérimentale : par exemple, pour rendre compte des phénomènes électromagnétiques, on parle des champs électrique et magnétique, reliés par les équations de Maxwell… ou, plus simplement lorsqu'il s'agit d'un circuit électrique, de tensions et intensités.

2. D'autre part, le mot « modèle » désigne un concept mathématique précis en logique du premier ordre, qui donne une sémantique ou interprétationaux symboles (Badiou emploie plutôt le mot « marques ») des énoncés mathématiques : par exemple, qui associe au + des formules mathématiques l'opération d'addition usuelle sur les entiers.

Badiou développe plutôt ce second aspect. J'aime bien la façon dont il compare un travail très technique comme la construction d'un modèle « alternatif » de la théorie des ensembles avec une construction plus concrète : la construction d'un modèle de la géométrie riemannienne au sein de la géométrie euclidienne, tout simplement en prenant la sphère comme « plan » et ses grands cercles comme « droites ». En revanche, le vocabulaire employé est parfois inhabituel (peut-être est-ce seulement une question d'époque), et certaines explications me semblent un peu obscures.

Badiou relève également une limitation de la théorie des modèles, que certains de mes étudiants relèvent d'ailleurs d'eux-mêmes : construire un modèle d'une logique dans la mathématique « naturelle », « informelle », c'est le construire dans une méta-logique qui pourrait fort bien être elle même incohérente, autrement dit repousser d'un cran le problème de la cohérence sans l'épuiser.

En annexe, Badiou donne une démonstration du théorème de complétude de la logique du premier ordre (démontré par Gödel dans sa thèse de doctorat) par les témoins de Henkin (personnellement j'ai plutôt tendance à donner la construction d'un modèle de Herbrand, mais les goûts et les couleurs…).

Il y a en revanche quelque chose que je n'ai pas compris, c'est l'opposition maintes fois évoquée dans l'ouvrage entre l'« épistémologie bourgeoise » et une supposée épistémologie prolétarienne ou marxiste, basée sur le « matérialisme dialectique ». J'apprécierais donc sur ce sujet l'éclairage de spécialistes de philosophie, quand bien même l'ouvrage évoqué se voulait un cours d'initiation à la philosophie pour scientifiques.

Je conçois bien que toute modélisation mathématique suppose un choix de ce qui est important (et reflété dans le modèle) et de ce qui est négligeable ou hors champ. Pour prendre un exemple tiré de l'informatique, la modélisation des calculs informatiques par sémantique dénotationnelle fait disparaître le temps nécessaire au calcul, de sorte que deux programmes qui calculent la même fonction, mais l'un considérablement plus longtemps que l'autre, sont considérés comme équivalents par cette sémantique. On comprend bien que, s'agissant de tout problème se rapportant à l'humanité ou à la société, le choix de ce qu'il est important ou non d'observer et d'intégrer dans le modèle est politique, et que ce choix, intériorisé dans des modèles qui prétendent à une objectivité scientifique, relève bien d'une idéologie qui dépend d'un temps, d'un lieu, d'une histoire.

Il s'agit cependant ici d'une reconstruction personnelle de ce que Badiou aurait bien pu vouloir dire. Il me semble fort probable que, s'agissant d'un ouvrage cité et réédité d'un philosophe français reconnu, il devrait y avoir quelques lecteurs capables de m'éclairer !

Si je pense avoir une certaine idée de la lutte des classes, j'avoue notamment une certaine incompréhension du « matérialisme dialectique », bien que j'aie vu le terme dans l'introduction d'un ouvrage chinois de mathématiques. Là encore, toute aide serait appréciable, sachant que l'article Wikipédia ne m'aide guère.

Il me semble bien que dans Les petits cailloux de Bruno Poizat, il est dit qu'un problème en calculabilité est juste un ensemble d'entiers naturels, dans une idéologie (ou est-ce une téléologie ?) qui veut que ce problème soit décidé.

C'est un peu plus subtil que cela. La plupart des problèmes de décision sont décrits non pas en termes d'entiers naturels, mais de structures finies comme des graphes, des automates, des formules, qui sont codées par des entiers naturels ; autrement dit l'ensemble d'entiers naturels dont il est question dépend du codage choisi.

Le codage est laissé implicite parce que, la plupart du temps, celui-ci n'a aucune importance du point de vue des propriétés de calculabilité et de complexité tant qu'il est raisonnable. Par exemple, un codage raisonnable d'un graphe est sa matrice d'adjacence, et pour encoder celle-ci en entiers naturels on peut utiliser un codage « raisonnable » des tableaux d'entiers, lui-même basé sur un codage « raisonnable » des couples d'entiers.

En revanche, du point de vue de la théorie de la complexité, est « déraisonnable » un codage qui occuperait une taille bien supérieure à celle d'un codage « raisonnable », par exemple un codage du graphe par la matrice d'adjacence suivi d'un nombre de zéros exponentiel en la taille du graphe. En effet, un tel codage fait artificiellement baisser la complexité des algorithmes proposés, puisque celle-ci est mesurée par rapport à la taille de l'entrée : si cette taille est artificiellement enflée, l'algorithme apparaît moins cher (c'est un peu comme la malhonnêteté d'une entreprise qui se prétendrait peu chère car avec un coût horaire un peu plus faible que ses concurrences, mais qui gonflerait considérablement le nombre d'heures nécessaires).

J'ai employé le mot « malhonnête », et effectivement, certains peuvent jouer sur les définitions pour présenter leurs travaux sous un jour meilleur (et notamment planquer des exponentielles sous le tapis, ce qui m'inciterait presque à raconter la blague sur l'exponentielle qui va dans un bar). Un grand classique : écrire les entiers en unaire et non en binaire (c'est-à-dire écrire IIIIIIIIIIIIIIII, soit 15 caractères, au lieu de 15, soit 2 caractères), ou, dans le même genre, formuler la complexité en fonction du nombre d'états et non du nombre de bits qui les encodent.

On peut également proposer des codages malhonnêtes où l'entrée devrait, sous peine d'être refusée comme mal formée, contenir tout ou partie de la solution du problème.

Certains codages, en revanche, rendent plus dur la tâche de l'algorithme de décision, par exemple les codages implicites ou succincts de graphes où la matrice d'adjacence est représentée par une formule logique prenant en entrée les numéros (en binaire) des sommets concernés, et produisant en sortie un booléen indiquant si oui ou non l'arête est présente. De tels codages, le plus souvent, font passer un problème de NP-complet à NEXPTIME-complet (voir Papadimitrou & Yannakakis, 1986). Là encore, par défaut on considère n'est pas dans un tel cas et qu'on utilise un encodage « explicite ».

Nous en concluons donc que les définitions usuelles de calculabilité et complexité font appel à des notions de bon sens et d'honnêteté tant chez l'auteur que chez le lecteur ! Surprenant pour des mathématiques, que l'on imagine déconnectées des intérêts humains...

Récemment, au détour d'une conversation s'est posée la question de la scientificité des mathématiques, notamment selon les critères de Popper. Le point de vue de mon interlocutrice — j'espère ne pas le trahir — était que les objets mathématiques n'étant pas des objets physiques, le critère de réfutabilité de Popper ne s'applique pas : on ne peut pas réfuter une propriété mathématique par une expérience du monde réel. La droite mathématique (le corps des réel) est certes une idéalisation d'objets physiques (une règle, la trajectoire d'un rayon lumineux...) mais n'est pas un objet réel. Les axiomes mathématiques peuvent d'ailleurs décrire des objets mathématiques sans rapport avec le monde réel (par exemple, le groupe de classes d'idéaux d'un anneau de nombres).

J'entends cette critique et j'y suis sensible. J'aurais toutefois deux objections.

Tout le monde a déjà parlé de Nate Silver, cet analyste américain qui, s'appuyant sur des statistiques et un modèle mathématique assez simple (accumuler les résultats de sondages en privilégiant les plus récents et les plus fiables), a prédit correctement les 50 états de l'élection présidentielle américaine, après des succès pour d'autres élections et le baseball.

Je me demande quel est le sens à accorder aux « chances » affichées, du type « Obama a 80% de chances de gagner, Romney 20% ». Pour moi, c'est un modèle bayésien : il s'agirait en quelque sorte de probabilités conditionnées par les observations précédentes, avec comme espace des évènements les votes pour tous les électeurs. Dans ce cas, quelle est la distribution initiale supposée (et a-t-elle même une quelconque importance) ? Chaque électeur a une probabilité indépendante 50/50 de voter pour l'un ou l'autre ?

En revanche, je n'arrive pas à attribuer une interprétation fréquentiste. Si Silver s'était contenté de donner un chiffre pour Obama avec un intervalle de confiance, aucun problème (interprétation fréquentiste : si on refaisait un très nombre de fois les sondages et on appliquait l'algorithme de Silver, on obtiendrait plus d'une certaine proportion des résultats dans l'intervalle de confiance), mais là, je ne vois pas.