{"id":4748,"date":"2015-01-29T08:26:14","date_gmt":"2015-01-29T07:26:14","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4748"},"modified":"2015-01-29T08:26:15","modified_gmt":"2015-01-29T07:26:15","slug":"resena-formal-proofs-for-nonlinear-optimization","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-formal-proofs-for-nonlinear-optimization\/","title":{"rendered":"Rese\u00f1a: Formal proofs for nonlinear optimization"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"https:\/\/coq.inria.fr\/\">Coq<\/a> titulado <a href=\"http:\/\/jfr.unibo.it\/article\/download\/4319\/4160\">Formal proofs for nonlinear optimization<\/a>.<\/p>\n<p>Sus autores son<\/p>\n<ul>\n<li><a href=\"http:\/\/cas.ee.ic.ac.uk\/people\/vmagron\">Victor Magron<\/a> (del grupo <a href=\"http:\/\/www3.imperial.ac.uk\/circuitssystems\">Circuits and Systems<\/a> en el Imperial College de Londres, Reino Unido),<\/li>\n<li><a href=\"http:\/\/www.cmap.polytechnique.fr\/~allamigeon\">Xavier Allamigeon<\/a> (del grupo <a href=\"http:\/\/team.inria.fr\/maxplus\">Maxplus<\/a> del INRIA y del CMAP, \u00c9cole Polytechnique, CNRS, Palaiseau, Francia),<\/li>\n<li><a href=\"http:\/\/www.cmap.polytechnique.fr\/~gaubert\">St\u00e9phane Gaubert<\/a> (del grupo <a href=\"http:\/\/team.inria.fr\/maxplus\">Maxplus<\/a> del INRIA y del CMAP, \u00c9cole Polytechnique, CNRS, Palaiseau, Francia) y<\/li>\n<li><a href=\"http:\/\/www.lix.polytechnique.fr\/Labo\/Benjamin.Werner\">Benjamin Werner<\/a> (del LIX, \u00c9cole Polytechnique, CNRS, Palaiseau, Francia)<\/li>\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  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.<\/p>\n<p>  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.<\/p>\n<p>  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.<\/p>\n<p>  The application range for such a tool is widespread; for instance Hales&#8217; proof of Kepler&#8217;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.\n<\/p><\/blockquote>\n<p>El trabajo se ha publicado en el <a href=\"http:\/\/jfr.unibo.it\/article\/view\/4319\">Journal of Formalized Reasoning<\/a>.<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Coq se encuentra <a href=\"http:\/\/nl-certify.forge.ocamlcore.org\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq titulado Formal proofs for nonlinear optimization. Sus autores son Victor Magron (del grupo Circuits and Systems en el Imperial College de Londres, Reino Unido), Xavier Allamigeon (del grupo Maxplus del INRIA y del CMAP, \u00c9cole Polytechnique, CNRS, Palaiseau, Francia), St\u00e9phane Gaubert (del grupo Maxplus del&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[100],"tags":[45,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4748"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=4748"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4748\/revisions"}],"predecessor-version":[{"id":4749,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4748\/revisions\/4749"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4748"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4748"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4748"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}