CvxLean: modeling convex optimization problems in Lean

Stream: Lean Together 2024

[Andrés Goens]

@Ramon Fernández Mir is there a fundamental reason why you don't do the change of variables in the equality saturation part as a rewrite?

[Ramon Fernández Mir]

That is a great question!! I tried to do that initially.

If you do it naively by adding a rule that merges $x$ and $e^{x'}$, then you have an issue when analyzing curvatures because the same e-class could have $\log(x)$, $x'$ and $e^{x''}$. I assume that terms represented by the same e-class only have one known curvature (e-classes will have nodes that are a mixture of {DCP unknown, DCP convex} or {DCP unknown, DCP concave} or {DCP unknown, DCP affine}). Or, in other words, rewrites preserve the "mathematical" curvature of expressions.

I think it might be possible to make egg explore changes of variables, but it is not straightforward because they are a problem-level transformation, so it cannot be done locally by replacing var nodes.

[Ramon Fernández Mir]

It was also a bit of a design decision, where I wanted to split what the user does and what egg can do more clearly. But if we could use egg to discover changes of variables, that would be very cool, especially for more complicated ones.

[Andrés Goens]

oh interesting! Yeah that makes sense, the change of variables does not fall into the type of equivalence of terms you're considering there? even if the resulting domains are equivalent?

[Andrés Goens]

or is it more subtle (that the convexity is not an invariant of the equivalence class of the terms)?

[Martin Dvořák]

When working with Matrix.Computable.dotProduct, can you reuse mathlib theorems about Matrix.dotProduct?

[Ramon Fernández Mir]

Andrés Goens said:

oh interesting! Yeah that makes sense, the change of variables does not fall into the type of equivalence of terms you're considering there? even if the resulting domains are equivalent?

Basically they are not a "rewrite" but rather a map $(f, cs) => (f \circ g, cs \circ g)$ where $g$ is the change of variables. Note that this is an issue because what we send egg is the "skolemized" objective function and constraints. So in order to do that properly, we would need to have functions (so you have to deal with binders, which is annoying in egg) as part of our language in egg and rules for composition. If we had that, then you could add it as a rewrite rule.

We support some maps, but these are of the form $(f, cs) => (m \circ f, cs)$, which are easy to simulate as rewrites.

[Ramon Fernández Mir]

Martin Dvořák said:

When working with Matrix.Computable.dotProduct, can you reuse mathlib theorems about Matrix.dotProduct?

No, we indeed lose any lemma about dot products. These are only used once you have your reduced problem and you want to extract the coefficients so that you can solve it (say, a constraint is posOrthCone (dotProduct a x) where a is constant). Then, in general, you need to compute to extract a. So we replace every real function by its floating-point counter parts and get the coefficients of the problem. And we do not prove any correctness result about that step.

[Ramon Fernández Mir]

Ramon Fernández Mir said:

Andrés Goens said:

oh interesting! Yeah that makes sense, the change of variables does not fall into the type of equivalence of terms you're considering there? even if the resulting domains are equivalent?

Basically they are not a "rewrite" but rather a map $(f, cs) => (f \circ g, cs \circ g)$ where $g$ is the change of variables. Note that this is an issue because what we send egg is the "skolemized" objective function and constraints. So in order to do that properly, we would need to have functions (so you have to deal with binders, which is annoying in egg) as part of our language in egg and rules for composition. If we had that, then you could add it as a rewrite rule.

We support some maps, but these are of the form $(f, cs) => (m \circ f, cs)$, which are easy to simulate as rewrites.

Here by $(f,cs)$ I mean objective function $f$ and constraints $cs$

[Martin Dvořák]

Ramon Fernández Mir said:

Martin Dvořák said:

When working with Matrix.Computable.dotProduct, can you reuse mathlib theorems about Matrix.dotProduct?

No, we indeed lose any lemma about dot products. These are only used once you have your reduced problem and you want to extract the coefficients so that you can solve it (say, a constraint is posOrthCone (dotProduct a x) where a is constant). Then, in general, you need to compute to extract a. So we replace every real function by its floating-point counter parts and get the coefficients of the problem. And we do not prove any correctness result about that step.

You define Matrix.Computable.dotProduct generically but then you use it only for α being Float? Or are there also integer types?

[Ramon Fernández Mir]

It is only used for Float at the moment