preuve et ordinateur

e=mc3 · September 2008

Bonjour

le fil récemment ouvert à propos de la découverte d'un nouveau nombre de Mersenne, m'amène à me reposer une question que je me pose depuis bien longtemps quant à la véracité mathématique d'une assertion prouvée à l'aide d'un ordinateur et non vérifiable à la main.

En supposant les algorithmes irréprochables d'un point de vue théorique, tout part du postulat qu'un ordinateur ne commet aucune erreur détectable à l'échelle macroscopique.

Je rappelle d'abord le scandale qu'il y a eu il y une quinzaine d'année lors de la lancée d'un nouveau processeur par Intel où certains calcul en virgule flottante posaient problème. Seuls des gens pointus s'en étaient rendus compte.

Mais même. Les labos d'IBM ont démontré il y a déjà plus de 20 ans (et c'est un fait reconnu aujourd'hui) que le rayonnement cosmique influait sur le fonctionnement des processeurs et générait de temps en temps des erreurs. Les contrôles par codes correcteurs en interne ne peuvent définitivement éliminer toute source de problème de ce genre ou autre.

Quand on sait le nombre de milliards de milliards de milliards etc d'opérations nécessaires pour démontrer la véracité de certaines propositions on est légitimement en droit de se poser la question de l'existence ou non d'une erreur non détectée (non détectable) lors de ces calculs.

Dans la logique classique une proposition est soit vraie soit fausse. Une simple erreur sur des milliards (beaucoup beaucoup beaucoup plus en fait) d'opérations peut faire basculer le vrai du côté du faux et réciproquement. Le fait d'effectuer des vérifications en réalisant ces calculs sur des machines différentes programmées par des équipes différentes diminue la probabilité d'erreur si à chaque fois la conclusion, après avoir laissé tourner la machine pendant des semaines, est la même. Par exemple: VRAI.

Mais au final, quel que soit le nombre de personnes qui effectueront ces tests sur des machines différentes, on ne fera qu'augmenter de manière considérable la probabilité que la proposition soit vraie. On ne peut mathématiquement prétendre que cette probabilité soit rigoureusement égale à 1.

Bref, pour moi, l'ordinateur est un outil qui aide à donner des pistes très sérieuses concernant la véracité ou non de telle ou telle proposition, sans plus dès que le nombre d'itérations prend des valeurs astronomiques.

Je vais même plus loin, mais là on rentre dans la philosophie, peut on considérer comme vraie une démonstration certes effectuée à la main, mais qui a nécessité des centaines de pages et n'est vérifiable que par une poignée d'individus.

Cela rejoint un principe qui est rappelé dans une annexe à la réforme du programme de troisième introduisant les probabilités et qui en substance (je caricature) dit que l'on peut considérer comme vrai (dans le domaine des probas)ce qui est intuitivement considéré comme tel par par une majorité d'autres personnes.

jean lismonde · September 2008

bonjour

ta question porte d'abord sur la crédibilité des ordinateurs, elle est bonne bien-sûr,
de même les calculatrices utilisées quotidiennement par nos élèves des classes secondaires ou supérieures

mais un contre-exemple trouvé à la main suffit à détruire une conjecture
qu'un ordinateur par des milliers d'expériences avait semblé corroborer
aux échecs les bons joueurs cherchent toujours à mettre en défaut les ordinateurs

donc oui l'homme est souverain sur la machine et a le droit de la contester
mais la charge de la preuve incombe alors au chercheur vis-à-vis de ses élèves ou collègues

à la fin de ton intervention tu parles des travaux scientifiques difficiles à vérifier:
la démonstration par Wiles du dernier théorème de Fermat en arithmétique n'est pas accessible à n'importe quel matheux!
la communauté mathématique admet sa véracité jusqu'à ce qu'un autre chercheur démontre le contraire
(ce qui peut demander des décennies voire des siècles), c'est le principe scientifique

tu termines par une réflexion sur le calcul des probabilités:
c'est une science mathématique qui comme les autres branches de notre discipline
est soumise à vérification empirique et peut être contestée sur le plan des principes et raisonnements
mais elle n'est pas plus exposée qu'une autre!

cordialement

e=mc3 · September 2008

Bien sûr que nos ordinateurs sont fiables. C'est même ce que l'homme à conçu de plus fiable à ce jour. Il n'en demeure pas poins qu'il s'agit d'une création de l'homme et qu'à ce titre, sans même rentrer dans des détails techniques, d'un point de vue purement philosophique, l'ordinateur ne peut être fiable à 100%

qui connait l'odre de grandeur sous forme d'une puissance de 10 du nombre d'opération processeur nécessaire pour trouver le dernier nombre de Mersenne trouvé ou la dernière décimale de Pi trouvée par exemple?

Il est intéressant de comparer ce nombre à la probabilité d'une erreur lors d'une opération par un processeur.

JJ · September 2008

Bonjour,

le cerveau humain, lui aussi, est soumis à des aléas. Sans même aller jusqu'aux rayons cosmiques, ni parler d'Alzheimer ce qui serait excessif, chacun sait que les causes d'errements sont malheureusement nombreuses, encore plus que pour les ordinateurs !
Et pourtant, il semble que l'on ait plus confiance en une preuve établie par un mathématicien, qu'une autre établie par un ordinateur (en partie seulement : l'ordinateur reste quand même programmé, dirigé et contrôlé par un ou des hommes).
On comprend bien qu'il y a tout un contexte scientifique qui fait qu'une démonstration, proposée par un mathématicien, soit finalement considérée comme valable. Pourquoi ceci serait-il strictement réservé à l'activité cérebrale humaine, dont l'ordinateur serait exclus ou soumis à une suspicion particulière ?

Christian Vassard · September 2008

Bonjour,
Je rappelle que les nombres de Mersenne premiers, ou les décimales de pi d'ailleurs, sont scrupuleusement vérifiés avant d'être rendus publics. On ne se contente pas du résultat renvoyé par un ordinateur particulier, et c'est heureux. Je ne connais pas en détail la procédure de vérification mais les calculs sont repris et contrôlés sur un autre ordinateur, éventuellement avec un autre algorithme. Cela diminue quand même singulièrement le risque d'erreur.
Par ailleurs, ce n'est pas vraiment ce que j'appelle une "démonstration par ordinateur", dont la plus célèbre, sinon la seule ou quasiment, fut celle du théorème des quatre couleurs. A moins que quelqu'un ait des informations plus précises que moi...
Cordialement
Christian V

boun0 · September 2008

un livre intéressant à lire plus ou moins autour de ce sujet : "Les métamorphoses du calcul"

e=mc3 · September 2008

C'est quoi une démonstration si ce n'est démontrer la véracité d'une proposition

Ce qui me gêne c'est
1)le caractère binaire du résultat à trouver: VRAI ou FAUX. Cela implique une extrême fragilité face aux erreurs de calcul avec une grande difficulté à découvrir s'il y a une erreur (le jour où il y en a une et cela finira bien par arriver plus on manipulera des nombres grands). Pour moi il y a une grande différence entre un programme capable de générer des nombres premiers et un programme capable de vérifier la primalité. Dans le premier cas si deux équipes différentes font tourner deux programmes différents sur des machines différentes et génèrent toutes les deux un même nombre à un million de chiffre, la probabilité d'erreur (que les deux équipes soient tombées sur un même nombre à un million de chiffre qui ne soit pas premier alors que l'algorithme n'était censé générer que des nombres premiers)est beaucoup beaucoup plus faible que celle dans la vérification de primalité, parce que dans le premier cas on est confronté à une énorme quantité de nombres possibles alors que dans le deuxième cas il n' y a que deux possibilités O ou 1 (vrai ou faux)

2°)Si la probabilité d'erreur de l'ordinateur est du même ordre de grandeur que l'inverse du nombre d'opérations qu'on lui fait réaliser pour prouver un résultat on est en droit de douter du résultat.

Christian Vassard · September 2008

Bonjour,
Je suis d'accord sur le caractère binaire du résultat, 0 ou 1, à ceci près que la probabilité qu'un grand nombre entier soit premier est finalement assez faible... pour un entier de 10^7 chiffres, elle est de l'ordre de 10^-6 sauf erreur de ma part. Donc deux ordinateurs, ou plusieurs, qui confirmeraient qu'un même entier est premier, permettent d'établir, sinon un preuve, du moins une très très très forte présomption que le nombre en question est premier.
Quant à dire que l'on a fait une démonstration... certes, mais pas la plus noble qui soit... Car montrer que 17 par exemple est premier relève plus de la mise en place d'un algorithme, que d'une démonstration mathématique.

Tu considères l'ordinateur comme un esprit humain, en quelque sorte qui se tromperait de plus en plus avec la fatigue et la répétition des calculs et dont la probabilité d'erreur dépendrait du nombre d'opérations effectuées. Je crois que les causes d'erreur dans un microprocesseur ne sont pas liées à la répétition des calculs. Le bug du pentium en est la preuve: c'est sur un calcul simplissime (une division je crois), que le processeur donnait un résultat fantaisiste.
Il suffit en fait de ne pas tomber sur un calcul qui ne marche pas... un ordinateur normalement est testé, et on peut considérer que tous les calculs marchent sans problème.

Je considère que la probabilité qu'un ordinateur se trompe est, certes pas nulle, mais en tout cas bien plus proche de 0 que la probabilité qu'un mathématicien a de se tromper dans une démonstration. J'aurais donc plus confiance dans un résultat donnant un nombre de Mersenne, que dans une démonstration humaine, comme celle de Wiles. Ceci étant, on peut quand même considérer cette dernière comme exacte.

Bien cordialement
Christian

e=mc3 · September 2008

C'est beau la confiance...

Les processeurs d'aujourd'hui sont infiniment plus complexes que ceux d'il y une quinzaine d'année, donc quand on dit qu'ils sont testés ok mais bon...on peut considérer qu'il n'y a pas de bug...tant qu'on n'en n'a pas constaté (comme pour Wiles!).

Et pour info le bug du pentium du milieu des années 90 n'a pas été trouvé tout de suite. S'il avait suffit de faire une simple division (sous entendu on fait 21/3 et il ne vous sort pas 7) pour le mettre en évidence ça aurait été un b...el planétaire et très lourd de conséquences. Il ne faut pas oublier qu'on ne manipule jamais directement (à moins d'être un fou d'assembleur) le processeur mais qu'on travaille au travers d'applications de niveau plus élevé et que bien des bugs peuvent venir d'un compilateur C ou même de l'application elle même qui a fait une mauvaise allocation mémoire ou que sais je. Il n'était donc pas facile à l'époque après que certains aient constaté qu'il y avait le problème d'arriver en incriminer le processeur lui même et non les applications.

Ce qui me gêne c'est de raisonner dans le vague sans mettre en regard le nombre d'opérations effectuées et la fiabilité des outils utilisés, comme si ce problème était secondaire.

Il l'est peut être aujourd'hui, je n'ai pas les chiffres pour pouvoir en discuter.

En tous les cas si la question devait ne pas se poser aujourd'hui elle finira bien par ce poser car on cherche à répondre à des questions mathématiques de plus en plus complexes nécessitant des volumes de calculs toujours plus importants et en tous les cas bien plus complexes que dans les plus pointues des applications et cela tout simplement parce que le mathématicien s'autorise à se poser des questions d'aucune utilité à priori (connaître la milliardième décimale de pi présente-t-il un intérêt pratique?) avec une certaine fascination pour l'infini. COntrairement au physicien qui ne voit pas l'intérêt de manipuler des longueurs plus grandes que l'univers (même s'il est en expansion) le mathématicien peut s'autoriser à manipuler des nombres aussi grands qu'il le souhaite et rien ne peut le stopper dans sa recherche effreinée, quasi mégalo, de nombres de Mersenne premiers toujours plus grands. Que cherche-t-on alors? A se rapprocher de Dieu?

bs · September 2008

Bonjour,

Peut-être est-ce déjà mentionné ( je n'ai pas tout lu ) mais il me semble que le second grand théorème ayant nécessité l'utilisation d'ordinateurs est le théorème de classification des groupes simples finis , et donc, des groupes sporadiques et du "Monstre" en particulier (1985).

Ref: Le théorème géant - Daniel Gorenstein - Pour La Science - Fev 1986

Amicalement.

Christian Vassard · September 2008

Bonjour

Exact BS! Un fameux théorème aussi passant pas l'examen d'un grand nombre de cas, comme pour le théorème des quatre couleurs!

Pour E=mc3: je ne dis pas que tout ceci est secondaire, mais à l'inverse il ne faut sans doute pas lui donner une importance cruciale, comme tu sembles le faire.
Il me semble que l'évolution des mathématiques se fait vers les ordinateurs, et que nous n'y échapperons pas! Restons vigilants, j'en suis d'accord avec toi.

Bien cordialement
Christian

leg0 · September 2008

bonjour
la véracité du test des nombre de Mersenne n'est en aucun cas une démonstration
tout simplement du fait que le test est démontré!

ensuite on utilise de gros calculateur pour effectuer toutes les opération du test de Lucas/L ;soit P - 2 opérations = 43 112 607 pour M46.

je ne vois vraiment pas ce qu'il y a d'insurmontable pour un calculateur, car si à ce niveau de calcul les ordinateurs ou même des calculatrices ne serait pas capable d'effectuer ces opération sans se tromper, alors rien n'enpèche de les faire à la main sans se tromper...!!!!(:P)
(ce qui implique de ne pas oublier toutes les décimales)

la deuxième vérification est tout simplement une confirmation avec du materiel plus performant et prenant 5 fois moins de temps, c'est tout.

e=mc3 · September 2008

Je n'ai pas dit que sur le cas d'espèce l'usage de l'ordinateur était incensé.

pour info un disque dur commet en moyenne une erreur tous les $10^15$ bits. Mais il est vrai que c'est l'élément le moins fiable dans un ordinateur.

euzenius · September 2008

Bonsoir,

Je me souviens avoir fait tourner un programme visant à modéliser le remplissage d'un barrage en 30 jours de deux manières : la première jour après jour, l'autre heure après heure. Les résultats concernant les contraintes était bien différents dans les deux cas. Diminuer la période de calcul c'est introduire le bruit blanc des approximations par virgule flottante.

Dans le cas où l'on a des calculs justes le bruit blanc cosmique peut effectivement interférer mais je pense qu'il faut vraiment du temps et j'ignore lequel, mais effectivement il suffit d'une seule modification pour tout foutre en l'air, mais on peut recommencer.

D'ailleurs la raison du système binaire est qu'il pose moins de problème question courants de fuite alors que les système ternaire et au delà génèrent ce risque bien plus important que celui des rayons cosmiques.

Pour votre gouverne sur ce phorum j'ai déjà évoqué ce que j'ai appelé la divine identité (8 carrés) et qui étend l'identité de Brahmagupta (2 carrés) en augmentant le nombre de possibilités. Brahmagupta donne deux possibilités et la divine identité 1024 (à vérifier) ce qui n'est pas envisageable à la main. Or cette divine identité peut servir dans l'étude de la factorisation des entiers via leurs représentations en somme de carrés. Il faudra donc sans doute prévoir un jour une arithmétique assistée par ordinateur les calculs de base ne pouvant se faire à la main. Mais bon on peut aussi en avoir besoin pour du simple calcul matriciel dans Z...

Bonne réflexion

Euzenius

JJ · September 2008

Bonjour,
"e=mc3" a écrit (18 septembre, 11:01:09) :

C'est quoi une démonstration si ce n'est démontrer la véracité d'une proposition
Ce qui me gêne c'est
1) Le caractère binaire du résultat à trouver: VRAI ou FAUX … etc.
2) Si la probabilité d'erreur de l'ordinateur… etc.

Certes, mais attention aux amalgames et à ne pas se tromper sur l'origine des divergences d'appréciations. Tout le monde est d'accord : le but est d'établir des propositions vraies et il y a des risques d'erreurs, ceci que ce soit avec l'aide de l'ordinateur ou purement "à la main".
Les risques liées à l'usage de l'ordinateur ont été largement soulignés. Quant aux démonstrations "à la main", il est arrivé de nombreuses fois qu'elles soient révélées fausses par la suite.
En fait, ces observations ne sont pas l'objet réel de la discussion. Ce qui est en cause, c'est le processus de validation qui s'engage après qu'une proposition ait été faite. Ces vérifications sont généralement faites par plusieurs spécialistes différents et souvent avec des méthodes différentes. Suivants les cas, elle sont faites "à la main" ou avec participation de calculs par ordinateur. Elles aboutissent après des délais parfois longs, à ce que la communauté scientifique accepte la proposition comme étant vraie, ou au contraire qu'une faille soit révélée dans la preuve initialement proposée. Tout ceci s'applique aussi bien aux procédés "à la main" qu'à ceux "à l'ordinateur".
Quel est le risque d'aboutir à ce qu'une proposition fausse (sans qu'on le sache, évidemment) soit finalement acceptée, à tort, comme étant vraie ? C'est bien cette question qui se pose dans un cas comme dans l'autre.
On aurait tendance à croire que le risque est nul pour les démonstrations par les méthodes traditionnelles et qu'il est faible, mais non nul, pour les méthodes par ordinateur. C'était certainement vrai lorsqu'il s'agissait de démonstrations relativement simples. Mais il s'agit maintenant de propositions beaucoup plus complexes et qui, parfois, ne sont à la portée que d'un petit nombre de spécialistes dans le monde. Les vérifications, même purement à la main lorsque cela reste possible, ne sont plus faites par de nombreux mathématiciens, mais par quelques uns seulement dont c'est le domaine de travail. Il n'est pas totalement impossible que la même erreur de raisonnement ou de démonstration soit commise par ce petit nombre de personnes que l'erreur faite initialement par le premier mathématicien à l'origine de la proposition. Ceci d'autant plus que sa démarche à été publiée et lue par les autres, ce qui a pu les influencer inconsciemment. On ne peut pas dire qu'une proposition, acceptée comme étant vraie, le soit effectivement avec un risque d'erreur rigoureusement nul. Et ceci vaut pour le travail "à la main", ainsi que pour celui "à l'ordinateur".
Le risque étant finalement infime, c'est une question de sentiment et d'appréciation que de dire qu'il est plus élevé dans un cas que dans l'autre.
Mais les choses devenant de plus en plus complexes d'une part, et d'autre part les progrès des méthodes "électroniques" et du calcul formel étant considérables et se poursuivant (bien que l'on soit encore loin de ce qui serait souhaitable), ma confiance aux preuves par ordinateur (géré et contrôlé par l'homme, bien sûr) tend à s'accroître, alors que j'ai un peu moins confiance au trop faible nombre de vérifications d'une démonstration monumentale qui n'est à la portée que de quelques spécialistes seulement, qu'il faut croire sur parole, de même que l'on doit croire sur parole ceux qui font des vérifications à l'aide d'ordinateurs.

Alban · September 2008

LA démonstration de théorème de Képler sur l'empilement des sphères a aussi récemment été assistée par ordinateur (2004 si je ne m'abuse).

Il y a une belle vidéo sur la notion plus générale de "vérité" en mathématiques mais je n'arrive plsu à trouver le lien (le conférencier de l'ens Lyon parle d'un théorème de Poincaré-Bendixon dont la véracité a connu quelques tumultes au cours du temps : vrai, puis faux, puis on ne sait pas !)

Francois_D_pas_logge · September 2008

Salut,

trouverait-on ça ici: Vidéos ENS Lyon?

Amicalement,

F.D.

nicolas.patrois · September 2008

e=mc3 a écrit:

Ce qui me gêne c'est
1)le caractère binaire du résultat à trouver: VRAI ou FAUX.

C’est pour ça qu’on teste le programme sur différentes architecture et compilés par différents compilateurs, voire différents langages.

preuve et ordinateur

Réponses

Bonjour!

Catégories

In this Discussion