Preuves de programmes numériques, arithmétique à virgule flottante et analyse numérique
Présentation
Les activités de recherche poursuivies par l'axe « Preuves de programmes numériques » concernent la preuve de programmes contenant des calculs sur des nombres à virgule flottante, typiquement des nombres simple ou double précision de la norme IEEE-754.
L'arithmétique à virgule flottante est principalement utilisée pour calculer avec des nombres réels de façon approchée mais efficace. À cause d'une précision limitée, les opérations flottantes peuvent introduire des erreurs au cours des calculs numériques. La figure sur la droite illustre ce phénomène dans le cas de l'orientation de trois points représentés par la flèche orange. Les deux extrémités sur la diagonale sont fixées, tandis que le point du milieu se déplace librement. La couleur (bleu/vert/rouge) au niveau du point milieu indique l'orientation. Par exemple, quand ce point est au-dessus de la diagonale, les trois points sont orientés dans le sens anti-horaire, d'où la couleur bleue.
L'orientation des trois points peut s'obtenir en calculant le déterminant d'une matrice 2×2 et en s'intéressant à son signe (5 soustractions, 2 multiplications). Un déterminant nul signifie que les trois points sont alignés ; s'il est positif, les trois points sont orientés dans un sens ; et s'il est négatif, dans l'autre. Le signe calculé semble généralement correct, mais la partie inférieure de la figure montre que les imprécisions liées aux opérations flottantes entraîne un calcul incorrect de l'orientation pour certaines positions du point milieu, en particulier quand les trois points sont presque alignés.
What Every Computer Scientist Should Know About Floating-Point Arithmetic
Personnes
Sylvie Boldo, Guillaume Melquiond, et partiellement Catherine Lelay et Claude Marché.
Anciens contributeurs
Tuyen Nguyen.Thématiques
Arithmétique à virgule flottante
Nous nous intéressons à la vérification d'algorithmes qui effectuent des opérations flottantes afin d'obtenir des résultats subtils. Ces algorithmes sont généralement courts mais ce qu'ils calculent ne se devine pas d'une simple lecture de leur code. En effet, ils représentent l'état de l'art et ont été raffinés encore et encore jusqu'à obtenir les meilleurs performances pour une précision donnée du résultat. Les opérations ont ainsi été réordonnées, des expressions ont été approchées, des principes d'exclusion ont été utilisés, et ainsi de suite. Ces algorithmes ont été testés en profondeur pendant leur développement, mais la plage des nombres flottants est tellement large que des tests exhaustifs sont hors de portée. C'est pourquoi nous développons des méthodes et des outils permettant de les vérifier formellement et de s'assurer que tous les comportements possibles ont bien été pris en compte.
Nous avons développé une formalisation générique de l'arithmétique à virgule flottante qui est utilisable aussi bien pour vérifier des programmes numériques que pour calculer au sein d'un assistant de preuve. Nous avons aussi vérifié formellement la correction de plusieurs algorithmes utilisés comme briques de base : calcul précis du discriminant, transformations sans erreur, émulation de l'opérateur FMA (fused-multiply-add), etc. La figure de droite présente l'algorithme émulant le FMA.
L'écriture manuelle de preuves formelles s'est révélée un succès, mais c'est une approche qui passe mal à l'échelle : la vérification d'algorithmes longs devient vite pénible et trop coûteuse en temps, même pour des experts en systèmes formels. Nous développons donc aussi des outils automatiques capable de vérifier des propriétés arithmétiques (domaines, erreur d'arrondi, etc) et d'en générer une preuve formelle.
Du fait de l'expertise mathématique et numérique dont sont issus les systèmes qui nous intéressent, la correction d'une partie seulement d'entre eux peut être automatiquement traitée. Une intervention humaine reste nécessaire pour vérifier les parties les plus subtiles. C'est pourquoi nous nous concentrons sur la coopération entre preuve interactive et outils automatiques. Étant donné un programme annoté, des obligations de preuve exprimant sa correction sont générées. Idéalement, la majorité de ces obligations seront déchargées automatiquement, par exemple à l'aide d'outils dédiés au calcul flottant. Les quelques unes restantes seront alors prouvées manuellement dans un système formel. Mais elles n'ont pas besoin pour autant d'être prouvées intégralement ; il suffit de les simplifier suffisamment pour que les outils automatiques prennent le relai.
Nos analyses prennent aussi en compte les changements de sémantiques apportés aux algorithmes numériques par l'environnement de calcul (architecture matérielle, compilateurs, etc). Par exemple, le jeu d'instruction d'un processeur peut fournir des registres flottants étendus ou des opérateurs FMA. Un compilateur risque alors d'en tirer avantage pour optimiser le code. Par conséquent, la précision des opérations flottantes à l'exécution ne correspond plus à celle prévue par l'algorithme initial, provoquant ainsi des changements de comportement.
Programmes d'analyse numérique
Nous souhaitons développer et appliquer des méthodes pour prouver formellement la correction de programmes provenant de l'analyse numérique. Cela se fait en deux temps: erreur d'arrondi et erreur de méthode. L'erreur d'arrondi correspond à l'accumulation des erreurs d'arrondi lors du calcul des valeurs. Il a fallu développer de nouvelles techniques complexes car les techniques usuelles donnaient une borne d'erreur trop importante par rapport à la réalité. L'erreur de méthode correspond aux erreurs dues à la discrétisation de l'équation aux dérivées partielles sur une grille. Les preuves mathématiques issues de la littérature se sont révélées insuffisantes et il a fallu combler quelques trous afin de finir formellement cette preuve. La principale difficulté a été la définition du O mathématique qui doit être très précis (par rapport aux notations mathématiques imprécises) et uniforme sur un intervalle.
Nous avons travaillé sur l'équation des ondes acoustique en une dimension, ce qui correspond à l'oscillation d'une corde attachée à ses deux extrémités comme sur l'image de gauche. Cette équation aux dérivées partielles est approximée par un schéma aux différences finies du second ordre, aussi appelé « schéma à 3 points ». Plus précisément (voir l'image de droite), la valeur en pjk (point rouge) dépend de pj-1k-1, pjk-1, pj+1k-1 et pjk-2 (points bleus).
Développements de logiciels ou de preuves
- Flocq (Floats for Coq) est une formalisation de l'arithmétique à virgule flottante pour le système Coq. Elle fournit une large bibliothèque de théorèmes sur l'arithmétique multi-base et multi-précision ; elle permet aussi d'effectuer des calculs numériques efficaces dans Coq.
- PFF est une formalisation Coq de l'arithmétique flottante fournissant des définitions et des propriétés de haut niveau. Elle est maintenant remplacée par la bibliothèque Flocq.
- Gappa est un outil de vérification automatique des propriétés de programmes numériques en arithmétique à virgule fixe ou flottante. Bien que conçu pour être utilisé directement, il peut aussi servir de prouveur pour la plateforme Why ou de tactique pour l'assistant de preuve Coq.
- Coq.Interval fournit une tactique Coq pour prouver automatiquement certaines inégalités entre expressions réelles contenant des fonctions élémentaires.
- Participation à Why3, Why/Jessie et Frama-C.
Collections de programmes prouvés
See our gallery of verified programs or S. Boldo's gallery.Contrats
- Projet ANR - INS VERASCO
- Projet RTRA Digiteo Coquelicot
- Normalisation de l'arithmétique d'intervalles IEEE-1788 (INRIA D2T)
Anciens contrats
Publications majeures
| [1] | Guillaume Melquiond. Floating-point arithmetic in the Coq system. Information and Computation, 216:14-23, 2012. [ bib | DOI ] |
| [2] | Sylvie Boldo and Guillaume Melquiond. Flocq: A unified library for proving floating-point algorithms in Coq. In Elisardo Antelo, David Hough, and Paolo Ienne, editors, Proceedings of the 20th IEEE Symposium on Computer Arithmetic, pages 243-252, Tübingen, Germany, 2011. [ bib | DOI | full paper on HAL ] |
| [3] | Florent de Dinechin, Christoph Lauter, and Guillaume Melquiond. Certifying the floating-point implementation of an elementary function using Gappa. IEEE Transactions on Computers, 60(2):242-253, 2011. [ bib | DOI | full paper on HAL ] |
| [4] | Sylvie Boldo and Thi Minh Tuyen Nguyen. Proofs of numerical programs when the compiler optimizes. Innovations in Systems and Software Engineering, 7:151-160, 2011. [ bib ] |
| [5] | Sylvie Boldo. Floats & Ropes: a case study for formal numerical program verification. In 36th International Colloquium on Automata, Languages and Programming, volume 5556 of Lecture Notes in Computer Science - ARCoSS, pages 91-102, Rhodos, Greece, July 2009. Springer. [ bib ] |
| [6] | Sylvie Boldo and Guillaume Melquiond. Emulation of FMA and Correctly-Rounded Sums: Proved Algorithms Using Rounding to Odd. IEEE Transactions on Computers, 57(4):462-471, 2008. [ bib | full paper on HAL | PDF ] |