Seminar Details
An Overview of "HyperTree Proof Search for Neural Theorem Proving"
- Start Date: March 1, 2023
- Event Start Time: 12:30 PM
- Event End Time: 2:00 PM
- Seminar Series: Rutgers LEAN (Mathematics) Seminar
- Presenter(s): Liam Schramm - Rutgers University
- Event Location: Hill Center, Room 005
- Event Additional Info: <p>A Zoom option to attend is available. Please contact one of the organizers for the link.</p>
- Presentation Type: Stand Alone Presentation
- Abstract:
HyperTree Proof Search (HTPS) is the current state-of-the-art algorithm for automated theorem proving in Lean. I will go over Monte Carlo Tree Search and AlphaGo, and show how HTPS applies these to the problem of proof search. Along the way we'll talk about why we probably need both machine learning and the theory of exploration in reinforcement learning for efficient automated theorem proving.