A Theoretical Framework for Self-Play Theorem Proving Algorithms
2026-06-01 • Machine Learning
Machine Learning
AI summaryⓘ
The authors study a way for computer programs to get better at proving math theorems by playing with themselves, using two roles: one that proves theorems and one that makes up new ones. They represent theorems as points in a network and show that if this network is well connected, the system can prove many more theorems quickly. They also notice that the 'theorem generator' can create overly complicated or unimportant theorems, so they suggest a way to make the set of generated theorems more varied and meaningful. Finally, they explain a way to measure how similar theorems are using a learning method that turns the theorems into points in space for easier comparison.
Self-playTheorem provingLarge Language ModelsGraph theoryReversible random walkConjecturerProverDiffusion similarityContrastive learningEmbedding
Authors
Thomas Chen, Zhiyuan Li
Abstract
Self-play, a type of training algorithm that enables a model to self-improve, has recently shown promising empirical results in the context of formal theorem proving using Large Language Models (LLMs). (Dong & Ma, 2025) instantiate self-play with two cooperating agents: a prover, which proves theorems, and a conjecturer, which generates new theorems as a curriculum to the prover. In this paper, we provide a theoretical framework for understanding the self-improvement capabilities of self-play algorithms for theorem proving. First, we formalize the set of theorems as a graph, with nodes as theorems and edges between pairs of theorems with similar semantics. We introduce a set of primitive assumptions that characterize the guarantees of a trained prover and how a conjecturer can access the structure of the graph. Second, we show that if the underlying graph of theorems is well-connected, then a prover-conjecturer system, where the conjecturing algorithm is based on a reversible random walk, is sufficient to grow the set of proved theorems exponentially. Third, motivated by an issue encountered empirically by self-play algorithms, where the conjecturer tends to generate artificially complex and non-fundamental theorems, we propose a diversity measure for a training distribution of theorems generated by a conjecturer and an improved conjecturing algorithm that locally maximizes this diversity measure, by computing the diffusion similarity between neighboring theorems in the theorem graph. Finally, we describe a method to compute the diffusion similarity by using contrastive learning to embed nodes into Euclidean space and then computing the inner-product between embeddings.