zbMATH — the first resource for mathematics

Certification of bounds of non-linear functions: the templates method. (English) Zbl 1390.68570
Carette, Jacques (ed.) et al., Intelligent computer mathematics. MKM, Calculemus, DML, and systems and projects 2013, held as part of CICM 2013, Bath, UK, July 8–12, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-39319-8/pbk). Lecture Notes in Computer Science 7961. Lecture Notes in Artificial Intelligence, 51-65 (2013).
Summary: 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.
For the entire collection see [Zbl 1268.68008].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
11E25 Sums of squares and representations by other particular quadratic forms
14P10 Semialgebraic sets and related spaces
65K10 Numerical optimization and variational techniques
68W30 Symbolic computation and algebraic computation
90C22 Semidefinite programming
90C30 Nonlinear programming
Full Text: DOI