Journées FastRelax

05-07 Juin 2018

La réunion a eu lieu au centre Inria de Sophia Antipolis, en salle Coriolis (Bâtiment Galois). Comment venir ?

Programme

Mardi 5 Juin

Possibilité de déjeuner sur place.
14:00
Accueil
14:30
Florian Steinberg Interval computations and some computable analysis [support]
15:00
Florent Bréhard, A computer-assisted proof for a new lower bound on H(4) in Hilbert's sixteenth problem (joint work with N. Brisebarre and W. Tucker) [support]
15:30
Pause
16:00
Marc Mezzarobba, Truncation Bounds for Differentially Finite Series [support]
16:30
Laurent Théry, Comparison algorithms between binary64 and decimal64 floating-point numbers [support]
17:00
Discussions

Mercredi 06 Juin

9:30
Paul Zimmermann, On various ways to split a floating-point number (joint work with Jean-Michel Muller and Claude-Pierre Jeannerod) [article]
10:30
Pause
11:00
Manuel Eberl, Semi-Automatic Real Asymptotics in Isabelle/HOL [support]
11:30
Cyril Cohen, Formalization Techniques for Asymptotic Reasoning in Classical Analysis [support]
12:00
Déjeuner
14:00
Mioara Joldes et Denis Arzelier, Global Probability of Collision (joint works with F. Bréhard, J.-B. Lasserre and A. Rondepierre)
  1. Problem modeling via occupation measures
  2. On a moment inverse problem with D-finite functions
15:30
Pause
16:00
Damien Rouhling , Formal Proofs for Control and Robotics: A Case Study [support]
16:30
Discussions : Prolongation FastRelax
19:30
Dîner au restaurant "Les vieux murs" à Antibes

Jeudi 7 Juin

9:30
Pascal Molin, Calcul des périodes de courbes algébriques [support]
10:10
Fredrik Johansson, Numerical integration in arbitrary-precision ball arithmetic [support]
10:30
Yves Bertot, Distant decimals of PI [support]
10:50
Pause
11:10
Bruno Salvy , Generalized Hermite Reduction, Creative Telescoping and Definite Integration of D-Finite Functions
11:40
Erik Martin-Dorel, Global optimization in Coq: Present and future work in ValidSDP [support]
12:30
Fin des rencontres

Résumés

Cyril Cohen, Formalization Techniques for Asymptotic Reasoning in Classical Analysis

Formalizing analysis on a computer involves a lot of "epsilon-delta" reasoning, while informal reasoning may use some asymptotical hand-waving. Whether or not the arithmetic details are hidden using some abstraction like filters, a human user eventually has to break it down for the proof assistant anyway, and provide a witness for the existential variable "delta". We describe formalization techniques that take advantage of existential variables to delay the input of witnesses until a stage where the proof assistant can actually infer them. We use these techniques to prove theorems about classical analysis and to provide equational Bachmann-Landau notations. This partially restores the simplicity of informal hand-waving without compromising the proof. As expected this also reduces the size of proof scripts and the time to write them, and it also makes proofs more stable.

Laurent Théry, Comparison algorithms between binary64 and decimal64 floating-point numbers

We present a formalisation of the correctness of some comparison algorithms between binary64 and decimal64 floating-point numbers, using computation intensive proofs and a continued fractions library built for this formalisation.

Marc Mezzarobba, Truncation Bounds for Differentially Finite Series

I will present a flexible symbolic-numeric algorithm for computing bounds on the remainders of series solutions of linear ODEs with polynomial coefficients. Such bounds are useful in rigorous numerics, typically in rigorous versions of the Taylor method of numerical integration of ODEs. The algorithm fully covers the case of generalized series expansions at regular singular points. It is a key part of the rigorous Taylor method implemented in the Sage package ore_algebra, and experiments with the implementation show that it yields tight bounds in practice at an acceptable computational cost, even for equations of high order with coefficients of large degree.

Paul Zimmermann, On various ways to split a floating-point number

We review several ways to split a floating-point number, that is, to decompose it into the exact sum of two floating-point numbers of smaller precision. All the methods considered here involve only a few floating-point operations with rounding to nearest, including possibly the fused multiply-add (FMA). Applications range from the implementation of integer functions such as floor or round to ``scaling'' of calculations (such as sqrt(a^2+b^2)) to avoid spurious underflow and overflow.

This is a joint work with Claude-Pierre Jeannerod and Jean-Michel Muller.

Manuel Eberl, Semi-Automatic Real Asymptotics in Isabelle/HOL

Computer Algebra Systems can easily compute limits and asymptotic expansions of complicated real functions; interactive theorem provers, on the other hand, provide very little support for such problems and proving asymptotic properties of a function often involves long and tedious manual proofs.

In this talk, I will present my work about bringing automation for real-valued asymptotics to Isabelle/HOL using multiseries expansions. This yields a procedure to automatically prove limits and ‘Big-O' estimates of real-valued functions similarly to computer algebra systems like Mathematica and Maple – but while proving every step of the process correct.

Pascal Molin, Calcul des périodes de courbes algébriques

On décrit un algorithme efficace pour le calcul des périodes de courbes algébriques par intégration numérique, qui a été implanté dans le cadre de courbes superelliptiques y^m=f(x), ainsi que les problèmes à résoudre pour généraliser l'approche aux courbes algébriques générales.

Fredrik Johansson. Numerical integration in arbitrary-precision ball arithmetic.

We discuss arbitrary-precision numerical integration with rigorous error bounds in the framework of ball arithmetic. A new implementation has recently been added to the Arb library. Rapid convergence is ensured for piecewise complex analytic integrals by use of the Petras algorithm, which combines adaptive bisection with degree-adaptive Gaussian quadrature where error bounds are determined via complex magnitudes without evaluating derivatives. The code is general, easy to use, and efficient, often outperforming existing non-rigorous software.

Yves Bertot, Distant decimals of PI.

Three algorithms for computing distant decimals of PI have been studied in formal proofs. The first one is the BBP formula and its use in the computation of single remote hexadecimal digits.

The other two rely on arithmetic-geometric means and are related so that the computation of convergence speed for one relies on the other. We also study accumulated rounding error bounds.

Mioara Joldes et Denis Arzelier, Global Probability of Collision

The increasing number of space debris in Low Earth Orbits constitute a serious hazard for operational satellites. In this talk, we propose an exact and rigorous mathematical modeling for the general case of collision probability computation for multiple encounters between such objects. This theoretical formulation is based on the measure theory framework and the related developments on the generalized moment problem. It handles full generality, both with respect to the dynamics of the objects, the encounter duration, the number of objects involved, and the distribution of their initial state. The main ingredients of this modeling are: (1) lifting of the nonlinear dynamics into a linear equation of measures via Liouville’s equation; (2) posing a linear optimization problem on measures, whose objective function is exactly the sought probability of collision; (3) practically solving via a hierarchy of semi-definite optimization moment problems.

While this practical numerical way of solving LP problems on measures is well-known and applicable, in our case, important numerical issues have been identified. Firstly, the dimension of the general problem is currently prohibitive for SDP solvers. Secondly, several examples show that numerical results in low dimension do not achieve a good accuracy.

In the second part of this talk, we focus on some ongoing works which explore different strategies to mitigate these issues. Firstly, we discuss the approximate (but efficient) computation of higher order moments of some "nice" positive measure (whose density wrt Lebesque measure is holonomic). To compute recurrences for such moments, we use multivariate holonomic functions and creative telescoping. Secondly, we attempt to approximately reconstruct the support of the initial collision-prone states in a two-objects long-term encounter, by extending a method of J.B. Lasserre and M. Putinar which makes clever use of Stokes theorem. Given a finite number of numerically computed moments for a measure with holonomic density, and assuming a real algebraic boundary for the support, we discuss a preliminary result on an algorithmic method for obtaining the coefficients of a polynomial vanishing on this boundary.

This is joint work with F. Bréhard, D. Gueho, J-B. Lasserre, A. Rondepierre and in collaboration with CNES.

Florent Bréhard, A computer-assisted proof for a new lower bound on H(4) in Hilbert's sixteenth problem

We provide a computer-assisted proof for a new lower bound on H(4) in the Hilbert 16th problem, that is the maximum number of limit cycles that can occur in a polynomial planar vector field of degree 4. Indeed, we exhibit a quartic vector field for which we rigorously prove the existence of at least 24 limit cycles. Hilbert's 16th problem is part of Hilbert's famous list of 23 problems presented in 1900 at the International Congress of Mathematicians in Paris. The second part of this problem asks whether there exists, for each natural integer n, a finite upper bound H(n) on the number of limit cycles a polynomial planar vector field of degree n can have. For now, a proof of this conjecture seems out of reach, even for n = 2. A simpler version of this problem restricts the investigation to perturbed Hamiltonian systems. The upper bound Z(n) for such systems of degree n was proved to be finite for all n. A key ingredient is the Poincaré-Pontryagin theorem that relates the number of limit cycles with the number of zeros of so-called Abelian integrals along the level curves of the potential function associated to the Hamiltonian system.

The quartic system we investigate is not Hamiltonian but still integrable, so that the Poincaré-Pontryagin theorem still applies. Our work consists in approximating the Abelian integral associated to each monomial of the perturbation (as function of the energy level of the potential function), adjusting the coefficients to maximize the number of zeros of the resulting linear combination, and finally computing rigorous enclosures of the integral at various points to certify the number of sign changes. For that purpose, we use Rigorous Polynomial Approximations [1,2,3] via our free C library available here [4], which allows us to perform rigorous and efficient evaluations of the Abelian integral.

A formalization of this result in Coq is in progress, in order to avoid possible implementation errors that may lead to a wrong result. This is a joint work with Nicolas Brisebarre and Warwick Tucker.