Intern paper at LICS 2021

Our research intern Todd Waugh Ambridge will present the paper Global Optimisation with Constructive Reals at the ACM/IEEE Symposium on Logic in Computer Science.

Abstract—We draw new connections between deterministic, complete, and general global optimisation of continuous functions and a generalised notion of regression, using constructive type theory and computable real numbers. Using this foundation we formulate novel convergence criteria for regression, derived from the convergence properties of global optimisations. We see this as possibly having an impact on optimisation-based computational sciences, which include much of machine learning. Using computable reals, as opposed to floating-point representations, we can give strong theoretical guarantees in terms of both precision and termination. The theory is fully formalised using the safe mode of the proof assistant AGDA. Some examples implemented using an off-the-shelf constructive reals library in JAVA indicate that the approach is algorithmically promising.

Link to the video presentation: https://youtu.be/Sf3EmMxCNE4

Link to the paper: https://www.cs.bham.ac.uk/~txw467/lics21.pdf

The full program of the conference is at http://easyconferences.eu/lics2021/program/ .