文章基本信息

标题：Formal Proofs for Nonlinear Optimization
本地全文：下载
作者：Victor Magron ; Xavier Allamigeon ; Stéphane Gaubert 等
期刊名称：Journal of Formalized Reasoning
印刷版ISSN：1972-5787
出版年度：2015
卷号：8
期号：1
页码：1-24
DOI：10.6092/issn.1972-5787/4319
语种：English
出版社：Alma Mater Studiorum - University of Bologna
摘要：We present a formally verified global optimization framework. Given a semialgebraic or transcendental function f and a compact semialgebraic domain K, we use the nonlinear maxplus template approximation algorithm to provide a certified lower bound of f over K. This method allows to bound in a modular way some of the constituents of f by suprema of quadratic forms with a well chosen curvature. Thus, we reduce the initial goal to a hierarchy of semialgebraic optimization problems, solved by sums of squares relaxations. Our implementation tool interleaves semialgebraic approximations with sums of squares witnesses to form certificates. It is interfaced with Coq and thus benefits from the trusted arithmetic available inside the proof assistant. This feature is used to produce, from the certificates, both valid underestimators and lower bounds for each approximated constituent. The application range for such a tool is widespread; for instance Hales' proof of Kepler's conjecture yields thousands of multivariate transcendental inequalities. We illustrate the performance of our formal framework on some of these inequalities as well as on examples from the global optimization literature.
其他摘要：We present a formally verified global optimization framework. Given a semialgebraic or transcendental function f and a compact semialgebraic domain K, we use the nonlinear maxplus template approximation algorithm to provide a certified lower bound of f over K. This method allows to bound in a modular way some of the constituents of f by suprema of quadratic forms with a well chosen curvature. Thus, we reduce the initial goal to a hierarchy of semialgebraic optimization problems, solved by sums of squares relaxations. Our implementation tool interleaves semialgebraic approximations with sums of squares witnesses to form certificates. It is interfaced with Coq and thus benefits from the trusted arithmetic available inside the proof assistant. This feature is used to produce, from the certificates, both valid underestimators and lower bounds for each approximated constituent. The application range for such a tool is widespread; for instance Hales' proof of Kepler's conjecture yields thousands of multivariate transcendental inequalities. We illustrate the performance of our formal framework on some of these inequalities as well as on examples from the global optimization literature.
关键词：Polynomial Optimization Problems;Hybrid Symbolic-numeric Certification;Semidefinite Programming;Transcendental Functions; Semialgebraic Relaxations;Flyspeck Project;Maxplus Approximation;Templates Method;Proof Assistant