Optimization for ML and AI Seminar: Self-play Algorithms for Math Theorem Proving

Tengyu Ma, Stanford University

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.

Tengyu Ma is an assistant professor of computer science at Stanford University. His research interests broadly include topics in machine learning, algorithms and their theory, such as deep learning, (deep) reinforcement learning, pre-training / foundation models, robustness, non-convex optimization, distributed optimization, and high-dimensional statistics.

Zoom: https://bit.ly/Opt-AI-ML