Certification of Bounds of Non-linear Functions: the Templates Method

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 : 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.
Type de document :
Communication dans un congrès
Jacques Carette and David Aspinall and Christoph Lange and Petr Sojka and Wolfgang Windsteige. Conferences on Intelligent Computer Mathematics (CICM 2013), Jul 2013, Bath, United Kingdom. Springer Berlin Heidelberg, 7961, pp.51-65, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-39320-4_4〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00932333
Contributeur : Xavier Allamigeon <>
Soumis le : jeudi 16 janvier 2014 - 17:02:29
Dernière modification le : jeudi 12 avril 2018 - 01:46:58

Lien texte intégral

Identifiants

Collections

Citation

Xavier Allamigeon, Stéphane Gaubert, Victor Magron, Benjamin Werner. Certification of Bounds of Non-linear Functions: the Templates Method. Jacques Carette and David Aspinall and Christoph Lange and Petr Sojka and Wolfgang Windsteige. Conferences on Intelligent Computer Mathematics (CICM 2013), Jul 2013, Bath, United Kingdom. Springer Berlin Heidelberg, 7961, pp.51-65, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-39320-4_4〉. 〈hal-00932333〉

Partager

Métriques

Consultations de la notice

327