Jackson, Paul

Fleuriot, Jacques

Fernández Mir, Ramon

2024-08-06T10:03:31Z

2024-08-06T10:03:31Z

2024-08-06

This thesis is concerned with developing and enhancing several components of CvxLean, a convex optimization modeling framework based on the mechanical proof assistant Lean 4. Convex programming studies the class of optimization problems that are either convex (convex objective function and feasible set) or equivalent to a convex problem. In practice, solvers expect the input to be in conic form, a low-level representation of the problem. Transforming a problem to an equivalent problem in conic form is not straightforward. It often requires several steps and uses properties of the functions involved in the problem in nontrivial ways. This is exactly the process that we formally verify in this work. The main transformation we verified is the "DCP transformation" step. This required formalizing and extending disciplined convex programming (DCP), a popular technique to transform problems into conic form. It works by iteratively replacing applications of well-understood functions with new variables and conic constraints. In our development, each replacement is augmented with proof obligations that are then combined to produce an overall proof of equivalence between the starting problem and its conic form counterpart. DCP requires problems to follow a strict set of rules. Often, users need to adjust how they write problems to follow these rules. Instead, we propose an automated and verified "pre-DCP transformation" step using an e-graph-based rewriting system. This procedure explores the space of equivalent problems and finds a sequence of rewrites to transform initial user problems into DCP-compliant forms. The applicability of the methods that we describe throughout the thesis to real-world problems is backed by a number of examples and case studies.

https://hdl.handle.net/1842/42057

http://dx.doi.org/10.7488/era/4779

en

The University of Edinburgh

Alexander Bentkamp, Ramon Fernández Mir, and Jeremy Avigad. Verified reductions for optimization. In Sriram Sankaranarayanan and Natasha Sharygina, editors, Tools and Algorithms for the Con struction and Analysis of Systems - 29th International Confer ence, TACAS 2023, Held as Part of the European Joint Confer ences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II, volume 13994 of Lecture Notes in Computer Science, pages 74–92. Springer, 2023. doi:10.1007/978-3-031-30820-8\_8

Kevin Buzzard, Chris Hughes, Kenny Lau, Amelia Livingston, Ra mon Fernández Mir, and Scott Morrison. Schemes in Lean. Exp. Math., 31(2):355–363, 2022. doi:10.1080/10586458.2021.1983489

theorem proving

formal verification

proof assistants

Lean

convex optimization

convex programming

Verified transformations for convex programming

Thesis or Dissertation

Doctoral

PhD Doctor of Philosophy