Habilitation Defense

My habilitation thesis is entitled The quest of modeling, certification and efficiency in polynomial optimization. A preliminary version of the manuscript is available here.

My defense took place on Tuesday May 25th 2021 at 5:00 p.m. in the conference room at LAAS CNRS, Toulouse, France. The jury was composed of: Antonio Acin Salma Kuhlmann, President Jean-Bernard Lasserre, Parrain Bernard Mourrain, Reviewer Patrick Panciatici Mihai Putinar, Reviewer Anders Rantzer, Reviewer Bruno Salvy

Abstract:

Certified optimization techniques have successfully tackled challenging verification problems in various fundamental and industrial applications. The formal verification of thousands of nonlinear inequalities arising in the famous proof of Kepler conjecture was achieved in August 2014. In energy networks, it is now possible to compute the solution of large-scale power flow problems with up to thousand variables. This success follows from growing research efforts in polynomial optimization, an emerging field extensively developed in the last two decades. One key advantage of these techniques is the ability to model a wide range of problems using optimization formulations, which can be in turn solved with efficient numerical tools. My methodology heavily relies on such methods, including the moment-sums of squares (moment-SOS) hierarchy by Lasserre which provides numerical certificates for positive polynomials as well as recently developed alternative methods. However, such optimization methods still encompass many major issues on both practical and theoretical sides: scalability, unknown complexity bounds, ill-conditioning of numerical solvers, lack of exact certification, convergence guarantees. This manuscript presents results along these research tracks with the long-term perspective of obtaining scientific breakthroughs to handle certification of nonlinear systems arising in real-world applications.

In the first part, I focus on modeling aspects. One relies on the moment-SOS hierarchy to analyze dynamical polynomial systems, either in the discrete-time or continuous-time setting, and problems involving noncommuting variables, for example matrices of finite or infinite size, to model quantum physics operators. In the second part, I describe how to design and analyze algorithms which output exact positivity certificates for either unconstrained or constrained optimization problems. In the last part, I explain how to improve the scalability of the hierarchy by exploiting the specific sparsity structure of the polynomial data coming from real-world problems. Important applications arise from various fields, including computer arithmetic (roundoff error bounds), quantum information (noncommutative optimization), and optimal power-flow.

PhD Defense

My PhD thesis is entitled Formal Proofs for Global Optimization -- Templates and Sums of Squares. A preliminary version of the manuscript is available here.

My defense took place on Monday December 9th 2013 at 10:00 a.m. in amphitheatre Gay-Lussac at École polytechnique, Palaiseau, France. The jury was composed of: Xavier Allamigeon, Co-Advisor Yves Bertot, Reviewer Stephane Gaubert, Co-Advisor Thomas Hales, Reviewer Didier Henrion, Reviewer Monique Laurent, President Markus Schweighofer Benjamin Werner, Advisor

Abstract:

The aim of this work is to certify lower bounds for real-valued multivariate functions, defined by semialgebraic or transcendental expressions and to prove their correctness by checking the certificates in the Coq proof system.

The application range for such a tool is widespread; for instance Hales' proof of Kepler's conjecture involves thousands of nonlinear inequalities. The functions we are dealing with are nonlinear and involve semialgebraic operations as well as some transcendental functions like cos, arctan, exp, etc. Our general framework is to use different approximation methods to relax the original problem into a semialgebraic optimization problem. It leads to polynomial optimization problems which we solve by sparse sums of squares relaxations.

First, we implement a classical scheme in global optimization. Namely, we approximate univariate transcendental functions with best uniform degree-d polynomial estimators. Then, we present an alternative method, which consists in bounding some of the constituents of the nonlinear function by suprema or infima of quadratic polynomials (max-plus approximation method, initially introduced in optimal control) with a carefully chosen curvature. Finally, we improve this approximation algorithm, by combining the ideas of the maxplus estimators and of the linear template method developed by Manna et al. (in static analysis). The nonlinear templates control the complexity of the semialgebraic estimators at the price of coarsening the maxplus approximations. In that way, we arrive at a new - template based - global optimization method, which exploits both the precision of sums of squares/SDP relaxations and the scalability of abstraction methods.

We successfully implemented these approximation methods in a software package named NLCertify. This tool interleaves semialgebraic approximations with sums of squares witnesses to form certificates. It is interfaced with Coq and thus benefits from the trusted arithmetic available inside the proof assistant. This feature is used to produce, from the certificates, both valid underestimators and lower bounds for each approximated constituent. We illustrate the efficiency of NLCertify with various examples from the global optimization literature, as well as tight inequalities issued from the Flyspeck project.