HyperTree Proof Search - Automated Theorem Proving with AlphaZero and Transformers!

Channel:
Singapore John Tan Chong Min
Subscribers:
5,330
Published on ● Video Link: https://www.youtube.com/watch?v=CIGl2NboS9s


Category:
Let's Play
Duration: 1:47:02
500 views
17

Ever wondered what it is like to use AlphaZero style techniques and Transformers to solve mathematical theorems? HyperTree Proof Search by Meta is here. This employs the Transformer architecture as the Policy and Value networks for AlphaZero, with the goal to be solved as the prompt. The policy network predicts the next action (tactic), and is able to output tactics of variable lengths. The value network predicts the probability of a given goal being solved, and is restricted to outputting "Provable" and "Unprovable" as a next token, akin to a classification problem, and the value is given by the probability it will output the "Provable" token!! These are all pretty interesting ideas to extend AlphaZero to a search problem with infinite number of actions.

Solving automated theorem proving might be a first step to helping to build architectures capable of reasoning and hence explainable neural networks. There is a use for such architectures, but the caveat is that it can be very compute intensive. No wonder evolution does not automatically endow us with a purely logical brain - it will be too energy intensive and time intensive to derive decisions for our survival.

Paper can be found at: https://arxiv.org/abs/2205.11491
Slides can be found at: https://github.com/tanchongmin/TensorFlow-Implementations/blob/main/Paper_Reviews/Hypertree%20Proof%20Search%20Slides.pdf

Video on AlphaGo / AlphaZero: https://www.youtube.com/watch?v=a4lrFMSwGWQ
Video on AlphaTensor: https://www.youtube.com/watch?v=6nYqyTzOQjw

0:00 Introduction and Motivation
4:53 Forwards and Backwards Proving Process
10:21 Key Insight of Theorem Proving
11:06 Sample Theorem in Lean
14:13 Lean Proof-tree
19:33 Lean Demo
26:55 Godel Incompleteness Theorem
28:30 Do humans think in logical statements?
33:05 AlphaZero Recap
43:44 HyperTree Proof Search Overall
58:23 HyperTree Proof Search Specifics
1:03:25 Policy and Value Networks (Transformers) Training
1:10:00 Difference from AlphaZero
1:12:28 Results on Lean
1:13:29 Discussion on HyperTree Proof Search Architecture
1:24:12 Discussion on logical thinking
1:42:48 Final words and how to train complex models efficiently
~~~~~~~~~~~~~~~~~~~~~~~~~~

AI and ML enthusiast. Likes to think about the essences behind breakthroughs of AI and explain it in a simple and relatable way. Also, I am an avid game creator.

Discord: https://discord.gg/fXCZCPYs
LinkedIn: https://www.linkedin.com/in/chong-min-tan-94652288/
Online AI blog: https://delvingintotech.wordpress.com/.
Twitter: https://twitter.com/johntanchongmin
Try out my games here: https://simmer.io/@chongmin



Other Videos By John Tan Chong Min


2023-04-02Is GPT4 capable of self-improving? Are we heading for AGI or AI doom?
2023-03-28How Visual ChatGPT works + Toolformer/Wolfram Alpha. LLMs with Tools/APIs/Plugins is the way ahead!
2023-03-21Tokenize any input, even continuous vectors! - Residual Vector Quantization - VALL-E (Part 2)
2023-03-07Using Transformers to mimic anyone's voice! - VALL-E (Part 1)
2023-02-28Learning Part-Whole Structure by Chunking - More Efficient than Deep Learning!!!
2023-02-21High-level planning with large language models - SayCan
2023-02-13Learning, Fast and Slow: Towards Fast and Adaptable Agents in Changing Environments
2023-02-07Using Logic Gates as Neurons - Deep Differentiable Logic Gate Networks!
2023-01-31Learn from External Memory, not just Weights: Large-Scale Retrieval for Reinforcement Learning
2023-01-17How ChatGPT works - From Transformers to Reinforcement Learning with Human Feedback (RLHF)
2023-01-09HyperTree Proof Search - Automated Theorem Proving with AlphaZero and Transformers!
2022-12-23CodinGame Fall Challenge 2022: A First Look (managed to get to Silver!)
2022-12-21Can ChatGPT solve CodinGame/Google Kickstart problems?
2022-12-19Reinforcement Learning Fast and Slow: Goal-Directed and Memory Retrieval Mechanism!
2022-12-12A New Framework of Memory for Learning (Part 1)
2022-11-14Hippocampal Replay for Learning (Full Length with Questions)
2022-11-14Hippocampal Replay for Learning (3 min summary)
2022-11-07AlphaTensor: Using Reinforcement Learning for Efficient Matrix Multiplication
2022-10-27Playing Go on TyGem and learning from AI (~ 3 kyu)
2022-10-13Heroes of Might and Magic III - Armageddon's Blade Campaign (First Playthrough) - Final!!!
2022-10-13Heroes of Might and Magic III - Armageddon's Blade Campaign (First Playthrough) - Part 6