Linear programming

Stream: Program verification

[Martin Dvořák]

Is there any formally-verified LP solver? In Lean would be best, but I am interested in a formally-verified LP solver in any language. In particular, I'd like to have one of those that are proven to run in polynomial time (worst case), that is not the simplex method. Even if the time complexity hasn't been formally verified.

[Karl Palmskog]

https://github.com/coq-polyhedra/coq-polyhedra and https://www.isa-afp.org/entries/Linear_Programming.html

[Martin Dvořák]

How much work do you think it would be if I wanted to formally verify the ellipsoid method? Let me leave the time complexity aside for a while.

Let's say I want to formalize the ellipsoid method and prove its correctness (for LP as a decision problem over rational numbers). In terms of being a Ph.D. student, could it be, for example, half of the dissertation thesis? Any estimate?

[Karl Palmskog]

effort probably varies a lot with what prover you use (existing libraries vs building new). A verified LP solver usable in practice would probably amount to about one paper in ITP or CPP or IJCAR. In some places, PhD students are expected to co-author maybe 3-4 such papers

[Martin Dvořák]

Karl Palmskog said:

effort probably varies a lot with what prover you use (existing libraries vs building new). A verified LP solver usable in practice would probably amount to about one paper in ITP or CPP or IJCAR. In some places, PhD students are expected to co-author maybe 3-4 such papers

By co-author, you mean a Ph.D. student working on it together with their supervisor? Or in a larger team?

[Karl Palmskog]

going from "verified LP solver" to person month estimation is going to yield false precision anyway. I'm not going to guess any more than that it's about one paper in ITP/CPP

[Martin Dvořák]

Thank you. I know it is impossible to tell beforehand how long a certain project will take, especially in this area. However, my motivation for asking these questions is the following.

My supervisor suggested that I should work on formal verification that LP is solvable in polynomial time. However, it would not be the whole dissertation project; it would be just one major step towards proving other complexity-theoretic results. And to me, it sounds like an overkill. Nevertheless, I wanted to ask someone else — I have no experience but someone else might have some.

[Karl Palmskog]

verifying complexity is a whole topic of its own. If you want to verify complexity, you probably want to look at libraries for that, such as: https://github.com/uds-psl/coq-library-complexity

Example paper proving functional correctness + complexity for a practical executable algorithm implementation (ITP '19): http://gallium.inria.fr/~fpottier/publis/gueneau-jourdan-chargueraud-pottier-2019.pdf

[Martin Dvořák]

I have been looking into Fabian Funze's projects. I am aware that no similar library is available in Lean right now.

Nevertheless, even if I worked in a language that has great libraries for complexity theory ready, I would still have to implement the algorithm and verify its correctness before I could establish the time complexity of LP as a decision problem. And, if this part is going to take half of my Ph.D. working timespan, I won't choose a dissertation project that has it [LP \in P] as a prerequisite.

[Karl Palmskog]

the approach by Chargueraud et al. for complexity is different from Kunze et al's work: https://gitlab.inria.fr/charguer/cfml2/-/tree/master/theories#model-of-separation-logic-with-time-credits

[Mario Carneiro]

LP solution verification is easy, because it can be expressed as a feasible point of the dual. If I were creating an LP solver in lean that is certainly what I would do. This does not address the complexity bounds but it's not clear to me whether you are actually trying to do this (and there is a huge amount of work to be done to get to the point where we can prove this, although you can shortcut some things if you want to skip to the good part)

[Karl Palmskog]

"solution verification", you mean translation validation? Unverified solution generation?

[Karl Palmskog]

if the goal is just a verified LP solution, then sure, but I don't think PC of ITP or CPP would be impressed

[Karl Palmskog]

Coq's lia tactic uses simplex by default and its proposed solution gets verified at Qed, so I guess it would qualify then (https://coq.inria.fr/refman/addendum/micromega.html)

[Joe Hendrix]

I think proving complexity theoretic results of decision procedures is a pretty niche topic.
On the one hand, if you are really excited about the topic, then a PhD would be a good opportunity to work on it. However, you are likely going to have to formalize a large amount of basics, and then formalize the algorithm itself (rather than just functional code that implements the decision procedure).
On the other hand, there is a lot of interest in actually having unverified efficient decision procedures in the FM academic community and industry (for specific decision problems). Very few people care about the complexity theory though (producing proofs of unsat has a bit more interest as you can leverage the proofs).

[Karl Palmskog]

my impression is that the "We verified algorithm X" papers are getting harder to sell without bells and whistles (unless the properties are exceptionally challenging to state and verify). People like code with machine-checked functional correctness, but it now is expected to come with performance evals and optimizations. One opportunity when code is verified might be to try crazy optimization techniques that real implementations won't try due to worry about bugs.

[Karl Palmskog]

Seminal example from the Coq community: https://github.com/mit-plv/fiat-crypto

[Martin Dvořák]

Mario Carneiro said:

LP solution verification is easy, because it can be expressed as a feasible point of the dual. If I were creating an LP solver in lean that is certainly what I would do. This does not address the complexity bounds but it's not clear to me whether you are actually trying to do this (and there is a huge amount of work to be done to get to the point where we can prove this, although you can shortcut some things if you want to skip to the good part)

It is what I would need to do in order to work on my supervisor's project. And it makes me nervous.

[Mario Carneiro]

The "skip to the good part" way to formalize computational complexity is to define a step-counting monad and write the algorithm in the monad, and prove bounds on how many steps are executed

[Mario Carneiro]

import data.list.basic

structure with_steps (α : Type*) := (steps : ℕ) (val : α)

def step {α} (a : α) : with_steps α := ⟨1, a⟩

@[simp] def delay {α} (n : ℕ) : with_steps α → with_steps α
| ⟨m, a⟩ := ⟨n + m, a⟩

instance : monad with_steps :=
{ pure := λ α a, ⟨0, a⟩,
  map := λ α β f ⟨n, a⟩, ⟨n, f a⟩,
  bind := λ α β ⟨n, a⟩ f, delay n (f a) }

@[simp] theorem pure_def {α} (a : α) : (pure a : with_steps α) = ⟨0, a⟩ := rfl
@[simp] theorem map_def {α β} (f : α → β) (n : ℕ) (a : α) : f <$> with_steps.mk n a = ⟨n, f a⟩ := rfl
@[simp] theorem bind_def {α β} (f : α → with_steps β) (n : ℕ) (a : α) :
  with_steps.mk n a >>= f = delay n (f a) := rfl

theorem list.map_is_linear_time {α β} (f : α → β) (l : list α) :
  l.mmap (λ a, step (f a)) = ⟨l.length, l.map f⟩ :=
by simp [step]; induction l; simp [mmap, return, add_comm, *]

[Martin Dvořák]

Mario Carneiro said:

The "skip to the good part" way to formalize computational complexity is to define a step-counting monad and write the algorithm in the monad, and prove bounds on how many steps are executed

What "features" would be "lost" if we used this approach?

[Mario Carneiro]

You are taking the computational model on faith here. That is, you get to say what is constant time, and you have to be careful to apply step everywhere it is needed, because if you don't you can prove bad things:

theorem list.map_is_constant_time {α β} (f : α → β) (l : list α) :
  (l.mmap (λ a, pure (f a)) : with_steps _) = ⟨0, l.map f⟩ :=
by simp [step]; induction l; simp [mmap, return, add_comm, *]

[Mario Carneiro]

Some other things you might want to take as axiomatic are, for example, the cost of performing addition or multiplication of elements of the base field

[Martin Dvořák]

True. Thanks.

[Mario Carneiro]

One recent paper I read that demonstrates this approach well is Hing Lun Chan's thesis Primality Testing is Polynomial-time: A Mechanised Verification of the AKS Algorithm, which proves the "PRIMES is in P" algorithm (both correctness and complexity bounds) in HOL4. See chapter 6 for the step counting stuff

[Martin Dvořák]

Mario Carneiro said:

LP solution verification is easy, because it can be expressed as a feasible point of the dual. If I were creating an LP solver in lean that is certainly what I would do.

Has the weak duality of LP been proved in Lean/mathlib already?

[Mario Carneiro]

There isn't a general theory of LPs in mathlib, so I think the answer is no unless it is a simple application of a theorem about matrices

[Martin Dvořák]

Actually, it is a simple application of the arithmetic of matrices.

[Martin Dvořák]

Actually, I don't know why the authors of https://www.isa-afp.org/entries/Linear_Programming.html emphasized in the abstract that they proved the weak duality of LP themselves.

[Mario Carneiro]

I think they are just pointing out the important theorems in the article, so that you know where to look to find the weak duality theorem. By reading the abstract you can see that the weak duality theorem is there but the simplex algorithm is not, even though you might guess it is the other way around.

[Martin Dvořák]

BTW, is there any kind of RAM model with step counting formalized in any language?

[David Wärn]

Strong duality for linear programming over the reals should follow from #7288

[Shreyas Srinivas]

David Wärn said:

Strong duality for linear programming over the reals should follow from #7288

I can intuit why weak duality would follow from hahn banach separation. How does strong duality follow?

[Shreyas Srinivas]

My intuition : Farkas Lemma is a version of Hahn Banach separation.

[Shreyas Srinivas]

Correction: I can't see why weak duality follows

[Shreyas Srinivas]

Update: I see what was meant now. But it still seems some translation is needed to bring about the LP formulation.

[Martin Dvořák]

LP duality is definitely on my wish list.

[Chris Hughes]

I did some work on this three years ago. https://github.com/ChrisHughes24/LP/blob/e3ed64c2d1f642696104584e74ae7226d8e916de/src/simplex2.lean#L646 If you're interested I can talk to you about it, but it might take some time for me to remember how to navigate this repository.

[Martin Dvořák]

Woah! Is it (both implementation and verification) finished?

[Chris Hughes]

Yes, and there's a more efficient version using array matrices which is also verified. I don't think I did Farka's lemma and to be honest I have trouble remembering what all the theorems are. I think the duality stuff is fairly straightforward once you have a verified terminating simplex algorithm. Termination was a tricky to prove I remember.

[Chris Hughes]

@Martin Dvořák Did you have any plans to go further with this? I'm considering revisiting this work.

[Martin Dvořák]

Imma be busy until 2023-03-10 with my current stuff. In mid-March, I will be deciding what to do next. The decision will mostly depend on how this community about doing complexity theory for mathlib4. Therefore, I cannot tell you right now whether I will use your code in my work.

[Martin Dvořák]

What is the status now? What theorem in Mathlib4 is closest to the strong LP duality?

[Martin Dvořák]

Let me get started!
https://github.com/leanprover-community/mathlib4/pull/7386
I want to hear opinions!