NuSCAP

Journées de fin de première année

8 au 10 juin 2022, Salle des conférences du LAAS, Toulouse

Programme

• Mercredi 8 juin
• 9h00-10h00. Petit déjeuner
• 10h00-11h00. Jean-Bernard Lasserre, Le noyau de Christoffel-Darboux et la fonction de Christoffel : Applications en analyse de données, approximation et interpolation.
Résumé
Si le noyau de Christoffel-Darboux (CD) est bien connu en théorie de l'approximation et polynômes orthogonaux, en revanche il n'a été utilisé en analyse de données que récemment. On montre qu'il s'avère être un outil simple à utiliser pour certains problèmes comme la détection de données aberrantes, l'inférence de support, l'estimation de densité. Nous proposons aussi une utilisation nouvelle pour l'approximation, l'interpolation, motivée par des applications de la hiérarchie moment-somme de carrés en contrôle optimal et pour la résolution de certaines équations au dérivées partielles non-linéaires.
• 11h00-11h30. Pause café
• 11h30-13h00. Nicolas Brisebarre et Guillaume Hanrot (LIP, ENS Lyon), Points entiers proches d'une courbe transcendante et évaluation correctement arrondie de fonctions : partie 1 et partie 2.
Résumé


Malgré plusieurs avancées significatives au cours des 30 dernières années, garantir l'évaluation correctement arrondie des fonctions élémentaires, telles que le cosinus, l'exponentielle ou la racine cubique par exemple, reste un problème difficile. On peut le formuler comme un problème d'approximation diophantienne, appelé le dilemme du fabricant de table, qui consiste à déterminer des points avec des coordonnées entières proches d'une courbe. Dans un travail récent, nous proposons deux approches algorithmiques pour résoudre ce problème. Elles sont étroitement liées à des travaux féconds de Bombieri et Pila et à la méthode, devenue classique en cryptographie, de Coppersmith. Nos résultats entraînent que le développement d'une bibliothèque mathématique correctement arrondie pour le format binary128 est désormais possible à un coût beaucoup plus faible qu'avec les approches existantes. Nous présenterons le contexte initial, une de nos approches et les résultats d'expériences pratiques.

• 13h00. Déjeuner
• 15h00. Ateliers à l'INSA
• Jeudi 9 juin
• 9h00-9h30. Petit déjeuner
• 9h30-10h30. Damien Pous, Formally verified approximations in Coq, via certificates, Coq demo.
  Abstract
  We will present a library to verify rigorous approximations of univariate functions on real numbers, with the Coq proof assistant. Based on interval arithmetic, this library also implements a technique of validation a posteriori based on the Banach fixed-point theorem.
  We illustrate this technique on the case of operations of division and square root, as well as solutions of polynomial equations. This library features a collection of abstract structures that organise the specification of rigorous approximations, and modularise the related proofs. This makes it possible to provide implementation of verified approximations in several bases (Taylor, Chebyshev, Fourier).
  We will demonstrate how this library can be used during the talk.
  Joint work with Florent Bréhard, Louis Gaillard, Assia Mahboubi.
  
• 10h30-11h00. Sylvie Putot, RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems.
Abstract
We present a unified approach, implemented in the RINO tool, for the computation of inner and outer-approximations of reachable sets of discrete-time and continuous-time dynamical systems, possibly controlled by neural networks with differentiable activation functions. RINO combines a zonotopic set representation with generalized mean-value AE extensions to compute under and over-approximations of the robust range of differentiable functions, and applies these techniques to the particular case of learning-enabled dynamical systems. The AE extensions require an efficient and accurate evaluation of the function and its Jacobian with respect to the inputs and initial conditions. For continuous-time systems, possibly controlled by neural networks, the function to evaluate is the solution of the dynamical system. It is over-approximated in RINO using Taylor methods in time coupled with a set-based evaluation with zonotopes. We demonstrate the good performances of RINO compared to state-of-the art tools Verisig 2.0 and ReachNN* on a set of classical benchmark examples of neural network controlled closed loop systems. For generally comparable precision to Verisig 2.0 and higher precision than ReachNN*, RINO is always at least one order of magnitude faster, while also computing the more involved inner-approximations that the other tools do not compute.
• 11h00-11h30. Pause café
• 11h30-12h00. Bogdan Pasca (INTEL), The Intel FPGA for AI - architecture and applications.
Abstract
The advent of AI has driven the exploration of high-density low-precision arithmetic on FPGAs. In this talk we introduce the Stratix 10 NX device - a variant of FPGA specifically optimized for the AI application space. In addition to the computational capabilities of the standard programmable soft-logic fabric, a new type of DSP Block provides the dense arrays of low precision multipliers typically used in AI implementations. This talk focuses on the arithmetic capabilities of the new DSP block and shows how it can be used both at application level as well as for activation function approximation.
• 12h00-13h00. Joris Picot, Tests of the sharpness of known bounds on the error of the FFT.
Résumé
We study the accuracy of the fast Fourier transform with numerical tests, in order to implement a rigorous polynomial multiplication algorithm. We tried different methods to generate random inputs in order to maximize errors, and we compare results with a recently published work that provides a new refined bound as well as a bad case. We also compared the performances of interval arithmetic with the aforementioned work.
• 13h00. Déjeuner
• 15h00. Ateliers à l'INSA
• Vendredi 10 juin
• 9h00-9h30. Petit déjeuner
• 9h30-10h30. Mioara Joldes, Some (missing) bits and pieces about saddle-point based rigorous evaluation.
  Abstract
  
• 10h30-11h00. Jean-Michel Muller, Accurate calculation  and formalisation in Coq of Euclidean Norms using Double-word arithmetic, Part I.
Abstract
We consider the computation of the Euclidean (a.k.a. L₂) norm of an n-dimensional vector in floating-point arithmetic. We review the classical solutions used to avoid spurious overflow or underflow and/or to obtain very accurate results. We modify a recently published algorithm by Stef Graillat et al. to allow for a very accurate solution, free of spurious overflows and underflows. The returned result will be within very slightly more than 0.5 ulp from the exact result, which means that we will almost always provide correct rounding.
• 11h00-11h30. Pause café
• 11h30-12h00. Laurence Rideau, Accurate calculation  and formalisation in Coq of Euclidean Norms using Double-word arithmetic, Part II: Formalisation en Coq de la norme euclidienne en arithmétique double-double.
Résumé
Nous présenterons la vérification à l'aide de Coq des preuves de correction  des algorithmes et des bornes d'erreur d'une partie des résultats  impliqués par le calcul de norme euclidienne décrit précédemment.
• 12h00-13h00. Bruno Salvy, Coefficients Asymptotics of Multivariate Rational Functions.
Abstract


The coefficient sequences of multivariate rational functions appear in many areas of combinatorics. Their diagonal coefficient sequences enjoy nice arithmetic and asymptotic properties, and the field of analytic combinatorics in several variables (ACSV) makes it possible to compute asymptotic expansions. We consider these methods from the point of view of effectivity. In particular, given a rational function, ACSV requires one to determine a (generically) finite collection of points that are called critical and minimal. Criticality is an algebraic condition, meaning it is well treated by classical methods in computer algebra, while minimality is a semi-algebraic condition describing points on the boundary of the domain of convergence of a multivariate power series. We show how to obtain dominant asymptotics for the diagonal coefficient sequence of multivariate rational functions under some genericity assumptions using symbolic-numeric techniques. To our knowledge, this is the first completely automatic treatment and complexity analysis for the asymptotic enumeration of rational functions in an arbitrary number of variables.

This is joint work with Stephen Melczer.

• 13h00. Déjeuner
• 15h00 Clôture des journées.