BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Computational Optimisation Group - ECPv6.15.11//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:Computational Optimisation Group
X-ORIGINAL-URL:https://optimisation.doc.ic.ac.uk
X-WR-CALDESC:Events for Computational Optimisation Group
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:UTC
BEGIN:STANDARD
TZOFFSETFROM:+0000
TZOFFSETTO:+0000
TZNAME:UTC
DTSTART:20140101T000000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=UTC:20150303T140000
DTEND;TZID=UTC:20150303T140000
DTSTAMP:20260403T184839
CREATED:20170124T102138Z
LAST-MODIFIED:20170124T102138Z
UID:560-1425391200-1425391200@optimisation.doc.ic.ac.uk
SUMMARY:Seminar: Formal Proofs for Nonlinear Optimization
DESCRIPTION:Title: Formal Proofs for Nonlinear OptimizationSpeaker: Dr. Victor MagronAffiliation: Department of Electrical and Electronic Engineering – Imperial College LondonLocation: Room 217 Huxley BuildingTime: 2:00pm \nAbstract. 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 algorithm 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 semidefinite 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.http://cas.ee.ic.ac.uk/people/vmagron/slides/quads.pdf \nAbout the speaker. Victor graduated from Ecole Centrale Paris Engineering School in 2010\, while receiving his MSc from the department of Systems Innovation\, Tokyo University (double diploma). In 2013\, he received his PhD in Computer Science at INRIA Saclay\, Ecole Polytechnique. In 2014\, he was a Postdoc fellow in the MAC team at LAAS in Toulouse\, France. He is currently a Research Assistant at Imperial College for the Circuits and Systems group\, in the department of Electrical and Electronic Engineering.
URL:https://optimisation.doc.ic.ac.uk/event/seminar-formal-proofs-for-nonlinear-optimization/
END:VEVENT
END:VCALENDAR