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

Le 24 août 2010  - Ecrit par  Étienne Ghys Voir les commentaires (15)

L’une des conférences plénières les plus appréciées par les participants de l’ICM [1] (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 !

JPEG - 29 ko
Irit Dinur

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 INDEPENDANT 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.

Notes

[1Voir ce billet.

Partager cet article

Pour citer cet article :

Étienne Ghys — «Vérifier une preuve : la conférence de Irit Dinur » — Images des Mathématiques, CNRS, 2010

Commentaire sur l'article

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

    le 24 août 2010 à 14:06, par Julien Olivier

    Je ne comprends pas bien votre objection : qu’un ordinateur soit capable de vérifier les preuves des quatre médaillés de cette année ne veut pas dire qu’un programme informatique soit capable de produire ces preuves non ?

    Un prof nous a dit une fois (cela remonte à loin et en plus je n’étais pas très bon donc si c’est une ânerie n’hésitez pas à corriger) : « Théoriquement, un ordinateur est capable d’énumérer tous les théorèmes de la théorie des groupes. Mais si on avait fait tourner cet ordinateur depuis 2000 ans, il n’en serait qu’à 1x1=1 ».

    Ce qu’il faut éviter c’est que les journaux ne publient la preuve P’ qui, j’imagine, serait absolument incompréhensible pour un humain.

    Répondre à ce message
  • Vérifier une preuve : la conférence de Irit Dinur

    le 24 août 2010 à 15:18, par Étienne Ghys

    Merci pour votre message. Quelques remarques pour éclairer des points que j’aurais du expliquer.

    D’abord, trouver une preuve d’un théorème est bien plus difficile et bien plus long que vérifier une preuve qu’on vous propose.

    Ce que je voulais dire en parlant des articles des médaillés Fields, c’est qu’ils ne sont bien sûr pas rédigés dans une langue qu’un ordinateur pourrait lire et vérifier. Ils contiennent des phrases en français (ou en anglais suivant les cas) qui mettent en jeu des choses implicites, qui sont en principe comprises par des mathématiciens « humains » et pas par des ordinateurs !

    Votre prof avait raison : on peut demander à un ordinateur d’écrire une à une toutes les preuves possibles, par ordre alphabétique en quelque sorte. Mais bien sûr, l’immense majorité des théorèmes que votre ordinateur va écrire n’auront aucun intérêt, et vous n’avez aucune idée à priori du temps que ça prendra pour voir apparaître la preuve de l’hypothèse de Riemann, si elle arrive un jour !

    Je suis tout à fait d’accord avec votre dernier commentaire : il nous faut des preuves lisibles par des êtres humains... C’est un peu ce que je voulais dire en signalant qu’une preuve n’est pas seulement une suite de symboles, mais doit contenir des idées..

    Etienne Ghys

    Répondre à ce message
  • Vérifier une preuve : la conférence de Irit Dinur

    le 24 août 2010 à 16:07, par Ilies Zidane

    Résultat fort intéressant (théoriquement), mais comme vous le dites, je doute qu’il puisse exister un jour un algorithme qui vérifie des preuves « sérieuses ». Une petite question : la construction de P’ est t-elle déterministe ?

    Répondre à ce message
    • Vérifier une preuve : la conférence de Irit Dinur

      le 24 août 2010 à 18:48, par Étienne Ghys

      Oui, en effet, c’est tout à fait déterministe et explicite.

      Etienne Ghys

      Répondre à ce message
    • Vérifier des preuves sérieuses

      le 25 août 2010 à 00:12, par Pierre Lescanne

      Vous doutez qu’il puisse exister un jour un algorithme qui vérifie des preuves « sérieuses ». Et bien, il y a des gens qui pensent exactement le contraire et ça leur donne une excellente piste de recherche.

      Répondre à ce message
    • Vérifier une preuve : la conférence de Irit Dinur

      le 25 août 2010 à 10:42, par Benoît Kloeckner

      Tout d’abord, n’oublions pas que les travaux d’Irit Dinur peuvent s’appliquer en informatique sur des « certificats », c’est-à-dire des preuves putatives qu’une certaine proposition est correcte. On peut vouloir certifier des énoncés mathématiques intéressants, mais aussi des calculs et des programmes.

      Ensuite, vous vous trompez : on sait déjà écrire dans des langage vérifiables par ordinateur des preuves très sérieuses. Le théorème des quatre couleurs a par exemple été vérifié ainsi. J’ai entendu parler d’un projet stupéfiant : une équipe de recherche s’attaque à la vérification par ordinateur de la classification des groupes finis simple.

      C’est à mon avis très intéressant, car cette classification est tellement longue à obtenir, tellement dispersée dans la littérature, qu’on n’est pas complètement sûrs que la preuve soit juste.

      En fait, je préfèrerais encore qu’on trouve à ces résultats des démonstrations assez simples pour être entièrement vérifiées par un être humain en un temps raisonnable, mais un certificat informatique est tout de même loin d’être négligeable.

      Il faut aussi se rappeler qu’il y a forcément des énoncés simple, vrai (et même démontrable) qui n’ont pas de démonstration courte. Évidemment, on ne sait pas lesquels !

      Répondre à ce message
  • Vérifier une preuve : la conférence de Irit Dinur

    le 25 août 2010 à 18:55, par Ilies Zidane

    Ca rend le théorème autant plus intéressant. Avez vous des références ou liens sur ce genre de programmation, ça doit être intéressant à décortiquer.

    Répondre à ce message
  • Vérifier une preuve : la conférence de Irit Dinur

    le 27 août 2010 à 15:33, par DanielAugot

    Hop, un lien vers les preuves en informatique

    Attention, cela n’est pas de même nature que le théorème PCP qui relève de la théorie de la complexité. De plus dans ce dernier, seules les preuves de taille polynomiale peuvent être encodées pour être vérifiée de manière probabiliste.

    Amitiés.

    Répondre à ce message
    • Vérifier une preuve : la conférence de Irit Dinur

      le 28 août 2010 à 16:04, par Étienne Ghys

      Merci pour ces références. Je crains cependant que ces articles de recherches ne soient un peu difficiles pour nos lecteurs ?

      Cordialement,

      Etienne Ghys

      Répondre à ce message
      • Vérifier une preuve : la conférence de Irit Dinur

        le 1er septembre 2010 à 17:47, par Pierre Lescanne

        Sur les preuves formelles en général, ceux qui lisent l’anglais peuvent lire Formal proof : theory and practice de Jim Harrison, qui est article pour un large public.

        Répondre à ce message
    • Vérifier une preuve : la conférence de Irit Dinur

      le 1er septembre 2010 à 17:59, par Pierre Lescanne

      Sur les démonstrations vérifiables et toujours pour les anglophones, je recommande Probalistically checkable proofs par Madhu Sudan qui s’adresse aussi à un large public. A vrai dire, je n’ai pas lu cet article précis, mais ceux que j’ai lus dans cette rubrique, sur des domaines que je ne connaissais pas, étaient excellents. Dites-moi si je me trompe pour celui-ci.

      N.B. L’accès que je donne peut être restreint. Faites-moi un courriel si vous rencontrez des problèmes.

      Répondre à ce message
  • Vérifier une preuve : la conférence de Irit Dinur

    le 30 août 2010 à 11:01, par DanielAugot

    Ah désolé pour le lien difficile. C’était pour répondre à Benoît ci dessus, qui dit j’ai entendu parler d’un projet stupéfiant : une équipe de recherche s’attaque à la vérification par ordinateur de la classification des groupes finis simple.

    J’ai juste voulu donner un point d’entrée sur ce projet. Je pense qu’en suivant les pages personnelles des chercheurs impliqués, on finit par trouver des éléments plus faciles.

    Amicalement,

    Daniel

    Répondre à ce message
    • Vérifier une preuve : la conférence de Irit Dinur

      le 2 septembre 2010 à 15:50, par Pierre Lescanne

      Dans premier temps, la formalisation en COQ de la démonstration du théorème de Feit et Thompson qui est une étape vers celui de la classification des groupes finis a bien avancé et je rappelle que John Griggs Thompson a reçu pour cela la médaille Fields en 1970.

      Répondre à ce message
  • Vérifier une preuve : la conférence de Irit Dinur

    le 13 septembre 2010 à 18:13, par Ilies Zidane

    Merci beaucoup pour les liens. En particulier DanielAugot, c’est pile ce que je cherchait.

    Répondre à ce message
  • Vérifier une preuve : la conférence de Irit Dinur

    le 2 novembre 2010 à 10:00, par Pierre Pansu

    Une info pour les lecteurs parisiens : Irit Dinur sera à Paris du 17 au 21 janvier 2011, pour un colloque mêlant informaticiens théoriciens et mathématiciens. Elle donnera un mini-cours de 3 séances, qui devrait exiger peu de connaissances préalables, voir
    http://www.math.ens.fr/metric2011/

    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