The goal of a posteriori validation methods is to get a quantitative and rigorous description of some specific solutions of nonlinear equations, often ODEs or PDEs, based on numerical simulations. The general strategy consists in combining a priori and a posteriori error estimates, interval arithmetic, and a fixed point theorem applied to a quasi-Newton operator. Starting from a numerically computed approximate solution, one can then prove the existence of a true solution in a small and explicit neighborhood of the numerical approximation.

I will first present the main ideas behind these techniques on a simple example, then describe a rather general framework in which they can be applied, and finally showcase that these techniques can be adapted in a straightforward and efficient way to produce rigorous continuation results, allowing to prove the existence of branches of solutions, and to rule out bifurcations.

In this talk I will present the Hierarchy Builder Domain Specific Language for Coq, and illustrate its use in building measure theory and the Lebesgue measure in a concise way.

Designing an efficient yet accurate floating-point approximation of a mathematical function is an intricate and error-prone process. This warrants the use of formal methods, especially formal proof, to achieve some degree of confidence in the implementation. Unfortunately, the lack of automation or its poor interplay with the more manual parts of the proof makes it way too costly in practice. This talk revisits the issue by proposing a methodology and some dedicated automation, and applies them to the use case of a faithful binary64 approximation of exponential. The peculiarity of this use case is that the target of the formal verification is not a simple modeling of an external code, it is an actual floating-point function defined in the logic of the Coq proof assistant, which is thus usable inside proofs once its correctness has been fully verified. This function presents all the attributes of a state-of-the-art implementation: bit-level manipulations, large tables of constants, obscure floating-point transformations, exceptional values, etc. This function has been integrated into the proof strategies of the CoqInterval library, bringing a 20x speedup with respect to the previous implementation.

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

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

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.

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.

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.

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.

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.

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.

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.