Même les ordinateurs font des erreurs !

Explosion d’Ariane 5 (1996).

Comme vu dans de nombreuses brèves précédentes, les mathématiques fournissent des algorithmes précis et rapides pour calculer toutes sortes de valeurs, de la trajectoire des planètes à la simulation des avalanches en passant par des concentrations de plancton. Néanmoins, une question se pose naturellement (surtout dans le cas de la météo où la comparaison est facile) : dans quelle(s) situation(s) les valeurs finales sont-elles justes ? La réponse est évidemment qu’elles ne le sont pas toujours. Et les conséquences peuvent être importantes !

Ainsi, le premier vol d’Ariane 5 en 1996 fut un échec : un dépassement de capacité mémoire non prévu a mené à une auto-destruction préventive de la fusée. Un autre exemple davantage lié aux erreurs de calcul est celui de l’anti-missile Patriot lors de la première guerre du Golfe en 1991 : à chaque tic de l’horloge (10 fois par seconde), la valeur 1/10 était ajoutée à un compteur. Mais 1/10 n’est pas exact pour un ordinateur (d’environ 0,000001% pour un nombre flottant sur 32 bits) et c’est donc la valeur 0.1000000014901… qui était chaque fois ajoutée. Cette toute petite erreur a été répétée pendant plus de 100 heures et ces erreurs, toujours dans le même sens, se sont accumulées jusqu’à ce que la différence entre les diverses horloges fasse que l’anti-missile rate un missile irakien. Le missile a alors tué 28 GIs.

En plus du fait que le phénomène étudié peut être plus complexe que ce qu’on réussit à modéliser, un calcul peut être entaché de bien des erreurs. Première source d’erreur : le mathématicien. L’algorithme peut être moins bon que prévu et on a pu sous-estimer le nombre de calculs à effectuer pour avoir un résultat précis. Deuxième source, le numéricien lors de la programmation des algorithmes en machine : accès erroné à la mémoire, erreur de signe… La moindre faute d’inattention peut donner un résultat aberrant.

Dernier facteur d’erreur bien plus insidieux que les précédents : les ordinateurs calculent faux. Chaque calcul est effectué avec un certain nombre de chiffres fixé. Un calcul doit souvent être arrondi pour être représenté dans ce format de nombre. Cela crée une erreur minime à chaque calcul, mais ces erreurs peuvent s’accumuler ou être magnifiées dans certains cas. Une solution à ces problèmes est l’utilisation d’outils (d’autres programmes) pour vérifier des programmes et des preuves, permettant ainsi de certifier la correction (c’est-à-dire la justesse) de ces derniers. Cela a été fait sur un programme très simple de résolution de l’équation des ondes en dimension 1.

Cette équation représente par exemple la vibration d’une corde. Dans d’autres circonstances, elle peut aussi bien représenter la propagation du son, de la lumière, ou des ondes sismiques. Sur cet exemple précis, nous avons:

spécifié ce que le programme devait faire (donner une réponse proche de la réponse mathématique),
prouvé formellement que la preuve mathématique était juste, ce qui signifie que la preuve a été mécaniquement vérifiée par ordinateur,
prouvé formellement qu’il n’y a pas d’erreur de programmation,
prouvé formellement une borne sur les erreurs d’arrondi.

Tout cela a représenté un gros travail (plus de 40 pages de preuves mathématiques usuelles sur papier, 11000 lignes de preuves formelles) utilisant 8 outils (dont Coq) de 6 personnes sur une période de 6 ans.

Brève rédigée par Sylvie Boldo (Inria), sur la base de ses travaux en collaboration avec François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond et Pierre Weis.

Pour en savoir plus :