Verifying backtracking algorithms

Stream: general

[Jineon Baek]

Hi! I'm Jin, a graduate student at UMich currently learning Lean for possible use in my research. In particular, I've been working on a problem called the moving sofa problem (see here for a brief description) for a while. I'm trying to improve the upper bound of the sofa area using computer-assisted approaches, and I want to formalize the result in Lean. The proof is still in progress, but I would like to get a general idea of what would be a realistic expectation I could have from Lean beforehand.

A major portion of my work in progress depends on a branch-and-bound algorithm that checks every possible cases using case division recursively. You can think of this as something analogous to counting all possible N-Queen problem configurations with backtracking. Currently, the whole algorithm is written in C++, so I would like to formalize the claim that the algorithm indeed checks every case. So basically, I need to formalize the whole search tree.
It seems possible to export the whole search tree from the C++ program with more work, but I can't estimate how hard it is. It requires me to do multiple steps: i) correctly implement the C++ algorithm, ii) export the whole search tree with everything required for formalization, and iii) import the data in lean and make an actual formalized result.

Instead, I wondered if we could implement the tree search algorithm directly in Lean. In this way, all aforementioned steps will be in a single language with no translation cost. For an example with N-Queen, we could prove that we can divide the counting problem into cases where a cell is either filled or empty. Using the proof term for that theorem, I think we can even implement a backtracking function in Lean 3 that will provably count the number of N-Queen configurations, which is essentially a computable function that is provably equal to the number of N-Queen configs.
What worries me at this moment is the runtime of the algorithm. It's hard to estimate the compute overhead from translating C++ code to Lean, but the C++ version already runs for around a whole day (~20h). What I understand vaguely is that Lean 3 uses interpreter to #eval a term so it might be slow, but Lean 4 is designed to be a programming language so it compiles a term into program which runs faster. Still, for verification purpose I expect the whole tree has to be generated as a single term, so it might not be that Lean 4 provides dramatic performance boost.

With that, the questions I would like to ask are these:
i) Will such implementation of backtracking algorithm + its verification possible in theory? If so, what would be possible challenges of actual implementation?
ii) Assuming i), will Lean 4 help boost the runtime of the verified backtracking algorithm?

Thank you for reading so far! And if you could, it will be much appreciated to hear what you think. I feel that there could be more details I need to provide to answer these, so feel free to ask and I am willing to clarify.

[Johan Commelin]

@Jineon Baek Welcome! This certainly sounds like a job for Lean 4 and not Lean 3.

[Mario Carneiro]

1. Yes, it is possible to verify results like this, but it will be quite expensive. The flyspeck project, in HOL Light, is of a similar flavor, with a large computer search and a verified algorithm forming part of the proof.
2. Yes, if you want to run the algorithm itself in lean then lean 4 is likely to be an order of magnitude faster than lean 3. If you settle for proving the program correct, then you can do equally well in either lean 3 or lean 4. There will probably still be a performance loss going from the C++ code to Lean 4 code, but it's hard to estimate how much; lean 4 is fairly competitive with other compiled languages.

One thing that can significantly help with the runtime is to turn your P algorithm into an NP algorithm: that is, determine some certificate or sequence of guesses that will help your program run as fast as possible, and verify only the guesses, not the means by which you obtained the guesses.

[Mario Carneiro]

Still, for verification purpose I expect the whole tree has to be generated as a single term,

This is not the case. It is possible to split the proof into lemmas, corresponding to the subcases in your search tree. That way the terms to be manipulated all have similar size, although there may be many of them. How many leaves are there in the search tree?

[Jineon Baek]

@Mario Carneiro Thank you for your answers!

There are ~40000 leaves in the search tree. Each node represents a certain set of sofas. In the search algorithm, to split a node there is (i) a branching step where we divide the set into two disjoint unions, and (ii) a step to check that a matrix is positive definite, and (iii) a step where we run convex quadratic programming to estimate the upper bound of sofas for that node, which is used also to finish search early. I need to do some benchmarking to see which of (i) or (ii) + (iii) is the runtime bottleneck, but I feel that the latter might be the one.

Like you said, only a certificate is needed to verify (ii) and (iii), which can be generated outside the verifier, so I actually feel a bit hopeful that we don't need to comprise much of the runtime. The flyspeck project uses a lot of LP, so my guess is that they have similar situation. Meanwhile, is it possible for Lean to use external program to obtain such certificate, likely by some tactic? It seems that lean4 has FFI, but I wonder if the same thing can be done in lean3.

I also want to make the following clear. It seems that multiple cases are possible when we say that we verified an algorithm.
(i) The algorithm code in lean is verified, and it is compiled as executable and ran, with the output we intended for a proof.
(ii) The whole proof term is constructed from the search tree, no matter how it is split in small pieces or not. The proof term is then verifiable by external verifier.
I would prefer to have (ii), as for (i) we need to also trust the compiler and the whole proof term is not generated in Lean. Will it be that lean4 is also magnitude faster for doing (ii)?

[Mario Carneiro]

Meanwhile, is it possible for Lean to use external program to obtain such certificate, likely by some tactic? It seems that lean4 has FFI, but I wonder if the same thing can be done in lean3.

The obvious method is to write the certificate to a file and then read it in