Zulip Chat Archive

Stream: Machine Learning for Theorem Proving

Topic: Tree of GPTs

Hank (Jun 03 2023 at 18:29):

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 (Jun 03 2023 at 23:14):

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 (Jun 04 2023 at 00:43):

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

Hank (Jun 04 2023 at 07:10):

I am thinking we can use ProofGPT as the nodes

Last updated: Dec 20 2023 at 11:08 UTC