Evaluation et Validation Automatique pour le calcul Flottant – EVA-Flo

Ce projet s'intéresse à la manière dont une formule mathématique (incluant des fonctions transcendantes et peut-être des itérations) se retrouve évaluée en virgule flottante dans un calculateur. Ce projet attaque cette question sous trois angles: comment évaluer une telle formule, comment automatiser la génération de code pour cette évaluation, comment valider la précision numérique du code obtenu. Il s'agit d'améliorer la situation actuelle, qui est la suivante. Un programmeur expert sait écrire un code de qualité tenant compte par exemple des propriétés mathématiques des fonctions utilisées, des ordres de grandeurs et de l'accumulation des erreurs d'arrondis, et de propriétés fines de l'arithmétique virgule flottante utilisée, mais ne dispose pas des outils permettant de transmettre cette expertise au compilateur. Le compilateur se contente d'assembler des opérateurs de base et des appels de fonctions de bibliothèques sans s'intéresser à la précision numérique du code produit. Quant à obtenir une garantie sur cette précision, c'est envisageable actuellement uniquement a posteriori, sur de tout petits codes, et de manière essentiellement manuelle. Notre approche sera de travailler en parallèle sur trois aspects : l'étude d'algorithmes d'évaluation de formules mathématiques (du point de vue précision et performance), la validation de tels algorithmes (notamment des aspects numériques) au cours de leur développement, afin de guider les choix algorithmiques, enfin l'automatisation de l'ensemble, point pour lequel la difficulté essentielle consiste à faire coopérer les composants utilisés pour chaque étape. Du point de vue algorithmique, on travaillera par exemple sur l'approximation d'une formule par un polynôme à une ou plusieurs variables. Si les mathématiques sont bien établies dans ce domaine, leur adaptation au monde du calcul flottant est souvent non triviale. Par exemple, il existe une grande variété de schémas d'évaluation d'un polynôme donné, certains minimisant les erreurs d'arrondis, d'autres maximisant le parallélisme, etc. De plus, si on peut construire le ``meilleur polynôme'' théorique d'approximation d'une fonction, dans un domaine et pour une norme donnés, obtenir le meilleure polynôme avec la contrainte que les coefficients sont exactement représentables en virgule flottante et en tenant compte de l'erreur d'arrondi due à l'évaluation du polynôme (et non plus seulement de l'écart entre la fonction et la valeur exacte que prend le polynôme) reste un problème ouvert, que l'on commence à attaquer sous divers angles. Outre cet aspect algorithmique fondamental, il s'agira essentiellement de généraliser et mécaniser une expertise acquise par les porteurs de projets, dans le cadre notamment de l'évaluation des fonctions élémentaires et de la géométrie algorithmique. Enfin, on cherchera à valider formellement la précision numérique du code final par rapport à la formule initiale. Une partie de l'automatisation est acquise, puisque des outils comme Coq, PVS ou HOL-light savent vérifier des preuve formelles incluant des aspects numériques. Toutefois ces outils ne rédigent pas la preuve, et notre apport sera de rechercher une classe de formules aussi large que possible pour laquelle cette rédaction d'une preuve de propriété numérique sera automatisable. Plus précisément, il s'agira de produire en parallèle le code évaluant la formule, et une preuve formelle d'une propriété de ce code, typiquement une borne de l'erreur totale entre le résultat du code et le résultat mathématique. Ici aussi, les porteurs du projet ont réalisé ce travail au cas par cas, et l'enjeu est de généraliser et d'automatiser. En général, l'automatisation complète avec garantie de solution optimale n'a pas de sens sans information supplémentaire sur le contexte de l'application, et il faudra formaliser ce qu'un outil a besoin de connaître en plus de la formule à implémenter. On pense naturellement au domaine d'entrée des valeurs et à la précis...