OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations

Martin-Dorel, Erik and Roux, Pierre A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations. (2017) In: 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017), 16 January 2017 - 17 January 2017 (Paris, France).

Full text not available from this repository.

Official URL: http://dx.doi.org/10.1145/3018610.3018622


Polynomial positivity over the real field is known to be decidable but even the best algorithms remain costly. An incomplete but often efficient alternative consists in looking for positivity witnesses as sum of squares decompositions. Such decompositions can in practice be obtained through convex optimization. Unfortunately, these methods only yield approximate solutions. Hence the need for formal verification of such witnesses. State of the art methods rely on heuristic roundings to exact solutions in the rational field. These solutions are then easy to verify in a proof assistant. However, this verification often turns out to be very costly, as rational coefficients may blow up during computations. Nevertheless, overapproximations with floating-point arithmetic can be enough to obtain proofs at a much lower cost. Such overapproximations being non trivial, it is mandatory to formally prove that rounding errors are correctly taken into account. We develop a reflexive tactic for the Coq proof assistant allowing one to automatically discharge polynomial positivity proofs. The tactic relies on heavy computation involving multivariate polynomials, matrices and floating-point arithmetic. Benchmarks indicate that we are able to formally address positivity problems that would otherwise be untractable with other state of the art methods.

Item Type:Conference or Workshop Item (Paper)
Additional Information:The definitive version is available at http://dl.acm.org This papers appears in CPP 2017, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs ISBN: 978-1-4503-4705-1 The original PDF is available at: https://dl.acm.org/citation.cfm?doid=3018610.3018622
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - INPT (FRANCE)
French research institutions > Office National d'Etudes et Recherches Aérospatiales - ONERA (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UPS (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
FAGames project of LabEx CIMI, the French ANR project ANR-12-INSE-0007 Cafein and the project SEFA IKKY.
Deposited By: IRIT IRIT
Deposited On:05 Feb 2018 12:51

Repository Staff Only: item control page