How exactly does GPTF perform its search algorithm?

Stream: lean-gptf

[Daniel Donnelly]

I'm wondering how the search algorithm of GPTF actually works. See this #general post for more info: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/How.20does.20Lean's.20search.20of.20its.20library.20work.3F/near/254319211

[Jason Rute]

Gptf for lean (it’s a bit different in metamath gptf) doesn’t have an explicit search. Instead everything is done via sentence completion (aka next token prediction, aka autoregressive language modeling). If you haven’t already, I encourage you to watch this talk (https://m.youtube.com/watch?v=EXpmbAfBNnw). Specifically, I explain how this works in the next few slides after the demo. (I made a small mistake. I said we do breadth first search. We actually do best first search.). If that makes sense and the you want to learn how a transformer works, see the neural conjecturing topic in #Machine Learning for Theorem Proving for some good videos and tutorials.

[Jason Rute]

Also, if you want to know “exactly” there is always the paper: https://arxiv.org/pdf/2102.06203.pdf

[Jason Rute]

When I said we don’t have an explicit search, I mean we don’t have an explicit search that searches through the lean library. (To anthropomorphize, lean gptf memorizes all of mathlib.) So the lean-gptf tool doesn’t use any form of search it just “dreams” up a dozen or so next steps and filters out those that don’t immediately fail. Now, in the paper we also test whether lean gptf can find whole proofs. Finding a proof is a type of tree (or graph) search where the nodes are the tactic states and the edges are the tactics. As I said above, for that we use best first search.