Journées FastRelax

29–31 mai 2017, Paris

La réunion aura lieu au LIP6, sur le campus de Jussieu, en salle 25-26/105 (1er étage, accès par les rotondes 25 ou 26). Comment venir ?

Programme

Lundi 29 mai

10:30
Accueil
11:00
Thomas Sibut-Pinote. Intégrales impropres en Coq.
12:00
Repas à L'Ardoise
13:30
Point sur les tâches à accomplir
14:30
Florent Bréhard. Résolution rigoureuse de systèmes d'équations différentielles linéaires couplées et applications en mécanique spatiale [support]
15:00
Florian Faissole. Erreurs d'arrondi des méthodes d'intégration numérique explicites. [support]
15:30
Damien Rouhling. A Formal Proof in Coq of LaSalle's Invariance Principle. [support]
16:00
Pause
16:30
Discussions

Mardi 30 mai

10:00
Sophie Bernard. Formalization of transcendence proofs : the omnipresence of polynomials. [support]
11:00
Discussions
12:30
Buffet sur place
14:00
Bruno Salvy. Fractions continues explicites pour des équations de type Riccati
14:30
Sylvie Boldo. Renormalisation d'expansions : une vérification formelle. [support]
15:00
Valentina Popescu. Implementation and performance evaluation of an extended precision floating-point arithmetic library for high-accuracy semidefinite programming [support]
15:30
Pause
16:00
Discussions
19:30
Dîner au Bouillon Racine

Mercredi 31 mai

10:00
Xavier Caruso. Calcul du logarithme p-adique.
11:00
Stef Graillat. Évaluation précise de polynômes et de fractions rationnelles.
11:30
Paul Zimmermann. Des calculs plus rapides sur 1 et 2 mots-machine dans GNU MPFR [support]
12:00
Repas à L'Ardoise
13:30
Raphaël Rieu-Helft. Une bibliothèque efficace et formellement prouvée pour les calculs sur grands entiers. [support]
14:00
Érik Martin-Dorel. A Reflexive Tactic for Polynomial Positivity using Numerical Solvers. [support]
15:00
Discussions
16:00
Fin des journées

Résumés

Sophie Bernard. Formalization of transcendence proofs : the omnipresence of polynomials.

The study of transcendental numbers really became active during the 19th century which was marked by four main results : the first ever proven transcendental number (Liouville), the transcendence of e, then pi, and finally the Lindemann-Weierstrass theorem. We present the formalization of these 3 last results, each of which follows the same proof structure. In particular, in both the algebra and analysis parts, polynomials are the building blocks of the proof, whether they be univariate or multivariate. This talk will then focus on the formalization in coq of these different kinds of polynomials and their properties, in the context of transcendence proofs.

Sylvie Boldo. Renormalisation d'expansions: une vérification formelle

Une brique de base du calcul sur les expansions flottantes est la renormalisation qui permet de "compresser une expansion". Cet exposé parlera d'une preuve formelle d'un tel algorithme qui a été semée d'embûches (erreur, dénormalisés, zéros intermédiaires).

Florent Bréhard. Résolution rigoureuse de systèmes d'équations différentielles linéaires couplées et applications en mécanique spatiale

Obtenir des bornes d'erreurs rigoureuses pour des solutions numériques d'équations différentielles ordinaires (EDO) est un enjeu de taille tant pour les applications critiques (aéronautique, aérospatial, médecine, etc.) que pour les preuves mathématiques assistées par ordinateur. Souvent, des problèmes non linéaires difficiles à étudier peuvent être linéarisés en équations différentielles ordinaires linéaires (EDOL) autour d'un point ou d'une trajectoire d'équilibre.

Nous présenterons un algorithme de validation a posteriori, qui étant donné une solution approchée d'une EDOL exprimée en base de Tchebychev, renvoie une borne d'erreur rigoureuse. Comme souvent en analyse numérique certifiée, le théorème du point fixe de Banach jouera un rôle clé. Nous verrons ensuite comment cette procédure peut s'étendre au cas vectoriel (système d'EDOL couplées). Enfin, nous illustrerons la méthode avec des exemples issus de la mécanique spatiale, comme le problème de rendez-vous ou le maintien à poste d'un satellite.

Florian Faissole. Erreurs d'arrondi des méthodes d'intégration numérique explicites.

Les équations différentielles ordinaires sont fréquemment étudiées dans le domaine du calcul scientifique. À l'exception de cas particuliers, il est généralement impossible de résoudre ces équations de façon exacte. C'est pourquoi des méthodes numériques sont utilisées pour obtenir une solution discrétisée. Nous nous intéressons à certaines de ces méthodes, comme la méthode d'Euler ou les méthodes de Runge-Kutta. Leur implémentation utilise des nombres à virgule flottante, ce qui peut conduire à une accumulation d'erreurs d'arrondi. Afin de garantir la précision de ces méthodes, nous proposons une analyse très fine des erreurs d'arrondis pour en expliciter des bornes raisonnables. Nous prenons en compte les propriétés mathématiques de telles méthodes et notamment la stabilité linéaire, une propriété garantissant leur bon comportement du point de vue mathématique.

Érik Martin-Dorel. A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations

Polynomial positivity over the real field is known to be decidable but even the best algorithms remain costly. An incomplete but often efficient alternative consists in looking for positivity witnesses as sum of squares decompositions. Such decompositions can in practice be obtained through convex optimization. Unfortunately, these methods only yield approximate solutions. Hence the need for formal verification of such witnesses. State of the art methods rely on heuristic roundings to exact solutions in the rational field. These solutions are then easy to verify in a proof assistant. However, this verification often turns out to be very costly, as rational coefficients may blow up during computations. Nevertheless, overapproximations with floating-point arithmetic can be enough to obtain proofs at a much lower cost. Such overapproximations being non trivial, it is mandatory to formally prove that rounding errors are correctly taken into account. We develop a reflexive tactic for the Coq proof assistant allowing one to automatically discharge polynomial positivity proofs. The tactic relies on heavy computation involving multivariate polynomials, matrices and floating-point arithmetic. Benchmarks indicate that we are able to formally address positivity problems that would otherwise be untractable with other state of the art methods.

This is a joint work with Pierre Roux that has been published at the CPP'2017 conference.

Valentina Popescu. Implementation and performance evaluation of an extended precision floating-point arithmetic library for high-accuracy semidefinite programming

Semidefinite programming (SDP) is widely used in optimization problems with many applications, however, certain SDP instances are ill-posed and need more precision than the standard double-precision available. Moreover, these problems are large-scale and could benefit from parallelization on specialized architectures such as GPUs. In this article, we implement and evaluate the performance of a floating-point expansion-based arithmetic library (CAMPARY) in the context of such numerically highly accurate SDP solvers. We plugged-in CAMPARY with the state-of-the-art SDPA solver for both CPU and GPU-tuned implementations. We compare and contrast both the numerical accuracy and performance of SDPA-GMP, -QD and -DD, which employ other multiple-precision arithmetic libraries against SDPA-CAMPARY. We show that CAMPARY is a very good trade-off for accuracy and speed when solving ill-conditioned SDP problems.

Raphaël Rieu-Helft. Une bibliothèque efficace et formellement prouvée pour les calculs sur grands entiers.

GMP est la bibliothèque de calcul en précision arbitraire la plus largement utilisée. Elle est écrite en C et en assembleur et met en oeuvre des algorithmes de pointe. Cet exposé présentera une bibliothèque pour les calculs sur grands entiers implémentée et formellement vérifiée avec la plateforme Why3. Elle met en œuvre les algorithmes de GMP pour les entrées de taille moyenne (moins de 1280 bits). L'usage d'un modèle mémoire dédié permet d'écrire du code Why3 qui ressemble très fortement au code C de GMP. La bibliothèque est extraite vers C, et le résultat est compatible avec GMP et compétitif en termes de performances.

Damien Rouhling. A Formal Proof in Coq of LaSalle's Invariance Principle

Stability analysis of dynamical systems plays an important role in the study of control techniques. LaSalle's Invariance Principle is a result about the asymptotic stability of the solutions to a nonlinear system of differential equations and several extensions of this principle have been designed to fit different particular kinds of system. We will present a formalization, in the Coq proof assistant, of a slightly improved version of the original principle. This is a step towards a formal verification of dynamical systems.

Bruno Salvy. Fractions continues explicites pour des équations de type Riccati

La plupart des C-fractions explicites classiques sont des cas particuliers de fractions continues dues à Euler et Gauss pour le quotient de séries hypergéométriques contiguës. Ces séries sont solutions d’équation de Riccati, à partir desquelles ces fractions continues peuvent être obtenues directement par une méthode due à Lagrange. Dans ce travail, nous abordons la méthode de Lagrange d’un point de vue symbolique, pour déterminer toutes les équations pour lesquelles elle donne des fractions continues explicites. Les résultats classiques sont ainsi obtenus de manière unifiée, ainsi que leurs q-analogues (des fractions continues dues à Heine). La méthode s’applique aussi aux équations de Riccati discrètes et fournit alors en cas particulier une fraction continue due à Brouncker sur la fonction Gamma. Il s’agit d’un travail joint avec Sébastien Maulat.

Paul Zimmermann. Des calculs plus rapides sur 1 et 2 mots-machine dans GNU MPFR

Dans un travail commun avec Vincent Lefèvre, nous avons optimisé les opérations de base de MPFR (addition, soustraction, multiplication, division, racine carrée) quand tous les opérandes ont la même précision, et que cette précision correspond à un ou deux mots-machine. Nous avons aussi implémenté un nouveau mode d'arrondi (arrondi fidèle). Tout cela sera disponible dans la version 4 de GNU MPFR.