Verified transformations for convex programming

Abstract

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.