TY - GEN
T1 - The templates method
AU - Allamigeon, Xavier
AU - Gaubert, Stéphane
AU - Magron, Victor
AU - Werner, Benjamin
PY - 2013/8/1
Y1 - 2013/8/1
N2 - The aim of this work is to certify lower bounds for real-valued multivariate functions, defined by semialgebraic or transcendental expressions. The certificate must be, eventually, formally provable in a proof system such as Coq. The application range for such a tool is widespread; for instance Hales' proof of Kepler's conjecture yields thousands of inequalities. We introduce an approximation algorithm, which combines ideas of the max-plus basis method (in optimal control) and of the linear templates method developed by Manna et al. (in static analysis). This algorithm consists in bounding some of the constituents of the function by suprema of quadratic forms with a well chosen curvature. This leads to semialgebraic optimization problems, solved by sum-of-squares relaxations. Templates limit the blow up of these relaxations at the price of coarsening the approximation. We illustrate the efficiency of our framework with various examples from the literature and discuss the interfacing with Coq.
AB - The aim of this work is to certify lower bounds for real-valued multivariate functions, defined by semialgebraic or transcendental expressions. The certificate must be, eventually, formally provable in a proof system such as Coq. The application range for such a tool is widespread; for instance Hales' proof of Kepler's conjecture yields thousands of inequalities. We introduce an approximation algorithm, which combines ideas of the max-plus basis method (in optimal control) and of the linear templates method developed by Manna et al. (in static analysis). This algorithm consists in bounding some of the constituents of the function by suprema of quadratic forms with a well chosen curvature. This leads to semialgebraic optimization problems, solved by sum-of-squares relaxations. Templates limit the blow up of these relaxations at the price of coarsening the approximation. We illustrate the efficiency of our framework with various examples from the literature and discuss the interfacing with Coq.
KW - Flyspeck Project
KW - Hybrid Symbolic-numeric Certification
KW - Max-plus Approximation
KW - Polynomial Optimization Problems
KW - Proof Assistant
KW - Quadratic Cuts
KW - Semialgebraic Relaxations
KW - Semidefinite Programming
KW - Templates Method
KW - Transcendental Functions
UR - https://www.scopus.com/pages/publications/84880741342
U2 - 10.1007/978-3-642-39320-4_4
DO - 10.1007/978-3-642-39320-4_4
M3 - Conference contribution
AN - SCOPUS:84880741342
SN - 9783642393198
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 51
EP - 65
BT - Intelligent Computer Mathematics - MKM, Calculemus, DML, and Systems and Projects 2013 - Held as Part of CICM 2013, Proceedings
T2 - Conference on Intelligent Computer Mathematics, CICM 2013, Co-located with the MKM 2013, Calculemus 2013, DML 2013, and Systems and Projects 2013
Y2 - 8 July 2013 through 12 July 2013
ER -