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.
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 ComputationsThe 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. |
12:30-13:00 | Yves Bertot | Formal proofs for trajectory computation in the plane with straight obstaclesOur 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). |
13:00-15:00 | Lunch break | |
15:00-16:00 | Guillaume Melquiond | Numerical Computations and Formal ProofsThe 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. |
16:00-16:30 | Discussion | |
16:30 | Coffee 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 lagrangianIn 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. |
10:30-11:00 | Tomáš Skřivan | Scientific Computing in Lean 4Scientific 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. |
11:00-11:30 | Coffee break | |
11:30-12:30 | John Harrison | Verified arithmetic for cryptographyI 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. |
12:30-13:00 | Maria Luiza Costa Vianna | A Geometric Approach to the Coverage Measure of the Area Explored by a RobotFull 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. |
13:00-15:00 | Lunch break | |
15:00-16:00 | Jean-Bernard Lasserre | The Christoffel function: Some applications in data analysis, approximation, and connectionsWe 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. |
16:00-16:30 | Discussion | |
16:30 | Coffee 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 equationsI 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. |
10:30-11:00 | Laurence Rideau | Formalization of Lange & Rump's proof of error estimation for iterated sums of floating point numbersWe 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. |
11:00-11:30 | Coffee break | |
11:30-12:30 | Patrick Massot | |
12:30-13:00 | Jean-Claude Yakoubsohn | High order methods for the SVDIn 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. |
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 mathematicsIn 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". |
10:30-11:00 | Joel Dahne | Cusped waves and special functionsIn 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. |
11:00-11:30 | Coffee break | |
11:30-12:30 | Michael Plum | Computer-assisted proofs for elliptic problems on bounded and unbounded domainsMany 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. |
12:30-13:00 | Pierre Roux | ValidSDP: Coq proofs of polynomial positivity using numerical solvers and floating-point computationsPolynomial 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. |
13:00-15:00 | Lunch break | |
15:00-16:00 | Fredrik Johansson | Computing special functions using integral representationsNumerical 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. |
16:00-16:30 | Discussion | |
16:30 | Coffee break | |
Friday 26/05/2023 (site Monod, Amphi B) | ||
09:30-10:30 | Daniel Wilczak | Rigorous computation of Poincaré mapsMany 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. |
10:30-11:00 | Érik Martin-Dorel | Hardware floating-point computations in CoqProof 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. |
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 proofsWe 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. |
12:30-13:00 | Discussion | |
13:00 | Lunch and end of the workshop |
Participants
- Johnson Daddy Audu
- Tülay Ayyıldız
- Yves Bertot
- Sylvie Boldo
- Alin Bostan
- Florent Bréhard
- Nicolas Brisebarre
- Cyril Cohen
- Maria Luiza Costa Vianna
- Joel Dahne
- Manuel Eberl
- Jordi-Lluís Figueras Romero
- Louis Gaillard
- Alexandre Guillemot
- Guillaume Hanrot
- John Harrison
- Nuwan Herath
- Alaa Ibrahim
- Claude-Pierre Jeannerod
- Fredrik Johansson
- Mioara Joldes
- Christina Katsamaki
- Pierre Lairez
- Jean Bernard Lasserre
- Assia Mahboubi
- Érik Martin-Dorel
- Patrick Massot
- Guillaume Melquiond
- Marc Mezzarobba
- Jason Mireles James
- Jean-Michel Muller
- Michael Plum
- Damien Pous
- Nathalie Revol
- Laurence Rideau
- Pierre Roux
- Kazuhiko Sakaguchi
- Bruno Salvy
- Tomas Skrivan
- Laurent Théry
- Arnaud Tisserand
- Warwick Tucker
- Anastasia Volkova
- Daniel Wilczak
- Jean-Claude Yakoubsohn
- Zafeirakis Zafeirakopoulos
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.