Tree of GPTs

Stream: Machine Learning for Theorem Proving

[Hank]

Has anyone seen the Tree of Thoughts paper? The model proposed there connects many LLMs into a tree. To be more specific, each node of the tree is a LLM. It inputs a sentence representing the current thought/state and outputs several next steps. I feel that the model mimics how a human solves a LEAN goal very well: when we see the current goal state, we think of several sequences of proof steps to make progress instead of only one sequence of proof steps. It would be exciting to incorporate this model into LEAN. Even nicer -- I saw the implementation on GitHub and it was quite easy, < 400 lines of code I would say.

[Junyan Xu]

Where in the paper does it say each node is a LLM? I do see a recent paper utilizing different LLMs, but not this one. image.png

[Hank]

Each node uses OpenAI's GPT, more specifically the Chat Completions API.

[Hank]

I am thinking we can use ProofGPT as the nodes