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 GayLussac at École polytechnique, Palaiseau, France. The jury was composed of:
 Xavier Allamigeon
 Yves Bertot, Reviewer
 Stephane Gaubert, CoAdvisor
 Thomas Hales, Reviewer
 Didier Henrion, Reviewer
 Monique Laurent
 Markus Schweighofer
 Benjamin Werner, Advisor

Abstract:
The aim of this work is to certify lower bounds for realvalued 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 degreed 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 (maxplus 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.
