CvxLean
CvxLean is a convex optimization modeling framework written in Lean 4.
Problems are stated using definitions from mathlib and can be rigorously transformed both automatically and interactively. They can be solved by calling the backend solver MOSEK.
Summary of features:
- Formal definitions. Users can define optimization problems in a natural way using custom syntax. These are formal objects we can reason about; usually, we want to talk about equivalences, reductions, and relaxations.
- User-guided transformations. For each relation (equivalence, reduction, and relaxation), we have formalized several relation-preserving transformations. These are realized as tactics and can be applied interactively in the
equivalence
,reduction
, orrelaxation
commands. - Proof-producing DCP transformation. Our main contribution is a verified version of the disciplined convex programming (DCP) canonization algorithm. It can be used through the
dcp
tactic. Thesolve
command also uses it behind the scenes. - Automatic transformation into DCP form. The
pre_dcp
tactic uses egg to find a sequence of rewrites to turn a problem into an equivalent DCP-compliant problem.
Auto-generated documentation can be found here.
Contents
Installation
You will need to install Lean, Rust and MOSEK following these steps:
- Set up Lean 4 (see these instructions).
- The easiest way is to use the
elan
version manager. - If you're using VSCode, install the Lean 4 extension.
- The easiest way is to use the
- Install Rust (see these instructions). This step is only necessary to enable the
pre_dcp
tactic. - Download MOSEK 10.0.12(BETA).
- Make sure that the directory containing the
mosek
binary is in your$PATH
. - To avoid any issues with this, we recommend also adding it to
CvxLean/Command/Solve/Mosek/Path.lean
. - Obtain a MOSEK license and place it in your home directory, i.e.
$HOME/mosek/mosek.lic
.
- Make sure that the directory containing the
Finally, go into the top CvxLean
directory and run:
./build.sh
Usage
One of the best ways to get started is to take a look at the examples in CvxLean/Test
and CvxLean/Examples
. We provide a short guide here.
Defining problems
Consider the optimization problem:
In CvxLean, it is defined as follows (see Test/Solve/Problems/SO.lean
):
def p :=
optimization (x y : ℝ)
maximize sqrt (x - y)
subject to
c₁ : y = 2 * x - 3
c₂ : x ^ 2 ≤ 2
c₃ : 0 ≤ x - y
This is a term of type Minimization (ℝ × ℝ) ℝ
. Our syntax allows us to use variable names and also name constraints, which is useful for referring to them.
An important remark is that we require the condition 0 ≤ x - y
, which is usually omitted, as CvxLean
will need to know that the square root application in the objective function is well-defined to produce a proof of equivalence between p
and its conic form counterpart.
Solving problems
Once p
has been defined, we can ask CvxLean to solve it as follows.
solve p
This command canonizes p
and calls MOSEK.
If successful, it will add several definitions to the environment:
p.conicForm
: the conic form of the problem after applying the DCP canonization procedure.p.status
: the feasibility status of the primal and the dual problem, in this case"PRIMAL_AND_DUAL_FEASIBLE"
, i.e. optimal.p.value
: if the problem is optimal, it corresponds to the (approximate) optimal value.p.solution
: if the problem is optimal, it corresponds to the (approximate) optimal point.
Crucially, we formally verify that p
is equivalent to p.conicFrom
.
In this case, p.solution
is
Transforming problems
Problems can also be transformed interactively. We will show the commands and tactics that we provide for this purpose.
Commands for user-guided transformations
To motivate the need for this, we start with a simple example.
Suppose our problem has
equivalence eqv/q :
optimization (x y : ℝ)
maximize x + y
subject to
h : (exp x) * (exp y) ≤ 10 := by
conv_constr =>
rw [← exp_add]
#print q
-- def q : Minimization (ℝ × ℝ) ℝ :=
-- optimization (x : ℝ) (y : ℝ)
-- maximize x + y
-- subject to
-- h : exp (x + y) ≤ 10
The transformation is done in a verified way using the lemma exp_add
from mathlib, which says that eqv
) between the initial problem and q
.
There are three commands for user-guided transformations, each enforcing a different proof term to be generated. They all have the form command pf/q : p
, where p
is the initial problem, q
is the resulting problem and pf
is the correctness proof. A sequence of tactics in these commands generates q
and pf
.
equivalence
: the goal is to showp ≡ q
. Mathematically, ifis a problem over and is a problem over , equivalence is witnessed by a pair of functions and such that maps solutions of to solutions of and maps solutions of to solutions of . reduction
: the goal is to showp ≼ q
. In this case, only a solution-preservingis required. relaxation
: the goal is to showp ≽' q
. Here, only a feasibility-preservingis required, with the additional requirement that for all -feasible , where and are the objective functions of and , respectively.
A small implementation detail is that the goal is actually set up with a metavariable, e.g. ⊢ p ≡ ?q
. The user transforms the left-hand side and the final state is closed by reflexivity, which instantiates ?q
with the problem shown in the last step.
Users rarely build
Equivalence-preserving tactics
The commands set the environment for verified transformations, but what tactics should one use? We have several specialized equivalence-preserving tactics (e.g., conv_constr
above), which we explain here. We split them into two groups.
Fully automated:
dcp
transforms a problem into conic form.pre_dcp
transforms a problem into DCP form.
User-directed:
conv_constr h => ...
andconv_obj => ...
are used to travel to one of the components of the problem in order to rewrite or simplify it (they are special cases of Lean's conv).rw_constr h => ...
andrw_obj => ...
are used similarly to the previous ones but used for conditional rewrites. Sometimes rewrites are only valid withing the feasible set of the problem, these tactics will assume the appropriate constraints.change_of_variables (u) (x ↦ ...)
, whereu : ℝ
is a new variable andx : ℝ
is an optimization variable (we currently only support real variables). It performs a change of variables, using a pre-defined library of valid changes, and proves any side conditions that arise.remove_constr h => ...
requires a proof that the constrainth
is implied from the other constraints, in which case it can be removed.rename_constrs [h₁, h₂, ...]
andrename_vars [x₁, x₂, ...]
are used to give new names to constraints and variables, respectively. They are useful for visualization purposes. Similarly,reorder_constrs [h₁, h₂, ...]
will reorder the constraints given a permutation of the constraint names.- Any lemma that proves an equivalence can be used as a tactic. To achieve the desired effect, it must be used in combination with
equivalence_step => ...
. For example,map_objFun_log
states that applyingto the objective function yields an equivalence (if the objective function is positive in the feasible set). One can write equivalence_step => apply map_objFun_log (...)
. In the future, all these transformations will be wrapped as tactics.
Quick demo
We show how to rigorously transform and solve the following problem in CvxLean:
Note that the solution is
You can find this example in CvxLean/Demos/README.lean
.
Citing
@inproceedings{bentkamp2023verified,
title={Verified reductions for optimization},
author={Bentkamp, Alexander and Fern{\'a}ndez Mir, Ramon and Avigad, Jeremy},
booktitle={International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
pages={74--92},
year={2023},
organization={Springer}
}
Contributing
There are many opportunities to improve CvxLean and many features that we would like to see implemented, so we welcome any contributions!
Some things to keep in mind when opening a pull request:
- Follow Lean's commit convention.
- Follow mathlib's style guidelines (style is actually checked in CI).