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.