Approximation rapide et fiable – Fast Relax

Le calcul numérique s'effectue de plus en plus efficacement, grace aux progrès du calcul haute performance et de bibliothèques numériques en amélioration constante. Cependant, dans la plupart des cas, la validité et la qualité des approximations qui sont produites est difficile, voire impossible, à établir. Pourtant, dans les applications critiques rencontrées par exemple dans les problèmes aérospatiaux, cette information est vitale.
Des réponses partielles sont apportées par les bibliothèques de calcul en précision arbitraire comme on en trouve dans les systèmes de calcul formel, par l'arithmétique d'intervalles, ou par les preuves formelles, mais l'approximation rapide et fiable reste un défi de recherche pour le long terme.

Dans ce projet, nous rassemblons des spécialistes de l'arithmétique des ordinateurs, des preuves formelles, du calcul formel, du calcul rigoureux et de la théorie du contrôle optimal. Notre but est de développer des preuves automatiques de valeurs numériques, avec des bornes d'erreur certifiée et raisonnablement fines, sans sacrifier l'efficacité. Les applications à la recherche de racines, à l'intégration numérique ou à l'optimisation globale peuvent toutes bénéficier de l'usage de nos résultats comme briques de base. Nous ambitionnons que notre travail pourra initier une tendance ``rapide et sûr'' dans la communauté du symbolique-numérique. Cela sera réalisé en développant des interactions entre nos disciplines, en concevant et en implantant des bibliothèques prototype, et en appliquant nos résultats à des problèmes concrets issus de la théorie du contrôle optimal.

Notre approche globale consiste en l'utilisation de calcul formel dans une phase de précalcul pour automatiser le calcul d'approximations et pour contrôler symboliquement toutes les erreurs numériques. L'approximation et la borne d'erreur obtenues à cette étape seront conçues pour être efficaces pour le stockage, la manipulation et l'évaluation dans les calculs numériques ultérieurs. Alors, les erreurs d'arrondi sont gérées via des calculs en précision multiple (mais modérée) et par de l'arithmétique d'intervalles. Des preuves formelles sont utilisées pour vérifier des certificats produits lors de la phase symbolique et pour prouver les procédures numériques de bas niveau. Cette approche est validée sur des applications cibles de la théorie du contrôle optimal.