AIAI Seminar - 03 March 2025 - Paul Jackson Speaker: Paul JacksonTitle: Verified Transformations for Convex Optimization Abstract:Convex optimization is a generalisation of linear programming. Instead of having linear equalities and inequalities defining a feasible set of points and a linear objective to be optimized, one also allows non-linear inequalities such that the feasible set is convex, and only require the objective function to be a convex function.In recent decades, interior point solution methods have given rise to a number of commercial and open-source convex optimization solvers, which have a variety of applications in engineering, industry and finance. Convex optimization problems are often expressed in a much richer language than the solvers take as input, and a variety of methods have been developed for automatically transforming problems into solver input formats. One popular scheme is Disciplined Convex Programming (DCP).I will talk about the recent work of my former PhD student Ramon Fernández Mir in developing a framework in the Lean proof assistant that formalizes and supports the application of DCP transformations. In this framework, transformation steps have to be proved correct, and the work uncovered a bug in the popular CvxPy DCP framework. A further advantage of using a proof assistant environment is that additional formal front-end problem transformations can be manually guided to reach the starting point of the DCP approach. This guiding can be rather tedious, and recent work has explored using e-graph rewriting to discover these front-end transformations automatically.The talk will assume no prior familiarity with convex optimization, proof assistants, or e-graph rewriting. For further information, consult Ramon's 2024 PhD thesis "Verified transformations for convex programming" https://era.ed.ac.uk/handle/1842/42057 and the following papers: "Transforming optimization problems into Disciplined Convex Programming form" R. Fernández Mir, P. Jackson, S. Bhat, A. Goens, T. Grosser International Conference on Intelligent Computer Mathematics (CICM). 2024. https://link.springer.com/chapter/10.1007/978-3-031-66997-2_11 "Verified reductions for optimization" A. Bentkamp, R. Fernández Mir, J. Avigad International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 2023. https://link.springer.com/chapter/10.1007/978-3-031-30820-8_8 For the code, visit:https://github.com/verified-optimization/CvxLean Mar 03 2025 14.00 - 15.00 AIAI Seminar - 03 March 2025 - Paul Jackson Hosted by AIAI Director Paul Jackson. G.03, Informatics Forum
AIAI Seminar - 03 March 2025 - Paul Jackson Speaker: Paul JacksonTitle: Verified Transformations for Convex Optimization Abstract:Convex optimization is a generalisation of linear programming. Instead of having linear equalities and inequalities defining a feasible set of points and a linear objective to be optimized, one also allows non-linear inequalities such that the feasible set is convex, and only require the objective function to be a convex function.In recent decades, interior point solution methods have given rise to a number of commercial and open-source convex optimization solvers, which have a variety of applications in engineering, industry and finance. Convex optimization problems are often expressed in a much richer language than the solvers take as input, and a variety of methods have been developed for automatically transforming problems into solver input formats. One popular scheme is Disciplined Convex Programming (DCP).I will talk about the recent work of my former PhD student Ramon Fernández Mir in developing a framework in the Lean proof assistant that formalizes and supports the application of DCP transformations. In this framework, transformation steps have to be proved correct, and the work uncovered a bug in the popular CvxPy DCP framework. A further advantage of using a proof assistant environment is that additional formal front-end problem transformations can be manually guided to reach the starting point of the DCP approach. This guiding can be rather tedious, and recent work has explored using e-graph rewriting to discover these front-end transformations automatically.The talk will assume no prior familiarity with convex optimization, proof assistants, or e-graph rewriting. For further information, consult Ramon's 2024 PhD thesis "Verified transformations for convex programming" https://era.ed.ac.uk/handle/1842/42057 and the following papers: "Transforming optimization problems into Disciplined Convex Programming form" R. Fernández Mir, P. Jackson, S. Bhat, A. Goens, T. Grosser International Conference on Intelligent Computer Mathematics (CICM). 2024. https://link.springer.com/chapter/10.1007/978-3-031-66997-2_11 "Verified reductions for optimization" A. Bentkamp, R. Fernández Mir, J. Avigad International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 2023. https://link.springer.com/chapter/10.1007/978-3-031-30820-8_8 For the code, visit:https://github.com/verified-optimization/CvxLean Mar 03 2025 14.00 - 15.00 AIAI Seminar - 03 March 2025 - Paul Jackson Hosted by AIAI Director Paul Jackson. G.03, Informatics Forum
Mar 03 2025 14.00 - 15.00 AIAI Seminar - 03 March 2025 - Paul Jackson Hosted by AIAI Director Paul Jackson.
