Professor Tengyu Ma (Stanford): Self-play Algorithms for Math Theorem Proving

Speaker: Professor Tengyu Ma (Stanford)

Title: Self-play Algorithms for Math Theorem Proving

Video: Click here to view

Abstract:  I will discuss RL algorithms for automated theorem proving with LLMs, especially in the possible future regime where we run out of high-quality training data. To keep improving the models with limited data, we draw inspiration from mathematicians, who continuously develop new results, partly by proposing novel conjectures or exercises and attempting to solve them. We design the Self-play Theorem Prover (STP) that simultaneously takes on two roles, conjecturer and prover, each providing training signals to the other.  At the end of the talk, I will mention a recent paper on extending the algorithm to include another role, Guide, which helps guide the conjecturer to generate clean and relevant conjectures, and a few other related works in using AI for math. 

Bio: Tengyu Ma is an assistant professor of Computer Science at Stanford University and the Chief AI Scientist at MongoDB. He received his Ph.D. from Princeton University. His research interests include topics in machine learning, algorithms, and their theory, such as deep learning, (deep) reinforcement learning, pre-training / foundation models, robustness, and non-convex optimization. He is a recipient of the ACM Doctoral Dissertation Award Honorable Mention, the Sloan Fellowship, and the NSF CAREER Award. He is a co-founder and was the CEO of Voyage AI until it was acquired by MongoDB in February 2025.