Friday, 11:30 - 11:55 h, Room: H 2038


Victor Magron
Certification of inequalities involving transcendental functions using semi-definite programming.

Coauthors: Xavier Allamigeon, St├ęphane Gaubert, Benjamin Werner


We consider the optimization problem minx ∈ K f(x), where f
is a multivariate transcendental function and K is a compact
semi-algebraic set. Recent efforts have been made to produce
positivity certificates for these problems, and to verify
these certificates with proof assistants such as COQ. Our motivation
is to automatically verify inequalities from the proof of Kepler
conjecture by Thomas Hales.
We will present a certification framework, combining semi-definite
programming with semi-algebraic approximations of transcendental
functions. Our method consists in an iterative decomposition of the
set K into subsets in which the inequalities to be certified are
expected to be either tight or coarse. Coarse inequalities are checked
by global optimization methods (solving a hierarchy of relaxed
problems using SOS solvers such as SparsePOP). Then, the feasible
points generated by these methods are used to refine iteratively the
semi-algebraic approximations of transcendental functions until the
needed accuracy is reached. Tight inequalities are certified locally
by Taylor-type models. Experimental results will illustrate numerical and scalability issues.


Talk 3 of the invited session Fri.1.H 2038
"Recent developments of theory and applications in conic optimization II" [...]
Cluster 4
"Conic programming" [...]


  The best way to go for you to know the credible Michigan Loans Online providers. On the global pharmaceutical market this medicine was issued in 2003 by two companies - Eli Lilly and ICOS. Initially, permission to sell Cialis was obtained in Europe, Australia, New Zealand.