2016 | ELEFFAN

2016 | ELEFFAN

Axe : SciLex
Sujet : Stabilité(s): liens entre l’arithmétique flottante et l’analyse numérique
Directeurs : Sylvie Boldo, Inria et Alexandre Chapoutot, ENSTA ParisTech
Institutions : Inria et ENSTA ParisTech
Laboratoire Gestionnaire : Inria
Doctorant : Florian Faissole
Début : 01/10/2016
Productions scientifiques :

  • 2019
    • Journal paper
      • Round-off error and exceptional behavior analysis of explicit Runge-Kutta methods. Sylvie Boldo, Florian Faissole, and Alexandre Chapoutot. Accepted for publication in IEEE Transactions on Computers, 8 pages, April 2019.
    • Conference paper
      • Formalisation en Coq des erreurs d’arrondi de méthodes de Runge-Kutta pour les systèmes matriciels. Florian Faissole. In 18èmes journées Approches Formelles dans l’Assistance au Développement de Logiciels, pages 19-26, Toulouse, France, June 2019.
    • Poster communication
      • Formalizing Loop-Carried Dependencies in Coq for High-Level Synthesis. Florian Faissole, George A. Constantinides, and David Thomas. Poster session of 27th IEEE Annual International Symposium on Field-Programmable Custom Computing Machines, San Diego, United States of America, April 2019.
  • 2018
    • Conference papers
      • A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers, Sylvie Boldo, Florian Faissole, Vincent Tourneur, 25th IEEE Symposium on Computer Arithmetic, Jun 2018, Amherst, MA, United States
      • Preuves constructives de programmes probabilistes, Florian Faissole, Bas Spitters, JFLA 2018 – Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-Mer, France. 2018, 29èmes Journées Francophones des Langages Applicatifs. 〈https://www.lri.fr/~sboldo/JFLA18/〉
      • Définir le fini : deux formalisations d’espaces de dimension finie, Florian Faissole, JLFA 2018 – Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-mer, France. pp.1-6, 2018, 29èmes Journées Francophones des Langages Applicatifs
  • 2017
    • Conference papers
      • Formalization and closedness of finite dimensional subspaces, Florian Faissole, SYNASC 2017 – 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Sep 2017, Timișoara, Romania. pp.1-7
      • Round-off Error Analysis of Explicit One-Step Numerical Integration Methods, Sylvie Boldo, Florian Faissole, Alexandre Chapoutot, 24th IEEE Symposium on Computer Arithmetic, Jul 2017, London, United Kingdom.〈http://arith24.arithsymposium.org/〉.〈10.1109/ARITH.2017.22〉
      • Preuve formelle du théorème de Lax–Milgram, Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero, 16èmes journées Approches Formelles dans l’Assistance au Développement de Logiciels, Jun 2017, Montpellier, France. 〈http://afadl2017.imag.fr/〉
      • Synthetic topology in HoTT for probabilistic programming, Florian Faissole, Bas Spitters, The Third International Workshop on Coq for Programming Languages (CoqPL 2017), Jan 2017, Paris, France. 〈http://conf.researchr.org/track/POPL-2017/CoqPL-2017-papers〉
      • A Coq formal proof of the Lax–Milgram theorem, Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero, 6th ACM SIGPLAN Conference on Certified Programs and Proofs, Jan 2017, Paris, France. 〈http://cpp2017.mpi-sws.org/〉. 〈10.1145/3018610.3018625〉
    • Poster communications
      • Synthetic topology in homotopy type theory for probabilistic programming, Florian Faissole, Bas Spitters, PPS 2017 – Workshop on probabilistic programming semantics , Jan 2017, Paris, France. pp.3 BibTex

Ressources : Autre page du projet ELEFFAN — Page web de Florian Faissole

Contexte : Ce sujet se situe à l’interface entre l’informatique et les mathématiques appliquées. La partie informatique est prépondérante car il s’agit ici de considérer des algorithmes issus de l’analyse numérique et de vérifier leur bon comportement sur ordinateur. Ce comportement, prouvé en supposant que les calculs sont parfaits, pourrait être mis en défaut par les problèmes d’arrondis et de
dépassements de capacité dûs aux calculs en arithmétique flottante.

Objectifs scientifiques : Les calculs sur ordinateur créent des erreurs à chaque calcul qui peuvent s’accumuler pour donner un résultat complètement faux dans certains cas pathologiques. Cette thèse a pour but d’éclaircir le lien entre deux notions: la stabilité au sens de l’analyse numérique et la stabilité au sens de l’arithmétique flottante. En arithmétique flottante, un algorithme est stable si, sur des entrées proches, il fournit des sorties proches. Le ratio entre la différence des entrées et la différence des sorties est appelé le conditionnement, et il caractérise la stabilité d’une fonction. En analyse numérique, la stabilité a un autre sens. Pour les équations aux dérivées partielles, cela signifie que les valeurs de la solution ne divergent pas. Pour les équations aux dérivées ordinaires, cela signifie la stabilité du système dynamique, et souvent la stabilité de Lyapunov. À noter qu’il existe également une notion de sensibilité aux données pour les schémas d’intégration numérique appelé “zero-stability” qui a beaucoup de ressemblance avec la notion de stabilité dans les nombres flottants. Cette thèse pourra mettre ce lien en évidence avant de considérer les autres types de stabilité des schémas numériques.

Perspectives : Les mathématiciens pensent qu’un schéma stable au sens de la dynamique est numériquement stable. Nous pensons que cette recette de cuisine est vraie, et nous aimerions la prouver formellement. L’idée est que les erreurs numériques vont se compenser à cause de la forme particulière qu’a un schéma numérique stable et convergent et donc que le calcul va globalement « bien » se passer.
Les erreurs d’arrondi locales peuvent facilement être bornées à chaque étape par les propriétés de l’arithmétique flottante spécifiées par la norme IEEE-754 (aux fonctions trigonométriques près). C’est particulièrement simple ici car les valeurs sont bornées grâce à la stabilité du schéma. Une difficulté sera de borner les erreurs finales au bout d’un grand nombre d’itérations. En fait, il semble que les compensations exhibées dans un cas particulier soient plus générales et s’appliquent en fait à une large classe de schémas numériques stables. Une autre difficulté est que le résultat doit être assez général pour s’appliquer à différents types de schémas, mais assez précis pour donner des bornes d’erreur utilisables sur les erreurs d’arrondi.