Transforming Optimization Problems into Disciplined Convex Programming Form

Disciplined convex programming (Dcp) is a popular framework for systematically reducing convex optimization problems to the low-level conic form commonly used by convex solvers. An arbitrary convex problem may not immediately be in a Dcp-compliant form, and several manual and error-prone steps are often needed to transform it into an equivalent form that is accepted by Dcp frameworks. We automate this process in CvxLean, a convex optimization modeling framework embedded in the Lean theorem prover. While the steps can be described using rewrite rules, there are not clear heuristics for orienting and applying them. Instead, we carry out an efficient breadth-first search for a suitable sequence of steps by making use of the egg e-graph-based term rewriting system. When egg finds a suitable sequence, we automatically prove it correct in Lean. This procedure is the first generic, proof-producing approach to transform a wide range of optimization problems into Dcp-compliant forms. Moreover, it is an important step towards a fully-verified and user-friendly convex programming environment.