Formal Proofs for Nonlinear Optimization
DOI:
https://doi.org/10.6092/issn.1972-5787/4319Keywords:
Polynomial Optimization Problems, Hybrid Symbolic-numeric Certification, Semidefinite Programming, Transcendental Functions, Semialgebraic Relaxations, Flyspeck Project, Maxplus Approximation, Templates Method, Proof AssistantAbstract
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.
References
Marianne Akian, Stéphane Gaubert, and Vassili Kolokoltsov.
Set coverings and invertibility of Functional Galois Connections.
In G.L. Litvinov and V.P. Maslov, editors, Idempotent
Mathematics and Mathematical Physics, volume 377 of Contemporary
Mathematics, pages 19--51. American Mathematical Society, 2005.
Also ESI Preprint 1447, http://arXiv.org/abs/math.FA/0403441.
M.~Akian, S.~Gaubert, and A.~Lakhoua.
The max-plus finite element method for solving deterministic optimal
control problems: basic properties and convergence analysis.
SIAM J. Control Optim., 47(2):817--848, 2008.
Xavier Allamigeon, Stéphane Gaubert, Victor Magron, and Benjamin Werner.
Certification of real inequalities -- templates and sums of squares.
Submitted for publication.~http://arxiv.org/abs/1403.5899.
Xavier Allamigeon, Stéphane Gaubert, Victor Magron, and Benjamin Werner.
Certification of bounds of non-linear functions : the templates
method, 2013.
Proceedings of Conferences on Intelligent Computer Mathematics, CICM
Calculemus, Bath.
Xavier Allamigeon, Stéphane Gaubert, Victor Magron, and Benjamin Werner.
Certification of inequalities involving transcendental functions:
combining sdp and max-plus approximation, 2013.
Proceedings of the European Control Conference, ECC'13, Zurich.
Micha"el Armand, Benjamin Grégoire, Arnaud Spiwack, and Laurent Théry.
Extending coq with imperative features and its application to sat
verification.
In Matt Kaufmann and LawrenceC. Paulson, editors, Interactive
Theorem Proving, volume 6172 of Lecture Notes in Computer Science,
pages 83--98. Springer Berlin Heidelberg, 2010.
M.~Montaz Ali, Charoenchai Khompatraporn, and Zelda~B. Zabinsky.
A numerical evaluation of several stochastic algorithms on selected
continuous global optimization test problems.
J. of Global Optimization, 31(4):635--672, April 2005.
Behzad Akbarpour and Lawrence~Charles Paulson.
Metitarski: An automatic theorem prover for real-valued special
functions.
J. Autom. Reason., 44(3):175--205, March 2010.
Frédéric Besson.
Fast reflexive arithmetic tactics the linear case and beyond.
In Proceedings of the 2006 international conference on Types for
proofs and programs, TYPES'06, pages 48--62, Berlin, Heidelberg, 2007.
Springer-Verlag.
R.~S. Boyer and J.~S. Moore.
Metafunctions: Proving them correct and using them efficiently as new
proof procedures.
In The Correctness Problem in Computer Science, pages 103--84.
Academic Press, New York, 1981.
Samuel Boutin. Using reflection to build efficient and certified decision procedures. In TACS'97. Springer-Verlag LNCS 1281, pages 515--529. Springer-Verlag, 1997.
Gilles Barthe, Mark Ruys, and Henk Barendregt. A two-level approach towards lean proof-checking, 1996.
A.~Cuyt, F.~Backeljauw, and C.~Bonan-Hamada. Handbook of Continued Fractions for Special Functions. SpringerLink: Springer e-Books. Springer, 2008.
W.~H. Fleming and W.~M. McEneaney. A max-plus-based algorithm for a Hamilton-Jacobi-Bellman
equation of nonlinear filtering. SIAM J. Control Optim., 38(3):683--710, 2000.
Benjamin Grégoire and Assia Mahboubi.
Proving equalities in a commutative ring done right in coq.
In Joe Hurd and Thomas~F. Melham, editors, TPHOLs, volume 3603
of Lecture Notes in Computer Science, pages 98--113. Springer, 2005.
Georges Gonthier.
Computer mathematics.
chapter The Four Colour Theorem: Engineering of a Formal Proof, pages
--333. Springer-Verlag, Berlin, Heidelberg, 2008.
B.~Grégoire and L.~Thery.
A purely functional library for modular arithmetic and its
application for certifying large prime numbers.
In U.~Furbach and N.~Shankar, editors, Proceedings of IJCAR'06,
volume 4130 of Lecture Notes in Artificial Intelligence, pages
--437. Springer-Verlag, 2006.
Thomas~C. Hales.
A proof of the kepler conjecture.
Math. Intelligencer, 16:47--58, 1994.
Thomas~C. Hales.
Some algorithms arising in the proof of the kepler conjecture.
In Boris Aronov, Saugata Basu, J'anos Pach, and Micha Sharir,
editors, Discrete and Computational Geometry, volume~25 of
Algorithms and Combinatorics, pages 489--507. Springer Berlin Heidelberg,
Thomas~C. Hales.
A proof of the Kepler conjecture.
Ann. of Math. (2), 162(3):1065--1185, 2005.
Thomas~C. Hales.
Introduction to the flyspeck project.
In Thierry Coquand, Henri Lombardi, and Marie-Franccoise Roy,
editors, Mathematics, Algorithms and Proofs, number 05021 in Dagstuhl
Seminar Proceedings, Dagstuhl, Germany, 2006. Internationales Begegnungs- und
Forschungszentrum f"ur Informatik (IBFI), Schloss Dagstuhl, Germany.
John Harrison.
Hol light: A tutorial introduction.
In Mandayam~K. Srivas and Albert~John Camilleri, editors,
FMCAD, volume 1166 of Lecture Notes in Computer Science, pages
--269. Springer, 1996.
Didier Henrion, Jean-Bernard Lasserre, and Johan Lofberg.
GloptiPoly 3: moments, optimization and semidefinite programming.
Optimization Methods and Software, 24(4-5):pp. 761--779, August
Erich~L. Kaltofen, Bin Li, Zhengfeng Yang, and Lihong Zhi.
Exact certification in global polynomial optimization via
sums-of-squares of rational functions with rational coefficients.
JSC, 47(1):1--15, jan 2012.
In memory of Wenda Wu (1929--2009).
Jean~B. Lasserre.
Global optimization with polynomials and the problem of moments.
SIAM Journal on Optimization, 11(3):796--817, 2001.
Jean~B. Lasserre and Mihai Putinar.
Positivity and optimization for semi-algebraic functions.
SIAM Journal on Optimization, 20(6):3364--3383, 2010.
David Monniaux and Pierre Corbineau.
On the generation of Positivstellensatz witnesses in degenerate
cases.
In Marko Van~Eekelen, Herman Geuvers, Julien Schmaltz, and Freek
Wiedijk, editors, Interactive Theorem Proving (ITP), volume 6898 of
Lecture Notes in Computer Science, pages 249--264. Springer Verlag,
August 2011.
W.~M. McEneaney.
Max-plus methods for nonlinear control and estimation.
Systems & Control: Foundations & Applications. Birkh"auser Boston
Inc., Boston, MA, 2006.
Guillaume Melquiond.
Floating-point arithmetic in the coq system.
Information and Computation, 216(0):14 -- 23, 2012.
Special Issue: 8th Conference on Real Numbers and Computers.
César Muñoz and Anthony Narkawicz.
Formalization of bernstein polynomials and applications to global
optimization.
Journal of Automated Reasoning, 51(2):151--196, 2013.
S. Owre, J.~M. Rushby, , and N. Shankar.
PVS: A prototype verification system.
In Deepak Kapur, editor, 11th International Conference on
Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial
Intelligence, pages 748--752, Saratoga, NY, jun 1992. Springer-Verlag.
Helfried Peyrl and Pablo~A. Parrilo.
Computing sum of squares decompositions with rational coefficients.
Theor. Comput. Sci., 409(2):269--281, 2008.
M.~Putinar.
Positive polynomials on compact semi-algebraic sets.
Indiana University Mathematics Journal, 42(3):969--984, 1993.
Markus Schweighofer.
Optimization of polynomials on compact semialgebraic sets.
SIAM Journal on Optimization, 15(3):805--825, 2005.
Alexey Solovyev and Thomas~C. Hales.
Formal~~verification of nonlinear inequalities with taylor interval
approximations.
CoRR, abs/1301.1702, 2013.
Alexey Solovyev.
Formal computations and methods.
Arnaud Spiwack.
Ajouter des entiers machine `a coq.
Sriram Sankaranarayanan, Henny~B. Sipma, and Zohar Manna.
Scalable analysis of linear systems using mathematical programming.
In Radhia Cousot, editor, Proc. of Verification, Model Checking
and Abstract Interpretation (VMCAI), volume 3385, pages 21--47, Paris,
France, January 2005. Springer Verlag.
Gilbert Stengle.
A nullstellensatz and a positivstellensatz in semialgebraic geometry.
Mathematische Annalen, 207(2):87--97, 1974.
Hayato Waki, Sunyoung Kim, Masakazu Kojima, and Masakazu Muramatsu.
Sums of squares and semidefinite programming relaxations for
polynomial optimization problems with structured sparsity.
SIAM Journal on Optimization, 17:218--242, 2006.
Makoto Yamashita, Katsuki Fujisawa, Kazuhide Nakata, Maho Nakata, Mituhiro Fukuda, Kazuhiro Kobayashi, and Kazushige Goto. A high-performance software package for semidefinite programs: Sdpa7. Technical report, Dept. of Information Sciences, Tokyo Institute of Technology, Tokyo, Japan, 2010.
Roland Zumkeller. Rigorous Global Optimization. PhD thesis, Ecole Polytechnique, 2008.
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2015 Victor Magron, Xavier Allamigeon, Stéphane Gaubert, Benjamin Werner
Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.
This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy
