Certified and Symbolic-Numeric Computation

May 22 to 26, 2023

ENS de Lyon, site Descartes, room D2 034 from Monday to Wednesday.

ENS de Lyon, site Monod, Amphi B from Thursday to Friday.

Practical information

Organizers: N. Brisebarre, A. Mahboubi, D. Pous, B. Salvy

The last twenty years have seen the advent of computer-aided proofs in mathematics and this trend is getting more and more important. This workshop aims at discussing the trust issues raised by the rise of computational mathematics, with an emphasis on numerical methods.

A first source of interest for such certified computations comes from theoretical parts of mathematics, such as dynamical systems or number theory, where the need for formalized definitions, and for proofs that can be checked computationally, has brought a lot of attention to formal proof systems. A typical example, in analytic number theory, is the recent proof of the ternary Goldbach conjecture by Helfgott, where a key part was played by a recent library for ball arithmetic, which relies heavily on computer algebra; the ultimate correctness guarantee can be achieved with the use of a formal proof system. Another source of interest comes from areas where numerical safety is critical, such as in autonomous vehicles, drones, or robust space mission design. There also, first interesting results have been obtained.

Unfortunately, most of the time, the necessary certification or formal verification routines are not easily available (or do not even exist). This is partly due to the fact that this field is still fairly recent but, actually, the main reasons are that the related scientific issues are difficult: algorithms returning certified error bounds are often terribly inefficient; obtaining formally verified implementations using a proof assistant requires a lot of manpower, and good backbone libraries.

The workshop will combine talks on recent proofs of mathematical results, where some level of certified computation played a crucial role, with overviews of the state-of-the-art on fast and stable numerical computations on computations returning certified numerical results, i.e., where an error bound is part of the output; on formally verified implementations for performing the aforementioned computations. The aim is to bring together experts from computer algebra, computer arithmetic, certified analysis and formal proof systems and practitioners of certified proofs in various parts of mathematics, so that they can exchange and interact on those issues that are at the interface between their areas.

Contact: csnc2023@ens-lyon.fr

Preliminary Program

    Monday 22/05/2023 (site Descartes, room D2 034)
10:30-11:20 Welcome breakfast/coffee
11:20-11:30 Presentation of the week
11:30-12:30 Mioara Joldes
Ten years of Space Junk and related Symbolic-Numeric Computations The goal is to give an overview of some works (and future challenges) related to the orbital collision risk assessment and mitigation strategies. The focus will be on the current and potential role of symbolic-numeric computations for such critical systems. In particular, we discuss about efficient and reliable methods for the evaluation of integrals which model the orbital collision probability between an active satellite and a space debris, whose position and velocity are only approximately known. Our approach exploits the algorithmic properties of holonomic functions, providing an evaluation that is not only reliable (the number of guaranteed correct digits is user-input) but also faster than traditional quadrature schemes. Firstly implemented and tested on a very large number of practical cases by CNES (French Space Agency), our algorithm has recently been embedded on board on the ESOC OPS-SAT 3-Units CubeSat satellite. This talk is based on joint works with D. Arzelier, F. Bréhard, M. Masson, J.-B. Lasserre, B. Salvy, R. Serra.
Slides
12:30-13:00 Yves Bertot
Formal proofs for trajectory computation in the plane with straight obstacles Our goal is to describe smooth trajectories for robots, so that these robots don't have to stop to change direction. Several formats of trajectories could be used, but we decided to focus on trajectories given by Bézier curves. It happens that these curves have mathematical properties that make it easy to verify formally that there are no collisions. Work in collaboration with Quentin Vermande (ENS, Paris) and Reynald Affeldt (AIST, Tokyo, Japan).
Slides
13:00-15:00 Lunch break
15:00-16:00 Guillaume Melquiond
Numerical Computations and Formal Proofs The main role of a system like Coq is to verify all the details of a proof written by the user using a formal language. Using such a proof assistant offers an unmatched confidence in the theorem statements, at the expense of a huge and tedious work by the user. While this approach is usually applied to symbolic reasoning, this talk will show how one can formalize mathematical theorems whose proofs rely on numerical computations. The first step is to implement arithmetic algorithms from the ground up in the logic of Coq: integer arithmetic, floating-point arithmetic, interval arithmetic, Taylor models. Once they have been formally verified, these numerical algorithms can be used inside formal proofs to alleviate the user proof effort. Moreover, they pave the way to using Coq, not only as proof assistant, but also as a computer algebra system: global optimization, root finding, proper and improper definite integrals, plots, and so on.
Slides
16:00-16:30 Discussion
16:30Coffee break
    Tuesday 23/05/2023 (site Descartes, room D2 034)
09:30-10:30 Jordi-Lluis Figueras
Existence of invariant tori in the large: from normally hyperbolic to lagrangian In this talk I plan to show some of the results we have been able to develop in the context of validating the existence of invariant tori in different contexts: from hyperbolic tori in skew product systems, to KAM tori in both twist maps and hamiltonian systems. All our results are looking at being able to prove the existence of these objects for systems far from the perturbative regime. Moreover, I will try to highlight during my talk some personal reflections on this topic, mathematics, and computer assisted proofs. This work has been developed in several projects in collaboration with Alex Haro and Alejandro Luque.
Slides
10:30-11:00 Tomáš Skřivan
Scientific Computing in Lean 4 Scientific computing has become increasingly complex, with one of the challenges being the translation of mathematical theory into computer code. The advanced mathematical concepts used in the theory are often difficult to express directly in code, leading to a disconnect between the theory and the resulting code. This can cause errors and make the code more difficult to understand. To address this challenge, we propose using an interactive theorem prover to bridge the gap between theory and code. Users can specify the problem, and then interactively modify the specification into executable code. For instance, the user may specify finding an initial condition for an ODE to minimize a certain function at a later time. Using specialized tactics, the user can then formulate corresponding adjoint problem, select a method for minimization, choose a time stepping scheme for solving differential equations, or apply symbolic or automatic differentiation. We use the Lean 4 programming language, which is well-suited for this task as it is both a general-purpose programming language and an interactive theorem prover. Furthermore, it has an extensive library of already formalized mathematics. Our current focus is on verified symbolic and automatic differentiation, with a particular emphasis on the comprehensive support for differentiating higher-order functions. This for example allows for symbolic variational calculus or formulation of adjoint problems. Our ultimate goal is to create a system that can be used by a wide audience to help them select the best computational method for their problems.
Slides
11:00-11:30 Coffee break
11:30-12:30 John Harrison
Verified arithmetic for cryptography I will describe some recent work developing a library of formally verified primitives for integer arithmetic, designed specifically for cryptographic applications. I will first describe the specific needs of this application domain, and in particular the importance of "constant-time" operations, a somewhat misleading term that I will try to explain accurately. I will then cover a few highlights of the algorithm design and formal verifications, and compare with related approaches.
Slides
12:30-13:00 Maria Luiza Costa Vianna
A Geometric Approach to the Coverage Measure of the Area Explored by a Robot Full coverage of an area of interest is a common task for an autonomous robot. Estimating the area explored by the robot is indeed essential for determining if path-planning algorithms lead to complete coverage. In this work, using a set membership approach, we propose a method for a guaranteed estimation of the area explored by an autonomous robot. The proposed algorithm is able to determine how many times each portion of the space has been sensed by the robot using a novel approach based on topological properties of the environment that has been scanned, and more precisely an estimation of certain winding numbers. This property is useful for localization inside homogeneous environments, e.g. the underwater environment, and assessment for potential revisiting missions. We demonstrate the efficiency of the presented approach on a real dataset acquired by an autonomous underwater robot.
Slides
13:00-15:00 Lunch break
15:00-16:00 Jean-Bernard Lasserre
The Christoffel function: Some applications in data analysis, approximation, and connections We briefly describe the Christoffel function, a well-know tool in approximation theory and orthogonal polynomials, but apparently overlooked in data analysis and data mining. It turns out that its remarkable properties make the CF an efficient and easy-to-use tool for some problems in data analysis (e.g. outlier detection, support inference). We will also reveal (in the author's opinion some surprising) connections with other domains of mathematics, including certificates of positivity in real algebraic geometry, optimisation and convex duality, Pell's polynomial equation.
Slides
16:00-16:30 Discussion
16:30Coffee break
    Wednesday 24/05/2023 (site Descartes, room D2 034)
09:30-10:30 Jason Mireles James
The FFT and computer assisted proofs for nonlinear functional equations I will discuss the use of the FFT as a component in computer assisted proofs for nonlinear problems. The talk will focus on arguments framed in Banach spaces (algebras) of rapidly decaying Fourier or Chebyshev sequences. Validated numerical methods which use interval arithmetic to obtain rigorous enclosures for the DFT/FFT are well known. This talk focuses on the analysis in the tail/truncation error estimates necessary for computer assisted proofs based on a posteriori analysis of nonlinear problems like boundary value problems for differential equations, and functional equations coming from the parameterization method. Using the FFT for such problems is a step toward developing general purpose software.
Slides
10:30-11:00 Laurence Rideau
Formalization of Lange & Rump's proof of error estimation for iterated sums of floating point numbers We present our formalization in Coq/Flocq of the Lange & Rump's result on error estimation for iterated perturbed sums of real numbers described in their paper "Error estimates for the summation of reals numbers with application to floating-point summation". Since this result can also be applied to the summation of double-double numbers, this error estimate has been widely used in our work on the accurate calculation of Euclidean described in our paper "Accurate calculation of Euclidean Norms using Double-word arithmetic". We show how we stated the result of Lange & Rump in Coq and how we adapted the paper proof to its use for the Euclidean norm.
Slides
11:00-11:30 Coffee break
11:30-12:30 Patrick Massot
12:30-13:00 Jean-Claude Yakoubsohn
High order methods for the SVD In this talk, we present a class of high order methods to approximate the singular value decomposition of a given complex matrix (SVD). To the best of our knowledge, only methods up to order three appear in the the literature. A first part is dedicated to define and analyse this class of method in the regular case, i.e., when the singular values are pairwise distinct. The construction is based on a perturbation analysis of a suitable system of equations associated to the SVD (SVD system). More precisely, for a given integer $p$, we define a sequence which converges with an order $p+1$ towards the left-right singular vectors and the singular values if the initial approximation of the SVD system satisfies a condition which depends on three quantities: the norm of initial approximation of the SVD system, the greatest singular value and the greatest inverse of the modulus of the difference between the singular values. From a numerical computational point of view, this furnishes a very efficient simple test to prove and certify the existence of a SVD in neighbourhood of the initial approximation. The second part of this study extends the method in the general case, i.e., when there are clusters of singular values. Moreover numerical experiments confirm the theoretical results both in the regular case of distinct singular value and in the singular case of multiple or clustered singular values.
Slides
13:00 Lunch, followed by free afternoon
19:30 Dinner at Restaurant Py, 16 cours Vitton, 69006 Lyon
    Thursday 25/05/2023 (site Monod, Amphi B)
09:30-10:30 Manuel Eberl
Some new tricks for formalising advanced mathematics In this talk, I will show a glimpse of an ongoing Isabelle/HOL formalisation project involving analytic number theory and complex analysis. In particular, I will highlight a few tools we had to build inside Isabelle to make solve some tricky aspects. Specifically: 1. Computational aspects like limits and series expansions that are often omitted on paper or delegated to a computer algebra system; 2. Geometric problems that seem trivial in pen-and-paper mathematics but become very painful in a theorem prover: winding numbers and tweaking integration contours to avoid "bad points".
Slides
10:30-11:00 Joel Dahne
Cusped waves and special functions In this talk I'll present a proof of the existence of a periodic highest, cusped, traveling wave solution to a family of equations coming from fluid mechanics. The proof is to a large extent computer assisted and the focus will be on the tools needed for the computations. A class of special functions known as the Clausen functions turns out to be of great importance. This is joint work with Javier Gómez-Serrano.
Slides
11:00-11:30 Coffee break
11:30-12:30 Michael Plum
Computer-assisted proofs for elliptic problems on bounded and unbounded domains Many boundary value problems for semilinear elliptic partial differential equations allow very stable numerical computation of approximate solutions, but are still lacking analytical existence proofs. In the lecture, a method is proposed 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 Newton-Kantorovich-type fixed-point argument which takes all numerical errors into account, and thus gives a rigorous mathematical proof. An important tool used in the method consists in the computation of eigenvalue bounds for differential operators. The method is used to prove existence and multiplicity statements for many specific examples of boundary value problems on bounded and on unbounded domains, including cases where purely analytical methods had not been successful.
Slides
12:30-13:00 Pierre Roux
ValidSDP: Coq proofs of 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.
Slides
13:00-15:00 Lunch break
15:00-16:00 Fredrik Johansson
Computing special functions using integral representations Numerical quadrature of integral representations is a powerful approach to computing special functions. It offers the possibility to obtain precise certified error bounds and is especially useful when one has to deal with large or complex parameters. This talk will give a brief introduction to different techniques and problems and discuss some recent implementation results.
Slides
16:00-16:30 Discussion
16:30Coffee break
    Friday 26/05/2023 (site Monod, Amphi B)
09:30-10:30 Daniel Wilczak
Rigorous computation of Poincaré maps Many phenomena of continuous-time dynamical systems can be efficiently computed or validated by discretization via Poincaré maps. These include and are not limited to proving chaos, connecting orbits, homoclinic/heteroclinic tangencies, various bifurcations (also global), even existence of hyperbolic attractors. It turns out that obtained enclosures for Poincaré maps can be significantly reduced by proper choice of Poincaré sections. Even in the case when the choice of Poincaré section is limited (for instance due to some engineering reasons or presence of symmetries which should be preserved) we can still manipulate coordinate system in which we represent the arguments and values of Poincaré maps. In the talk we will show that the optimal choice of Poincaré section nearby periodic orbit is related to left eigenvectors of the derivative of Poincaré map at a periodic point. We will also give an algorithm for efficient computation of Poincaré map in a given coordinate system that takes into account internal representation of solutions in an ODE solver. The algorithms are implemented and freely available as a part of the CAPD library. This is joint work with Tomasz Kapela and Piotr Zgliczyński.
Slides
10:30-11:00 Érik Martin-Dorel
Hardware floating-point computations in Coq Proof assistants like Coq and its Flocq library offer various models of floating-point arithmetic. These models proved useful to formally verify some floating-point algorithms and their implementations, such as optimizations in the verified CompCert C compiler. Floating-point arithmetic can also be used inside proof assistants to perform formal proofs of numerical results. This approach is instrumental in the interval arithmetic proofs carried out by the CoqInterval library. The computation capabilities of Coq make it very attractive to perform this kind of proofs by reflection. Unfortunately, until now, these floating-point computations were performed by emulation, using integer computations, not taking advantage of the floating-point units available in processors. This paper presents the implementation of hardware floating-point arithmetic within the Coq proof assistant, their link with the existing Flocq formalization of floating-point arithmetic and their use in two libraries to perform efficient proofs by reflection of numerical goals. Benchmarks show a speed-up of at least one order of magnitude.
Slides
11:00-11:30 Coffee break
11:30-12:30 Jean-Michel Muller
Obtaining error bounds that are certain, sharp… and whose proof is trustable: the curse of long and boring proofs We are interested in obtaining very sharp (indeed: asymptotically optimal) and certain (i.e., no « $+ O(u^k)$ » terms) error bounds for floating-point algorithms of medium size (say, less than around 20 operations). Unfortunately, this seems to imply that the proofs of these algorithms become long and tedious, so that almost nobody reads them in detail: the consequence is that it is not unlikely that they contain errors, that can remain unnoticed for years. We illustrate this problem with examples taken from computer arithmetic: addition and multiplication of « double word » numbers, and evaluation of the hypotenuse ($\sqrt{x^2+y^2}$) function. We discuss what computer algebra and formal proof bring to us, and the medium-term implication on the very notion of « publishing a proof » in an article.
Slides
12:30-13:00 Discussion
13:00 Lunch and end of the workshop

Participants

Code of Conduct

This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No. 101001995).

This workshop was also supported in part by the ANR Nuscap.