Vérifier une preuve : la conférence de Irit Dinur

• Monde de la recherche

.

L’une des conférences plénières les plus appréciées par les participants de l’ICM (Voir ce billet) (jusqu’à présent) a été celle de Irit Dinur. Elle a expliqué son thème de recherche en termes clairs et accessibles à tous, a présenté le « théorème PCP » et a même réussi à donner une esquisse de sa preuve. Tout cela en une heure. Chapeau !

Le travail du mathématicien, on le sait, consiste pour l’essentiel à démontrer de nouveaux théorèmes. La première étape (souvent la plus difficile !) consiste à se poser la bonne question : trouver le théorème qu’on aimerait bien démontrer. Il faut de l’imagination pour cela. La seconde étape, (pas facile non plus) consiste à trouver une preuve du théorème en question ! Et puis, la troisième étape, la moins drôle, et pourtant indispensable, consiste à convaincre ses collègues que la preuve est correcte…

En pratique, le matheux écrit une prépublication contenant la preuve et l’envoie à un journal. Le rédacteur en chef de ce journal, aidé par son comité de rédaction, choisit un ou plusieurs experts anomymes (les referees dans notre jargon) auxquels il demande de lire et de vérifier la preuve en question. Ce n’est que si les referees sont convaincus de la preuve (et aussi de l’intérêt du théorème !) que l’article peut être validé et publié.

Travail ingrat que celui du referee. Il doit lire le travail d’un autre et chercher la petite bête. Cela prend du temps, beaucoup de temps, et restera pour toujours anonyme (même s’il arrive malheureusement que l’anonymat ne soit pas respecté). Bien sûr, ce travail est également intéressant puisqu’il permet d’apprendre de nouvelles techniques, de nouvelles idées etc. Il n’empêche que les revues mathématiques ont de plus en plus de mal à trouver des referees qui acceptent de faire le travail sérieusement. C’est un problème sérieux et on voit souvent des articles publiés pour lesquels on peut se demander s’ils ont été relus par un referee.

D’une certaine manière, vérifier une preuve est un travail automatique. En principe, il suffit de lire le texte ligne à ligne et de vérifier pour chaque ligne qu’elle est bien une conséquence des lignes précédentes ! Bien sûr, un referee ne fonctionne pas de cette manière dans la pratique. Il commence par naviguer dans l’article, chercher les points clés, remettre à plus tard la vérification des points secondaires qui lui semblent « standards » etc. « Référer » sérieusement un article d’une centaine de pages par exemple est un travail considérable.

La conférence de Irit Dinur permettra-t-elle un jour de simplifier le travail des referees vérificateurs ? Combien de temps faut-il pour vérifier un article de \(N\) pages ? Il peut sembler évident qu’il faut un temps proportionnel à \(N\) puisqu’il faut tout lire dans l’ordre… Disons par exemple qu’un article de 100 pages contient 100 000 lettres ou signes et qu’il me faut 10 secondes pour lire et vérifier chaque lettre. Il me faudra travailler 1 000 000  secondes : 12  jours (et nuits…). S’il y a une erreur (et une seule suffit pour détruire la preuve), elle peut se trouver n’importe où !

Le théorème PCP que je vais essayer d’énoncer maintenant donne un autre point de vue sur le concept de preuve. (PCP veut dire « Probabilistic Checkable Proof ». Le théorème affirme que si une assertion possède une preuve \(cal P\) de longueur \(N\), alors elle possède une autre preuve \(cal P′\) qui est très facile à vérifier, tout au moins avec une bonne probabilité ! Précisément, cela signifie que si on choisit au hasard 3 lignes de la preuve \(cal P′\) et qu’on n’y trouve pas d’erreurs, alors il y a plus de 50% de chance qu’il n’y a pas d’erreur du tout. Si 50% ne vous suffit pas, on peut recommencer le test, en tirant \(3\) nouvelles lignes au hasard : si on ne trouve pas d’erreur, il y a plus de 75% de chances qu’il n’y en a pas. Et si je le fais, disons 100 fois, et que je ne trouve pas d’erreur, la probabilité qu’il existe une erreur quelque part, dans la partie non lue, sera inférieure à \(2^{-100}\), soit environ \(1,3. 10^{-30}\), c’est-à-dire microscopique. On peut dire qu’il reste une possibilité d’erreur mais quel referee oserait dire que la probabilité qu’il a laissé passer une erreur est inférieure à \(10^{−30}\) ! Ce qui est remarquable dans ce théorème, c’est que le nombre de lignes qu’il suffit de lire pour avoir une quasi-certitude que le théorème est correct est INDÉPENDANT de \(N\), c’est-à-dire de la longueur de la preuve !!!

Init Dinur a employé une analogie pour expliquer ce théorème. C’est un peu comme si, dit-elle, vous avez une tranche de pain qui a peut-être quelque part, un petite goutte de confiture, mais vous ne savez pas où. Vous prélevez un bout de la tartine, au hasard, et vous ne trouvez pas de confiture ; pouvez-vous en déduire qu’il n’y a pas de confiture du tout ? Certainement pas, sauf si vous faites beaucoup d’échantillonnages. Mais si vous commencez par étaler la confiture sur la tranche de pain avec un couteau, elle se retrouvera un peu partout et il suffit d’en prendre un échantillon pour savoir s’il y avait ou pas une goutte de confiture. Ici, c’est la même chose. On part d’une preuve \(\cal P\) qui possède quelque part, peut-être, une erreur. Il existe une manière d’« étaler » la preuve pour en construire une autre \(\cal P′\) dans laquelle les erreurs, s’il y en a, se sont « propagées » un peu partout et elles sont maintenant faciles à détecter en prenant un tout petit nombre d’échantillons.

Quelques remarques. La construction de la nouvelle preuve \(\cal P′\) à partir de \(\cal P\)  est complètement automatique et pourrait en principe être réalisée par un ordinateur. Vous me ferez l’objection que ce travail de traduction de la preuve prend un certain temps, certainement plus grand que \(N\), la longueur de la preuve. Alors, à quoi bon passer beaucoup de temps à traduire une preuve pour en fabriquer une autre facilement vérifiable si le temps de traduction est du même ordre de grandeur que la vérification toute simple de la preuve initiale ? Qu’a-t-on gagné dans ce jeu ? Plusieurs réponses à cela.

D’abord, on peut demander à l’auteur du théorème de faire ce travail lui-même et de soumettre directement la preuve \(\cal P′\). Le referee pourra alors vérifier la preuve très rapidement, dans un temps qui ne dépend pas de sa longueur (!), avec une très bonne probabilité.

Mais aussi, cela ouvre la porte à des choses un peu désagréables. Imaginons par exemple que je trouve une démonstration de l’hypothèse de Riemann, le rêve de tous les matheux, mais que je veuille la garder pour moi. Comment faire pour convaincre mes collègues que j’ai une preuve sans leur montrer ? Eh bien, je la traduit en \(\cal P′\) et mes collègues me demandent d’en montrer 300 lignes qu’ils choisissent eux-mêmes. S’ils ne trouvent pas d’erreurs, ils seront convaincus que je ne bluffe pas.

Bien sûr, tout cela est très théorique. Bien sûr, les preuves mathématiques qu’on trouve dans les revues sont très loin de ressembler à des suites de symboles qu’un ordinateur peut vérifier.

D’une certaine façon, un programme d’ordinateur est un peu comme une preuve. Il y a toujours le risque d’une erreur de programmation quelque part. On peut donc penser utiliser le théorème PCP dans ce cas. Alors, l’idée qu’une compagnie privée veuille vendre un logiciel sans dévoiler son contenu et que le client veuille s’assurer que le « logiciel marche bien » est beaucoup plus réaliste que celle selon laquelle je ne voudrais pas vous montrer ma preuve de l’hypothèse de Riemann 🙂

Il faudra encore attendre très longtemps pour qu’un ordinateur puisse vérifier un quelconque article de nos quatre récents médaillés Fields par exemple. Mais qui sait ? Un jour ? Mais si ce jour arrive, je ne suis pas sûr que j’aurai encore envie de faire des maths. Car une preuve, ce n’est pas qu’une suite de symboles, c’est avant tout une suite d’idées.

Un grand merci à Irit Dinur pour sa conférence.