Formal Proofs for Nonlinear Optimization

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

Abstract


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.

Keywords


Polynomial Optimization Problems; Hybrid Symbolic-numeric Certification; Semidefinite Programming; Transcendental Functions; Semialgebraic Relaxations; Flyspeck Project; Maxplus Approximation; Templates Method; Proof Assistant

Full Text:

PDF (English)

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.




DOI: 10.6092/issn.1972-5787/4319

Copyright (c) 2015 Victor Magron, Xavier Allamigeon, Stéphane Gaubert, Benjamin Werner

Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 Unported License.