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

Flyspeck projecthybrid symbolic-numeric certificationmax-plus approximationpolynomial optimization problemsproof assistantquadratic cutssemialgebraic relaxationssemidefinite programmingtemplates methodtranscendental functions

Mathematics Subject Classification ID

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

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)

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

Describes a project that uses

Uses Software

• MetiTarski
• Intsolver
• Coq
• SparsePOP
• Flyspeck

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)