Project topics and materials
Get Complete Project Material File(s) Now! »
Certified Global Optimization in the Literature
A common idea to handle Problem (1.1.2) is to first estimate f by multivariate poly-nomials and then obtain a lower bound of the resulting approximation by polynomial optimization techniques.
Computing lower bounds in constrained POP (see Problem(1.1.5)) is already a dif-ficult problem, which has received much attention. Sums of squares (SOS) relaxation based methods, leading to the resolution of semidefinite programs (SDP) have been developed in [Las01, PS03]. They can be applied to the more general class of semi-algebraic problems [Put93]. Moreover, Kojima has developed a sparse refinement of the hierarchy of SDP relaxations (see [WKKM06]). This has been implemented in the SPARSEPOP solver. Checking the validity of the lower bound of POP im-plies being able to control and certify the numerical error, as SDP solvers are typi-cally implemented using floating point arithmetic. Such techniques rely on hybrid symbolic-numeric certification methods, see Peyrl and Parrilo [PP08] and Kaltofen et al. [KLYZ12]. They allow one to produce positivity certificates for such POP which can be checked in proof assistants such as COQ [MC11, Bes07], HOL-LIGHT [Har07] or MetiTarski [AP10]. Alternative approaches to SOS/SDP are based on Bernstein polynomials [Zum08].
The task is obviously more difficult in presence of transcendental functions. Other methods of choice, not restricted to polynomial systems, include global optimization by interval methods (see e.g. [Han06]), branch and bound methods with Taylor mod-els [CGT11, BM09]. Other methods involve rigorous Chebyshev estimators. An im-plementation of such approximations is available in the Sollya tool [CJL10]. We also mention procedures that solve SMT problems over the real numbers, using interval constraint propagation [GAC12].
Recent efforts have been made to perform a formal verification of several Flyspeck inequalities with Taylor interval approximations in the HOL-LIGHT proof assistant [SH13]. The Flocq library formalizes floating-point arithmetic inside COQ [Mel12]. The tactic interval, built on top of Flocq, can simplify inequalities on expressions of real numbers.
Contribution
A General Certification Scheme
In this thesis, we develop a general certification framework, combining methods from semialgebraic programming (SOS certificates, SDP relaxations) and from approxima-tion theory. This includes classical methods like best uniform polynomials and less classical like maxplus approximation (inspired by optimal control and static analysis by abstract interpretation).
The present approach exploits both the accuracy of SOS relaxations and the scala-bility of the approximation and abstraction procedure. This leads to a new method in global optimization, the nonlinear template method, that produces certificates, which are ultimately proved in COQ.
The general principle of our framework is explained in Chapter 3. We alternate steps of semialgebraic approximation for some constituents of the objective function
f and semialgebraic optimization. The resulting constrained polynomial optimiza-tion problems are solved with sums of squares relaxation from Lasserre hierarchy, by calling a semidefinite solver. In this way, each iteration of the algorithms refines the following inequalities: f ∗ > fsa∗ > fpo∗ p .
where f ∗ is the optimal value of the original problem, fsa∗ the optimal value of its current semialgebraic approximation and fpop∗ the optimal value of the SDP relaxation which we solve. Under certain moderate assumptions, the lower estimate fpop∗ does converge to f ∗ (see Corollary 3.9).
Different semialgebraic approximation schemes for transcendental functions are presented, namely minimax estimators (Chapter 4), maxplus approximations (Chap-ter 5) and templates abstractions (Chapter 6).
Minimax Polynomial Approximations
A natural workaround to deal with non-polynomial optimization problems is to esti-mate the objective function f with its best uniform (also called “minimax”) degree-d polynomial approximation.
Thus, we obtain a hierarchy of minimax semialgebraic approximations, which leads to the algorithm minimax_optim. In practice, an interface with the software Sollya [CJL10] provides the univariate minimax polynomials.
Maxplus Estimators
The second method uses maxplus approximation of semiconvex transcendental func-tions by quadratic functions. The idea of maxplus approximation comes from op-timal control: it was originally introduced by Fleming and McEneaney [FM00] and developed by several authors [AGL08a, MDG08, McE07, SGJM10, GMQ11], to rep-resent the value function by a “maxplus linear combination”, which is a supremum of certain basis functions, like quadratic polynomials. When applied to the present context, this idea leads to approximate from above and from below every transcen-dental function appearing in the description of the problem by infima and suprema of finitely many quadratic polynomials.
In that way, we are reduced to a converging sequence of semialgebraic problems. A geometrical way to interpret the method is to think of it in terms of “quadratic cuts” quadratic inequalities are successively added to approximate the graph of a transcendental function.
This work was published in the Proceedings of the 12th European Control Con-ference [AGMW13b].
Templates Abstractions
The nonlinear template method is an improved version of the maxplus approxima-tion. By comparison, the new component is the introduction of the template tech-nique (approximating projections of the feasible sets), leading to an increase in scala-bility.
This technique is an abstraction method, which is inspired by the linear template of Sankaranarayanan, Sipma and Manna in static analysis [SSM05], their nonlinear extensions by Adjé et al. [AGG12], and the maxplus basis method [SGJM10].
In the present application, templates are used both to approximate transcenden-tal functions, and to produce coarser but still tractable relaxations when the standard SDP relaxation of the semialgebraic problem is too complex to be handled. As a mat-ter of fact, SDP relaxations are a powerful tool to get tight certified lower bound for semialgebraic optimization problems, but applying them is currently limited to small or medium size problems: their execution time grows very rapidly with the relax-ation order, which itself grows with the degree of the polynomials involved in the semialgebraic relaxations. The template method allows to reduce these degrees, by approximating certain projections of the feasible set by a moderate number of nonlin-ear inequalities.
They are also useful as a replacement of standard Taylor approximations of tran-scendental functions: instead of increasing the degree of the approximation, one in-creases the number of functions in the template.
In this dissertation, we present two families of templates:
• Non-convex quadratic templates for POP The objective polynomial of a non tractable POP is replaced by a suprema of quadratic polynomials (see Section 6.2).
• Polynomial underestimators templates for semialgebraic functions Given a degree d and a semialgebraic function fsa that involves a large number of lifting variables, we build a hierarchy of polynomial approximations, that converge to the best (for the L1-norm) degree-d polynomial underestimator of fsa (see Section 6.3).
A part of this work was published in the Proceedings of the Conferences on In-telligent Computer Mathematics, in the Lecture Notes in Artificial Intelligence (LNAI 7961) [AGMW13a].
Software Implementation in OCAML and COQ
The final achievement of this work is the software implementation of our general optimization algorithm, leading to the package NLCertify.
Given a nonlinear inequality and an approximation method as input, our pack-age NLCertify builds a hierarchy of approximations and generates the corresponding semidefinite relaxations, using OCAML libraries and external programs (Sollya and SDPA). The correctness of the bounds for semialgebraic optimization problems can be verified using the interface of NLCertify with COQ. Thus, the certificate search and the proof checking inside COQ are separated, a so called sceptical approach.
When solving a POP, the sums of squares certificate does not match with the sys-tem of polynomial inequalities, due to a rounding error. A certified upper bound of this error is obtained inside COQ (Section 7.3.2). This verification procedure is carefully implemented, using an equality test in the ring of polynomials whose co-efficients are arbitrary-size rationals (Section 7.2.2). It ensures efficient computation inside the proof assistant.
Moreover, these verifications for POP relaxations are combined to deduce the cor-rectness of semialgebraic optimization procedures, which requires in particular to assert that the semialgebraic functions are well-defined. It allows to handle more complex certificates for non-polynomial problems. Finally, the datatype structure of these certificates allows to reconstruct the steps of the optimization algorithm.
The software implementation package NLCertify, is described in Appendix B. At the time the author writes this PhD dissertation, the NLCertify tool contains more than 2600 lines of code for the COQ proof scripts and more than 15000 lines of code for the OCAML informal certification program.
Outline
This dissertation is organized as follows:
Part I introduces the required background about semialgebraic optimization and presents a general global optimization framework, which relies on an approximation algorithm approx and the optimization procedure optim.
• In Chapter 2, we recall the basic principles of semidefinite programming, the definition and properties of Lasserre relaxations of polynomial problems, to-gether with reformulations by Lasserre and Putinar of semialgebraic problems classes. The sparse variant of these relaxations is also presented.
• In Chapter 3, we describe our general approximation scheme for global opti-mization. Then, we give a proof of convergence of this algorithm.
Part II instantiates the algorithm approx with minimax, maxplus and templates approximations.
• In Chapter 4, we recall some fundamental statements about best uniform poly-nomial approximations. Then we present the performance results of our algo-rithm minimax_optim, which combines minimax estimators and SOS.
• In Chapter 5, the maxplus approximation and the samp_optim algorithm are presented. We show how this algorithm can be combined with standard domain subdivision methods, to reduce the relaxation gap.
• In Chapter 6, we present the nonlinear extension of the template method. We explain how to control the complexity of semialgebraic optimization problems with our algorithm template_optim.
Part III focuses on formal proofs for global optimization via templates and sums of squares.
• In Chapter 7, we recall the required background on the arithmetic available in-side COQ. Then, we explain how to check in COQ nonlinear inequalities involv-ing multivariate transcendental functions.
• In Chapter 8, we conclude and discuss the perspectives of this work.
Semidefinite Programming and Interior-Points methods
Semidefinite programming is relevant to a wide range of applications. The interested reader can find more details on the connection between SDP and combinatorial op-timization in [GLV09], control theory in [BEFB94], positive semidefinite matrix com-pletion in [Lau09]. A survey on semidefinite programming is available in the paper of Vandenberghe and Boyd [VB94]. Here, we give the basic definitions of primal and dual semidefinite programs, then explain how to solve these programs with the interior-points methods and recall some complexity results regarding the cost of these techniques. Even though semidefinite programming is not our main topic of interest, several encountered problems can be cast as semidefinite programs. We emphasize the fact that semidefinite programs can be solved efficiently (up to a few thousand op-timization variables) by freely available software (e.g. SeDuMi [Stu98], CSDP [Bor97], SDPA [YFN+10]).
First, we introduce some useful notations. We consider the vector space S n of real symmetric n × n matrices. Given X ∈ S n, let λmax(X) (resp. λmin(X)) be the maximum (resp. minimum) eigenvalue of X. It is equipped with the usual inner product X, Y = Tr(XY) for X, Y ∈ Sn. Let In be the n × n identity matrix. The Frobenius norm of a matrix X ∈ STn is defined by X F := Tr(X2) . A matrix M ∈ Sn n is called positive semidefinite if x Mx > 0, ∀x ∈ R . In this case, we write M < 0 and define a partial order by writing X < Y (resp. X ≻ Y) if and only if X − Y is positive semidefinite (resp. positive definite).
In semidefinite programming, one minimizes a linear objective function subject to a linear matrix inequality (LMI). The variable of the problem is the vector x ∈ Rm and the problem input data are the vector c ∈ Rm and symmetric matrices F0, . . . , Fm ∈ Sn.
The primal semidefinite program is defined as follows: psdp∗ := min cT x x∈Rm (2.1.1)
Table of contents :
1 Introduction
1.1 Problems Involving Computer Assisted Proofs
1.1.1 Nonlinear Inequalities arising in the Flyspeck Project
1.1.2 Formal Global Optimization Problems
1.1.3 Non Commutative Optimization
1.2 Certified Global Optimization in the Literature
1.3 Contribution
1.3.1 A General Certification Scheme
1.3.2 Software Implementation in OCAML and COQ
1.4 Outline
I A General Framework for Certified Global Optimization
2 Sums of Squares based Optimization
2.1 SDP and Interior-Points methods
2.2 Application of SDP to Polynomial Optimization
2.3 Application of SDP to Semialgebraic Optimization
2.4 Exploiting the System Properties
2.5 Hybrid Symbolic-Numeric Certification
3 A General Approximation Scheme
3.1 Abstract Syntax Tree of Multivariate Transcendental Functions
3.2 Combining Semialgebraic Approximations and SOS
3.3 Convergence of the Approximation Algorithm
II Nonlinear Optimization via Maxplus Templates
4 Minimax Semialgebraic Optimization
4.1 Minimax Univariate Polynomials
4.2 Combining Minimax Approximations and SOS
4.3 Numerical Test Results
4.4 Convergence Properties
4.5 Taylor Expansions
5 Maxplus Semialgebraic Estimators and SOS
5.1 The Basis of Maxplus Functions
5.2 Maxplus Approximation for Semiconvex Functions
5.3 Combining Maxplus Approximations and SOS
5.3.1 An Adaptive Semialgebraic Approximation Algorithm
5.3.2 An Optimization Algorithm based on Maxplus Estimators
5.3.3 Convergence Results
5.3.4 Refining Bounds by Domain Subdivisions
5.4 Numerical Results
5.4.1 Flyspeck Inequalities
5.4.2 Random Inequalities
5.4.3 Certification of MetiTarski Bounds
6 The Templates Method
6.1 Max-plus Approximations and Nonlinear Templates
6.2 Reducing the Size of SOS Relaxations for POP
6.2.1 Lower Bounds of Interval Matrix Minimal Eigenvalues
6.2.2 A Template Algorithm for POP
6.2.3 Numerical Results
6.3 Underestimators for Semialgebraic Functions
6.3.1 Best Polynomial Underestimators
6.3.2 A Convergent Hierarchy of Semidefinite Relaxations
6.3.3 Exploiting Sparsity
6.3.4 Numerical Experiments
6.4 The Template Optimization Algorithm
6.5 Benchmarks
6.5.1 Comparing three certification methods
6.5.2 Global optimization problems
6.5.3 Certification of various Flyspeck inequalities
III From Certified to Formal Global Optimization
7 Formal Nonlinear Global Optimization
7.1 The COQ Proof Assistant
7.1.1 A Formal Theorem Prover
7.1.2 Logic and Computation
7.1.3 Computational Reflection
7.2 Polynomial Arithmetic in COQ
7.2.1 From Binary Integers to Arbitrary-size Rationals
7.2.2 The polynomial ring structure
7.3 Formal Polynomial Optimization
7.3.1 Encoding Putinar Certificates
7.3.2 Bounding the Polynomial Remainder
7.3.3 Checking Polynomial Equalities
7.3.4 Checking Polynomial Nonnegativity
7.4 Beyond Polynomial Inequalities
7.4.1 Intervals
7.4.2 Semialgebraic expressions
7.4.3 POP relaxations
7.4.4 Formal Bounds for Semialgebraic Functions
8 Conclusion and Perspectives
8.1 Achievements
8.2 Perspectives
8.2.1 Complexity of the nonlinear template method
8.2.2 Extension to global optimization with transcendental constraints
8.2.3 Extension to nonlinear optimal control problems
8.2.4 Formal procedures for nonlinear reasoning
A Flyspeck Nonlinear Inequalities
A.1 Semialgebraic Flyspeck Inequalities
A.2 Transcendental Flyspeck Inequalities
A.2.1 Small-sized Flyspeck Inequalities
A.2.2 Medium-size Flyspeck Inequalities
B The NLCertify Package
B.1 Source Code Organization
B.2 Installation of the NLCertify Package
B.2.1 Compilation Dependencies
B.2.2 Installation
B.3 User Parameters
B.3.1 General Parameters
B.3.2 POP/SDP Relaxations Parameters
B.4 Certification of Nonlinear Inequalities
B.4.1 Input Settings
B.4.2 NLCertify Execution
