Certification of bounds of non-linear functions: the templates method

DOI10.1007/978-3-642-39320-4_4MaRDI QIDQ2843005zbMATH OpenOpenAlexFDO

Authors Xavier Allamigeon, Stéphane Gaubert, Victor Magron, Benjamin Werner

Publication date 9 August 2013

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1307.3231

zbMATH Keywords

semidefinite programmingproof assistanttranscendental functionspolynomial optimization problemsquadratic cutssemialgebraic relaxationsFlyspeck projecthybrid symbolic-numeric certificationmax-plus approximationtemplates method

Mathematics Subject Classification ID

Numerical optimization and variational techniques (65K10) Symbolic computation and algebraic computation (68W30) Nonlinear programming (90C30) Semidefinite programming (90C22) Semialgebraic sets and related spaces (14P10) Sums of squares and representations by other particular quadratic forms (11E25)

Abstract: 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.

Recommendations

• Formal Proofs for Nonlinear Optimization
• Certification of real inequalities: templates and sums of squares
• Dynamics of a parametrically excited system with two forcing terms
• NLCertify: a tool for formal nonlinear optimization
• Formal Global Optimisation with Taylor Models

Cited in

(7)

• Formal Proofs for Nonlinear Optimization
• Theorem Proving in Higher Order Logics
• Certification of real inequalities: templates and sums of squares
• Formal Global Optimisation with Taylor Models
• Proving tight bounds on univariate expressions with elementary functions in Coq
• Dynamics of a parametrically excited system with two forcing terms
• NLCertify: a tool for formal nonlinear optimization

Describes a project that uses

Uses Software

• Flyspeck
• Intsolver
• SparsePOP
• MetiTarski
• Coq

This page was built for publication: Certification of bounds of non-linear functions: the templates method

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2843005)