June 15th, 2023 at 10:15 am -- Marc Mezzarobba (CNRS, LIX, MAX)

Asymptotic Expansions with Error Bounds for Solutions of Linear
Recurrences

When a sequence (u(n)) of real or complex numbers satisfies a linear recurrence relation with polynomial coefficients, it is usually routine to determine its asymptotic behavior for large n. Well-known algorithms
and readily available implementations are often able, given a recurrence satisfied by (u(n)) and some additional information on the particular solution, to compute an explicit asymptotic expansion

up to any desired order r. If, however, one wishes to prove an inequality satisfied by u(n) for all n, a big-Oh error term is not sufficient and an explicit error bound on the difference between the sequence and its asymptotic approximation is required. In this talk, I will present a practical algorithm for computing such bounds, under the assumption that the generating series of the sequence (u(n)) is solution of a differential equation with regular (Fuchsian) dominant singularities. I will show how it can be used to verify the positivity of a certain explicit sequence, which T. Yu and J. Chen recently proved to imply uniqueness of the surface of genus one in R^{3} of minimal bending energy when the isoperimetric ratio is prescribed.

This is based on joint work with Ruiwen Dong and Stephen Melczer.

March 16th, 2023 at 10:15 am -- Fredrik Johansson (INRIA Bordeaux)

Faster computation of elementary functions
Over a decade ago, Arnold Schönhage proposed a method to compute elementary functions (exp, log, sin, arctan, etc.) efficiently in "medium precision" (up to about 1000 digits) by reducing the argument using linear combinations of pairs of logarithms of primes or Gaussian primes. We generalize this approach to an arbitrary number of primes (which in practice may be 10-20 or more), using an efficient algorithm to solve the associated Diophantine approximation problem. Although theoretically slower than the arithmetic-geometric mean (AGM) by a logarithmic factor, this is now the fastest algorithm in practice to compute elementary functions from about 1000 digits up to millions of digits, giving roughly a factor-two speedup over previous methods. We also discuss the use of optimized Machin-like formulas for simultaneous computation of several logarithms or arctangents of rational numbers, which is required for precomputations.

February 2nd, 2023 at 10:15 am -- Paul Zimmermann (INRIA Bordeaux)

Le projet CORE-MATH
Le projet CORE-MATH vise à fournir des implantations de référence avec arrondi correct des fonctions mathématiques. L'objectif est de produire des implantations efficaces pour intégration dans les bibliothèques mathématiques actuelles (libms), mais aussi de faire pression sur la prochaine révision du standard IEEE 754 (autour de 2029) pour imposer l'arrondi correct des fonctions mathématiques. Je décrirai l'état d'avancement du projet, notamment avec l'ajout des nouvelles fonctions du standard C23, et j'indiquerai les différentes manières de contribuer pour les membres du GT Éval.

January 10th, 2023 at 2:00 pm -- Harald Helfgott (Göttingen, Germany)

Calculs rigoureux, un brin de preuves automatiques, et l'espoir des preuves formelles : une miscellanée sur des thèmes de
Goldbach (faible)

January 27th, 2022 at 10:15 am -- Éric Goubault (LIX, École Polytechnique)

Verification of ReLU neural networks with tropical polyhedra

In this presentation, we are going to discuss the problem of range analysis for feedforward neural networks, which is a basic primitive for applications such as robustness of neural networks, compliance to specifications and reachability analysis of neural-network feedback systems. Our approach focuses on ReLU (rectified linear unit) feedforward neural nets that present specific difficulties: approaches that exploit derivatives do not apply in general, the number of patterns of neuron activations can be quite large even for small networks, and convex approximations are generally too coarse. In this presentation, we will employ set-based methods and abstract interpretation that have been very successful in coping with similar difficulties in classical program verification. We will present an approach that abstracts ReLU feedforward neural networks using tropical polyhedra. We will show that tropical polyhedra can efficiently abstract ReLU activation function, while being able to control the loss of precision due to linear computations. We show how the connection between ReLU networks and tropical rational functions can provide approaches for range analysis of ReLU neural networks.
This is joint work with Sylvie Putot.

December 16th, 2021 at 10:15 am -- Stef Graillat (PEQUAN, LIP6, Sorbonne Université)

On a compensated Ehrlich-Aberth method for the accurate computation of all polynomial roots

In this talk, we will use the complex compensated Horner’s method to derive a compensated Ehrlich-Aberth method for the accurate computation of all roots of a polynomial. In particular, under suitable conditions, we will show that the limiting accuracy for the compensated Ehrlich-Aberth iterations is as accurate as if computed in twice the working precision and then rounded into the working precision. Moreover, we will present a running error bound for the complex compensated Horner’s and use it to form robust stopping criteria for the compensated Ehrlich-Aberth iterations. Finally, extensive numerical experiments will illustrate that the backward and forward errors of the root approximations computed via the compensated Ehrlich-Aberth method are similar to those obtained with a quadruple precision implementation of the Ehrlich-Aberth method with a significant speed-up in terms of the computation time.

November 18th, 2021 at 3:00 pm -- Jan Verschelde (Dpt of Mathematics, Statistics and Computer, University of Illinois at Chicago, U.S.A.)

Least Squares on GPUs in Multiple Double Precision

Graphics Processing Units (GPUs) are well suited to offset the cost overhead caused by multiple double precision. Code generated by the CAMPARY software is applied to accelerate the solving of linear systems in the least squares sense in double double, quad double, and octo double precision. Thanks to the high Compute to Global Memory Access (CGMA) ratios of multiple double arithmetic, teraflop performance is already attained running the double double Householder QR on 1,024-by-1,024 matrices, on the NVIDIA P100 and the V100 GPUs. In doubling the precision from double double to quad double and from quad double to octo double, the observed cost overhead factors are lower than the factors predicted by the arithmetical operation counts.

October 7th, 2021 at 10:15 am -- Michael Plum (Fakultät für Mathematik, Karlsruher Institut für Technologie, Karlsruhe, Deutschland)

Computer-assisted existence and multiplicity proofs for semilinear elliptic boundary value problems

Many boundary value problems for semilinear elliptic partial differential equations allow very stable numerical computations of approximate solutions, but are still lacking analytical existence proofs. In this lecture, we propose a method which exploits the knowledge of a "good" numerical approximate solution, in order to provide a rigorous proof of existence of an exact solution close to the approximate one. This goal is achieved by a fixed-point argument which takes all numerical errors into account, and thus gives a mathematical proof which is not "worse" than any purely analytical one. A crucial part of the proof consists of the computation of eigenvalue bounds for the linearization of the given problem at the approximate solution. The method is used to prove existence and multiplicity statements for several specific examples, including cases where purely analytical methods had not been successful.

July 1st, 2021 at 10:15 am -- Sheehan Olver (Department of Mathematics, Imperial College London, United Kingdom)

Infinite Linear Algebra + Interval Arithmetic

This talk is designed as a bit of a mathematical magic show: we will live demo Julia packages that allow the construction of infinite-dimensional vectors and matrices, infinite matrix factorisation, solving infinite-dimensional linear systems, and even computation of spectrum. This methodology is also applicable to solving linear ordinary and partial differential equations and singular integral equations. The “grand reveal” is that many of the techniques also work with interval arithmetic, almost for free. One can, for example, compute interval bounds on zeros of Bessel functions by simply specifying the 3-term recurrence they satisfy. Peeling back the curtains, we will describe how underlying structure in the operators makes this possible, but also remaining gaps that mean that the leap to interval arithmetic is not quite as rigorous as it appears to be, and can in certain cases fail spectacularly.

June 17, 2021 at 10:15 am -- Guillaume Melquiond (Toccata, INRIA Paris Saclay)

Plotting in a formally verified way

An invaluable feature of computer algebra systems is their ability to plot the graph of functions. Unfortunately, when one is trying to design a library of mathematical functions, this feature often falls short, producing incorrect and potentially misleading plots, due to accuracy issues inherent to this use case. This work investigates what it means for a plot to be correct and how to formally verify this property. The Coq proof assistant has thus been turned into a tool for plotting function graphs that are guaranteed to be correct, by using reliable polynomial approximations. This feature is provided as part of the CoqInterval library.

May 20, 2021 at 10:15 am -- Joel Dahne (Uppsala Univ., Sweden)

A computer assisted counterexample to Payne’s nodal line conjecture with few holes

Payne conjectured in 1967 that the nodal line of the second Dirichlet eigenfunction must touch the boundary of the domain. In their 1997 breakthrough paper, Hoffmann-Ostenhof, Hoffmann-Ostenhof and Nadirashvili proved this to be false by constructing a counterexample in the plane with an unspecified, but large, number of holes and raised the question of the minimum number of holes a counterexample can have. In this talk I will present a computer assisted counter example with 6 holes.

It’s joint work with both Javier Gómez-Serrano and Kimberly Hou.