“Self-play Algorithms for Math Theorem Proving with LLMs”
Speaker Bio
Professor Ma is an Assistant Professor of computer science at Stanford. 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.
Abstract
I will discuss some RL algorithms for automated theorem proving with LLMs, especially in the possible future regime where we ran 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 (which are often variants of known results) 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.