2018-00418 - Post-doc on Formal Proofs about the Floating-Point Evaluation of Polynomials
Le descriptif de l’offre ci-dessous est en Anglais

Type de contrat : CDD de la fonction publique

Niveau de diplôme exigé : Thèse ou équivalent

Fonction : Post-Doctorant

A propos du centre ou de la direction fonctionnelle

Located at the heart of the main national research and higher education cluster, member of the Université Paris Saclay, a major actor in the French Investments for the Future Programme (Idex, LabEx, IRT, Equipex) and partner of the main establishments present on the plateau, the centre is particularly active in three major areas: data and knowledge; safety, security and reliability; modelling, simulation and optimisation (with priority given to energy).   

The 450 researchers and engineers from Inria and its partners who work in the research centre's 31 teams, the 100 research support staff members, the high-level equipment at their disposal (image walls, high-performance computing clusters, sensor networks), and the privileged relationships with prestigious industrial partners, all make Inria Saclay Île-de-France a key research centre in the local landscape and one that is oriented towards Europe and the world.

Contexte et atouts du poste

The job is within the FastRelax project, funded by the French National Research Agency (ANR). The aim of this project is to develop computer-aided proofs of numerical values, with certified and reasonably tight error bounds, without sacrificing efficiency. Applications to zero-finding, numerical quadrature or global optimization can all benefit from using our results as building blocks. We expect our work to initiate a "fast and reliable" trend in the symbolic-numeric community. This will be achieved by developing interactions between our fields, designing and implementing prototype libraries and applying our results to concrete problems originating in optimal control theory.

 

http://fastrelax.gforge.inria.fr/

Travel expenses for conferences and within the project sites (Paris, Lyon, Toulouse, Sophia-Antipolis) are covered within the limits of the scale in force.

Mission confiée

The goal of this post-doc is to develop formal proofs about a basic brick in floating-point arithmetic: the evaluation of a polynomial. In passing from a polynomial approximation to numerical values, we have to evaluate polynomials numerically. This is a known problem with a lot of literature. Nevertheless, this is a critical issue and formal proofs will ensure the correctness of the current theorems. Moreover, they will uncover their exact requirements. Indeed, exceptional behavior such as underflow may happen, and need to be taken care of in the formal proof assistant.


As the bounds will be loose in certain cases, the study will continue with the study of compensated algorithms, that are both more costly and more accurate. It is not yet known how to obtain faithful rounding (i.e., the computed result is one of the two adjacent floating-point numbers surrounding the exact result) for polynomial evaluation. Formal proofs of the previous results will help us in studying this problem and design such an algorithm with hopefully a moderate overhead compared to the classic Horner scheme. This may be inspired by recent work for the computation of the Euclidean norm of a vector. Another direction of extension is the computation of rounding to the nearest floating-point number, which is important in order to get a reproducible result even if the computations are performed in parallel.

The formal proofs will be in Coq, and will rely on the Flocq library developped inside the team.

 

References:

Nicholas J. Higham. Accuracy and Stability of Numerical Algorithms. SIAM. Second edition. 2002.

Stef Graillat, Philippe Langlois and Nicolas Louvet. Algorithms for accurate, validated and fast polynomial evaluation. Japan J. Indust. Appl. Math., 26 (2009), no. 2-3, 191-214.

Stef Graillat, Christoph Lauter, Peter Tang, Naoya Yamanaka and Shin'ichi Oishi. Efficient calculations of faithfully rounded l2-norms of n-vectors. ACM Transactions on Mathematical Software, 41 (2015), no. 4, article 24.

Sylvie Boldo and Guillaume Melquiond. Flocq: A Unified Library for Proving Floating-point Algorithms in Coq. In Proceedings of the 20th IEEE Symposium on Computer Arithmetic, pages 243-252, Tübingen, Germany, July 2011.

Sylvie Boldo and Guillaume Melquiond. Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System. ISTE Press - Elsevier, December 2017.

 

 

 

Principales activités

Main activities :

  • Study the state of the art of floating-point polynomial evaluation
  • Develop formal proofs of these results
  • Generalize these results to get tighter bounds and/or handle exceptional behavior
  • Write reports and submit research articles

Compétences

The topic of the post-doc is at the intersection of two different research fields. The candidate should therefore have a PhD thesis in the domain of either formal methods (with a basic knowledge of an interactive prover such as Coq, Isabelle, or PVS) or floating-point arithmetic. An interest in the other topic is expected.

Avantages sociaux

  • Subsidised catering service
  • Partially-reimbursed public transport
  • Social security
  • Paid leave
  • Flexible working hours
  • Sports facilities

Rémunération

Monthly gross salary : 2.653 euros