What should I read first if I want to verify algorithms?

Stream: new members

[Viliam Vadocz]

I just picked up Lean yesterday by going through the Number Game, and I am thinking about trying to formally verify properties of search algorithms such Monte-Carlo Tree Search (MCTS) with various modifications such as upper confidence bounds for trees (UCT) or terminal node solving.

• I don't know what has already been verified by the community and I would like to find out more.
• I also don't know how difficult something like this might be. I have an undergraduate CS background.
• What should I read first if my goal is to formally verify search algorithms? Theorem Proving in Lean 4 or Functional Programming in Lean?

[Yagub Aliyev]

Hi!

1) What has already been verified is in mathlib
https://github.com/leanprover-community/mathlib4
2) Examples of formally verified results published recently: https://www.tandfonline.com/toc/uexm20/31/2?nav=tocList
3) Are search algorithms theorems with proofs? If yes, then this can help: https://leanprover.github.io/theorem_proving_in_lean/
Otherwise this https://lean-lang.org/functional_programming_in_lean/

Good luck :fingers_crossed:

[Rémy Degenne]

We should now have most probability tools you need to analyse the UCT algorithm. However, what we have in this direction stops here: as far as I know nobody has done any regret bound proof for a RL or multi-armed bandit algorithm. There has been some work in Coq on RL methods: https://github.com/IBM/FormalML , but not in Lean.

I say that we have everything you'll need, but you'll want concentration inequalities like Azuma-Hoeffding if you follow the UCT paper proof and while we have everything we need to state it, it has not been done yet.
An interesting first step would be to prove a regret bound for the UCB bandit algorithm, since UCT is an adaptation of UCB to the more complex setting of tree search. I suggest you look at the Bandit Algorithms book by Tor Lattimore and Csaba Szepesvari for clean proofs (see https://tor-lattimore.com/ for a free pdf).

Overall, I'd say verifying properties of UCT is a feasible but not straightforward goal, and that might take some time.

[Viliam Vadocz]

Thanks for the helpful links, @Yagub Aliyev.

Also thanks for the suggestion of looking at UCB first, @Rémy Degenne. I have some additional questions:

• How much time would you estimate it would take me to learn Lean (and mathlib) to such a degree that I can verify regret bounds for UCB? You may assume a computer science undergraduate background with additional reading into type and category theories, experience with functional languages, and familiarity with the subject material in the context of RL.
• How long would it take to do the actual proof?
• Is translating an existing proof straightforward in your experience or do you tend to require new formalisms?