Certification of inequalities involving transcendental functions: combining SDP and max-plus approximation

Xavier Allamigeon 1, 2 Stéphane Gaubert 1, 2 Victor Magron 1, 3 Benjamin Werner 3, 4
2 MAXPLUS - Max-plus algebras and mathematics of decision
CMAP - Centre de Mathématiques Appliquées - Ecole Polytechnique, Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR
4 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : We consider the problem of certifying an inequality of the form $f(x)\geq 0$, $\forall x\in K$, where $f$ is a multivariate transcendental function, and $K$ is a compact semialgebraic set. We introduce a certification method, combining semialgebraic optimization and max-plus approximation. We assume that $f$ is given by a syntaxic tree, the constituents of which involve semialgebraic operations as well as some transcendental functions like $\cos$, $\sin$, $\exp$, etc. We bound some of these constituents by suprema or infima of quadratic forms (max-plus approximation method, initially introduced in optimal control), leading to semialgebraic optimization problems which we solve by semidefinite relaxations. The max-plus approximation is iteratively refined and combined with branch and bound techniques to reduce the relaxation gap. Illustrative examples of application of this algorithm are provided, explaining how we solved tight inequalities issued from the Flyspeck project (one of the main purposes of which is to certify numerical inequalities used in the proof of the Kepler conjecture by Thomas Hales).
Type de document :
Communication dans un congrès
European Control Conference (ECC'13), Jul 2013, Zurich, Switzerland. pp.2244 - 2250, 2013
Liste complète des métadonnées

https://hal.inria.fr/hal-00932348
Contributeur : Xavier Allamigeon <>
Soumis le : jeudi 16 janvier 2014 - 17:26:11
Dernière modification le : jeudi 10 mai 2018 - 02:06:51

Lien texte intégral

Identifiants

  • HAL Id : hal-00932348, version 1
  • ARXIV : 1307.7002

Citation

Xavier Allamigeon, Stéphane Gaubert, Victor Magron, Benjamin Werner. Certification of inequalities involving transcendental functions: combining SDP and max-plus approximation. European Control Conference (ECC'13), Jul 2013, Zurich, Switzerland. pp.2244 - 2250, 2013. 〈hal-00932348〉

Partager

Métriques

Consultations de la notice

427