1 Introduction↩︎

Formal theorem proving and mathematical reasoning with Large Language Models (LLMs) have made rapid progress, including systems that reached IMO gold-medal-level performance and systems reported to assist with open mathematical research problems [2], [3]. Among the technical ideas used to train LLM-based theorem provers, self-play via two cooperating models, a prover model and a conjecturer model, is a new and promising training technique.

Self-play can be viewed as an automated synthetic data generation mechanism, where a system of two models generate and solve gradually-more-difficult instances of a task, improving both models with no manually annotated data required. Self-play has been used to train models to play Go [4]. In the context of theorem proving, self-play algorithms have been studied empirically. STP [1] trains two models: a prover, which maps theorem statements to their proofs, and a conjecturer, which maps theorem statements to slightly more difficult theorem statements adaptively based on the prover. The prover and conjecturer models cooperate to gradually enable the prover to prove harder theorems.

To our knowledge, this is the first theoretical analysis of self-play training algorithms for formal theorem proving. In this work, we introduce a theoretical framework, based on a graph of theorems, where the primary objective is to design a training algorithm that yields a prover with a large knowledge set—the set of theorems it can prove (4). The framework introduces a set of primitive assumptions, characterizing how a prover can generalize in-domain when trained on a distribution of theorems and how a conjecturer can access the structure of the theorem graph. The space of training algorithms includes prover-conjecturer systems analogous to that in STP [1], where the conjecturer generates a sequence of distributions over theorems, which the prover is trained on to gradually increase its knowledge. Under a connectivity condition on the underlying theorem graph, we show that the prover-conjecturer system in 2, using a simple baseline conjecturing algorithm based on a reversible random walk, guarantees that the size of the prover’s knowledge set at iteration \(t \in \mathbb{N}\) grows exponentially in \(t\) ([thm:main]).

However, the size of the prover’s knowledge set alone is insufficient as an objective since the knowledge set can contain many related, non-fundamental theorems (e.g. increasingly complex arithmetic problems). Empirically, STP [1] use heuristic elegancy filters to filter out inelegant, artificially-complicated generated-conjectures. Minimo [5] also encounters an issue where the conjecturer generates longer and more complicated conjectures rather than deeper conjectures. The question we focus on is how to encourage the conjecturer to generate theorems whose fundamental proof ideas are more diverse, which we believe is related to the issues encountered empirically.

Towards quantifying diversity of a prover’s knowledge set and proposing algorithmic improvements to the conjecturer, the secondary objective of a training algorithm within our framework is: given a hyperparameter \(\tau \in \mathbb{N}\), maximize the size of the \(\tau\)-step expansion of the prover’s knowledge set in the theorem graph, a quantity we identify with the diversity of the prover’s knowledge. This prover-centric diversity is of practical use itself because it is heuristically the number of theorems with a \(\tau\)-step reduction to a theorem the prover knows how to prove, which the prover can prove at inference time given \(\tau\) steps of “reasoning." This prover-centric diversity can also be thought of as quantifying the size of the boundary of the prover’s knowledge set. Towards maximizing this prover-centric diversity, we propose a diversity measure for the training distribution of theorems generated by a conjecturer (which the prover is trained on) and show it lower bounds the prover-centric diversity ([lem:divt-kct-connection]). We propose an improved conjecturing algorithm (5) that generates training distributions that locally maximize this diversity measure, which requires computing a quantity called the diffusion similarity. Finally, we propose a new way to compute the diffusion similarity via contrastive learning ([thm:contembd]).

1.1 Technical Overview↩︎

1.1.0.1 Theorem Graph.

Let \(V \subset \{ 0,1\}^*\) be the set of all theorems, encoded as strings according to a formal language like Lean [6]. Let \(\mathcal{F}_{\mathrm{prover}}\) be the hypothesis class of prover models (e.g. the class of pre-trained LLMs), where every prover \(\mathcal{F}_{\mathrm{prover}}\ni f : V \to \Delta(\{ 0,1\}^*)\) maps a theorem to a distribution over proofs. A verifier \(\mathrm{Ver}: V \times \{ 0,1\}^* \to \{ 0,1\}\) verifies if a proof of a theorem is correct. Using \(\mathrm{Ver}\), for any prover \(f \in \mathcal{F}_{\mathrm{prover}}\) and theorem \(x \in V\) define the success rate \(\operatorname{succ}(x,f) \in [0,1]\) as the probability that \(f\) on input \(x\) generates a correct proof of \(x\). For any \(\varepsilon \in (0,1)\), define \(E(\varepsilon, \mathcal{F}_{\mathrm{prover}}) \subset V \times V\) as the set of pairs of theorems that are semantically similar, with respect to \(\mathcal{F}_{\mathrm{prover}}\):

\[\begin{align} E(\varepsilon, \mathcal{F}_{\mathrm{prover}}) := \{ (x,y) \in V \times V : \forall f \in \mathcal{F}_{\mathrm{prover}}, |\operatorname{succ}(x,f) - \operatorname{succ}(y,f)| \leq \varepsilon\}\label{eq:edge-ood} \end{align}\tag{1}\]

Fix \(\varepsilon\) and let \(E \subset E(\varepsilon,\mathcal{F}_{\mathrm{prover}})\). 3 and 4 of our framework require that for any theorem \(x\), the set \(N(x) := \{ y \in V : (x,y) \in E\}\) is efficiently computable. The neighbor oracle \(N : V \to 2^V\), mapping \(x \rightarrow N(x)\) is a key algorithmic primitive for the conjecturing algorithms we propose later. The theorem graph is the undirected graph \(G = (V,E)\) with nodes \(V\) and edges \(E\).

1.1.0.2 Further Assumptions.

We define a conjecturer as a mapping from a distribution \(D \in \Delta(V)\) of theorems (represented as a vector in \([0,1]^{|V|}\)) to a new distribution \(D' \in \Delta(V)\) of theorems. One type of conjecturer is a single step of a random walk with transition matrix \(P \in [0,1]^{|V| \times |V|}\), where \((D')^\top = D^\top P \in [0,1]^{1 \times |V|}\). Our first result assumes that \(|V| = \infty\) and that the random-walk-based conjecturer \(P\) satisfies a connectivity condition, 5. When \(P = P_{\mathrm{s.r.w.}}\) is a simple random walk, where a node transitions uniformly to its neighbors, then 5 amounts to a property of \(G\): that there exists \(\kappa > 0\) where for any finite subset of nodes \(A \subset V\) then \(\kappa \cdot |\partial A| \geq \deg(A)\) where \(|\partial A|\) are the number of edges with one endpoint in \(A\) and the other in \(V - A\), and \(\deg(A)\) is the sum of the degrees of nodes in \(A\). Finally, our framework includes 1 and 2, which are statistical-learning-like assumptions which describe how a prover trained on a finite sample of i.i.d. (theorem, proof) pairs from some training distribution \(D\) can generalize in-domain to \(D\).

1.1.0.3 A Baseline Conjecturing Algorithm.

First we show if the theorem graph \(G\) satisfies a connectivity assumption, 5, then a conjecturer, based on a nearest-neighbor-type reversible random walk, enables the prover to prove an exponential in \(t\) number of theorems at every iteration \(t \in \mathbb{N}\).

1.1.0.4 An Improved Conjecturing Algorithm for the Diversity Issue.

Suppose \(f \in \mathcal{F}_{\mathrm{prover}}\) is the final prover trained by a self-play algorithm like 2. Whereas [thm:main], under 5, provides guarantees of \(|K^p(f)| := |\{ x \in V : \operatorname{succ}(x,f) \geq p\}|\), the size of the prover’s knowledge, [thm:main] does not guarantee the diversity of the prover’s knowledge. For hyperparameter \(\tau \in \mathbb{N}\), we study how to optimize a proxy for diversity of the prover’s knowledge, \(|K^p_\tau(f)| := | \{ x' \in V : \exists x \in V : \operatorname{succ}(x,f) \geq p \mathrm{ and } \mathrm{dist}(x,x') \leq \tau\}|\). 1 depicts two provers, \(f_1\) and \(f_2\), that both can prove the same number of theorems (\(|K^p(f_1)| = |K^p(f_2)|\)), but where \(f_1\)’s knowledge set is much less diverse, in the sense that \(|K^p_\tau(f_1)| \ll |K^p_\tau(f_2)|\).

Suppose prover \(f\) is trained on theorem distribution \(D \in \Delta(V)\) in the sense that \(\mathbb{P}_{x \sim D}[\operatorname{succ}(x,f) \geq p] \geq 1 - \epsilon\) (as in 2). [lem:divt-kct-connection] shows that in order to maximize \(|K^p_\tau(f)|\), it is reasonable to maximize the following property of \(f\)’s training distribution: \(\mathrm{Div}^P_\tau(D) := \frac{1}{||D^\top P^\tau||^2_{\ell^2(1/\pi)}} = \frac{1}{\sum_{x \in V }(D^\top P^\tau e_x)^2 \frac{1}{\pi(x)} }\), where \(P\) is the transition matrix of a reversible, nearest-neighbor Markov chain. With this observation, the goal is to design a conjecturing algorithm that generates training distributions \(\{ D_t\}_{t \in \mathbb{N}}\) where \(\mathrm{Div}^P_\tau(D_t)\) is large for each \(t \in \mathbb{N}\). We propose 5, an improved conjecturer that defines a push-forward map \(C : V \to \Delta(V)\) where \(\forall x \in V\), \(C(x) \in \Delta(N(x))\). The weighting of \(C(x)\) is determined by maximizing \(\mathrm{Div}^P_\tau(C(x))\).

\[\begin{align} \forall x \in V, \, C(x) &\leftarrow \arg\max_{\mu \in \Delta(N(x))} \mathrm{Div}^P_\tau(\mu) = \arg\min_{\mu \in \Delta(N(x))} \mu^\top P^\tau \mathrm{diag}(1/\pi) (P^\tau)^\top \mu \end{align}\]

5 needs to compute the diffusion similarity \(\phi^{\mathrm{diff}}_\tau(y, y') := e_y^\top P^\tau \mathrm{diag}(1/\pi) (P^\tau)^\top e_{y'}\) for every pair of neighbors \(y,y' \in N(x)\) of \(x\). ¹ We show the diffusion similarity can be computed by embedding each node in \(G\) into Euclidean space via an embedding model learned with contrastive learning, and then computing the inner product between embeddings. This can be used as a subroutine in a conjecturing algorithm like 5.

Under additional assumptions, we prove [thm:e2e-contrastive-learning-result], which is an extension to the result of [thm:contembd] that applies for classes of embedding models \(\mathcal{F}_{\mathrm{emb}}\) where models \(\mathcal{F}_{\mathrm{emb}}\ni h_\theta : V \to \mathbb{R}^k\) have small embedding dimension \(k \ll |V|\). [thm:e2e-contrastive-learning-result] provides approximation-guarantees for an embedding model that is learned via empirical risk minimization (ERM).

In short, our contributions are:

1. We provide a theoretical framework for understanding and designing self-play theorem proving algorithms. The framework formalizes the set of theorems as a graph, where nodes are theorems. It introduces a set of primitive assumptions (1 – 4) that describe the properties of the graph and the computational primitives available to a self-play algorithm.

2. We show in [thm:main] that if the theorem graph and conjecturer satisfy a well-connectedness property (5), the number of theorems the prover-conjecturer system (2) proves grows exponentially with the number of self-play iterations.

3. Motivated by an issue encountered empirically by self-play algorithms where the conjecturer generates artificially complex and non-fundamental theorems, we propose a diversity measure for a training distribution of theorems generated by a conjecturer ([defn:diversity-measure]) and an improved conjecturer (5) that locally maximizes this diversity measure, by computing the diffusion similarity (3) between neighboring theorems in the theorem graph.

4. In [thm:contembd] and [thm:e2e-contrastive-learning-result], we describe a method to compute the diffusion similarity of two nodes of the theorem graph by using contrastive learning to embed nodes into Euclidean space and then computing the inner-product between the embeddings.

2 Related Work↩︎

2.0.0.1 LLM-Based Formal Theorem Proving Systems.

Formal theorem proving with LLMs in Lean [6] is commonly divided into two paradigms: step-level interaction and whole-proof generation. Step-level methods interact with Lean incrementally, proposing one tactic at a time [8]–[12]. Whole-proof methods instead generate a complete Lean proof in a single interaction [13]–[21].

2.0.0.2 Self-play for Formal Theorem Proving.

Regarding self-play theorem proving systems, STP instantiates a prover-conjecturer self-play loop from pre-trained LLMs, where the conjecturer is trained to generate synthetic theorems that are barely provable by the current prover [1]. Minimo instantiates a prover-conjecturer self-play loop to learn a prover from scratch, where the conjecturer generates conjectures via constrained decoding and the prover guides an MCTS proof search [5]. In contrast to these empirical works, our work develops a theoretical framework for analyzing when prover-conjecturer self-play can expand the set of provable theorems.

2.0.0.3 Theoretical Analyses of Self-play Algorithms.

Existing theoretical analyses of self-play largely focus on adversarial settings, such as zero-sum Markov games. The theorem-proving setting we study is different: the prover and conjecturer have asymmetric but cooperative roles. [22] provide a theoretical analysis of self-play algorithms in zero-sum Markov Games, showing convergence to a Nash Equilibrium [22]. The Wasserstein GAN training algorithm [23] is a theoretically-grounded asymmetric self-play algorithm, but still where the agents are adversarial to each other. Our work also differs from works that study how to learn a model to verify theorems in a purely statistical setting [24]. Our setting is non-statistical since the goal of the training algorithm is to allow the final model to generalize beyond its starting distribution, not just to generalize well on its starting distribution given i.i.d. samples. However, we will assume some statistical-learning primitives (2) in our framework.

2.0.0.4 Theorem Graphs.

Prior works formalize the graph or hyper-graph structure of mathematical theorems [25], [26]. In [25], each node represents a statement; the statement corresponding to a node can be deduced in one step via a deduction rule from the statements corresponding to its descendants. [26] formalizes nodes as statements, and each \((p,q)\) hyper-edge corresponds to applying a deduction rule on \(p\) input statements to yield \(q\) output conclusions. Axioms of the logical system are root nodes. In relation to these works, our notion of a theorem graph still represents mathematical statements as nodes. However, the definition of an edge is not defined in terms of deduction rules in a particular logical system. Rather, edges are determined by the class of prover models \(\mathcal{F}_{\mathrm{prover}}\), where an edge between two theorems \((x,y)\) indicates that for every prover \(f \in \mathcal{F}_{\mathrm{prover}}\), the success rate of \(f\) on theorem \(x\) is not too different from the success rate of \(f\) on theorem \(y\).

2.0.0.5 Graph Exploration Algorithms, Graph Diffusion, Contrastive Learning.

Given a graph, the question of how to design an algorithm to explore the graph efficiently has been studied in [27]. They formalize chain-of-thought reasoning as a random walk over a graph of ideas, where the goal of the reasoner is to hit a particular node of the graph, starting at a designated start node. The underlying graphs they study are metastable graphs [28]. The question we study in 5 is conceptually related to [27], in that we want to find a graph algorithm that can efficiently explore a graph with poor connectivity, such as metastable graphs. However, our proposed graph-exploration algorithms are different from [27]. In particular, our algorithm uses a similarity measure between nodes in the graph, called the diffusion similarity, that is defined in terms of a random walk on the graph. The diffusion similarity measure is closely related to the diffusion distance, a graph metric which is useful for characterizing the clustering-structure of a graph [29]. Finally, we propose a new way to compute the diffusion similarity, using a version of contrastive learning formalized by [30], who provide a theoretical characterization of the global minimizers of a particular contrastive loss in terms of the minimizers of a related matrix factorization objective.

3 Preliminaries↩︎

3.0.0.1 Notation.

\(0 \in \mathbb{N}\). \([n] := \{ 1, 2, \ldots, n\}\). For a set \(V\), \(2^V\) is its power set. For \(v \in \mathbb{R}^n\), \(\mathrm{diag}(v) \in \mathbb{R}^{n \times n}\) is the diagonal matrix with \(v\) on its diagonal. For \(M \in \mathbb{R}^{n \times n}\), \(i,j \in [n]\), denote \(M[i,j]\) the \((i,j)\)th entry, \(M[i]\) the \(i\)th row, and \(M[:, j]\) the \(j\)th column of \(M\). \(O^{k \times k}\) is the set of \((k\times k)\) orthogonal matrices. \(\mathbf{1}\) is the all-\(1\)’s vector. \(\forall x \in V\), \(e_x \in \mathbb{R}^{|V|}\) is the unit vector along dimension indexed by \(x \in V\). For an undirected, unweighted graph \(G = (V,E)\), for any \(x,y \in V\),   \(\mathrm{dist}(x,y)\) is the minimum number of edges of any path connecting \(x\) and \(y\) in \(G\). \(\deg(x)\) denotes the degree of node \(x \in V\). For \(x \in V, r \in \mathbb{N}\), denote \(B(x,r) := \{ x' \in V : \mathrm{dist}(x, x') \leq r\}\) and \(\partial B(x,r) := B(x,r) - B(x, r - 1), \, B(x, -1) := \emptyset\). For set \(S \subset V,\) let \(B(S, r) := \bigcup_{v \in S} B(v,r)\). For \(\pi,f, f' : V \to (0, \infty)\), let \(\langle f, f' \rangle_{\ell^2(1/\pi)} := \sum_{x \in V} f(x) f'(x) \frac{1}{\pi(x)}\) and \(||f||^2_{\ell^2(1/\pi)} := \langle f, f \rangle_{\ell^2(1/\pi)}\). Let \(\Delta(V)\) denote the set of probability distributions whose support is contained in the set \(V\). For \(D \in \Delta(V)\), \(\operatorname{supp}(D)\) is its support. For \(g : V \to \Delta(V)\), \(g \# D \in \Delta(V)\) is the distribution of \(y\), drawn according to this process: \(x \sim D, y \sim g(x)\). We say an algorithm has independent and identically distributed (i.i.d.) sample access to \(D\) if it has an oracle which it can query for i.i.d. samples \(x \sim D\).

3.0.0.2 Markov Chains on Graphs and Isoperimetric Inequality.

7.1 has more-detailed preliminaries. Let \(G = (V,E)\) be an undirected, connected graph with a countable set of vertices. Let \((V,P)\) denote an irreducible, reversible Markov chain with transition matrix \(P \in [0,1]^{|V| \times |V|}\) and invariant measure \(\pi : V \to (0,\infty)\) where reversibility means that \(\forall x,y \in V, \pi(x) P[x,y] = \pi(y) P[y, x]\). Let \(E(P)\) be the set of unordered tuples \((x,y)\) where \(P[x,y] > 0\). Given \(e \in E(P)\) we will write \(e = (e^-, e^+)\), but the choice of which end-point is \(e^-\) and which is \(e^+\) does not matter for our analysis. If \(E(P) \subset E\), then \((V,P)\) is nearest-neighbor-type random walk (Markov chain). The simple random walk \(P_{\mathrm{s.r.w.}}\) is a Markov chain where every node \(x\) transitions uniformly to its neighbors \(N(x)\). For any \(A \subset V\), let \(\partial A\) be the set of all edges in \(E(P)\) with one endpoint in \(A\) and the other in \(V - A\). Let \(\pi(A) := \sum_{x \in A} \pi(x)\) and \(a(\partial A) := \sum_{(e^-, e^+) \in \partial A} \pi(e^-) P[e^-, e^+] = \sum_{e^- \in A, e^+ \notin A} \pi(e^-) P[e^-, e^+]\).

3.0.0.3 Contrastive Learning.

8 contains more detailed preliminaries. Contrastive learning defines an algorithm for learning an embedding model that maps elements from a domain \(V\) (e.g. the set of real-world images) into Euclidean space \(\mathbb{R}^k\) for some \(k \in \mathbb{N}\). It is most notably used for training neural networks as embedding models [31]–[33]. We will use the setup of [30], which we describe below.

Let \(\mathcal{F}_{V}^{(k)}\) denote the class of all functions mapping \(V\) to \(\mathbb{R}^{k}\). Let \(\mathcal{F}_{\mathrm{emb}}\subset \mathcal{F}_{V}^{(k)}\) denote the hypothesis class of models \(h_\theta : V \to \mathbb{R}^k\) which we assume contains the ground-truth embedding model of the learning task. Contrastive learning defines two distributions of pairs of elements in \(V\): a positive pair distribution \(D_+ \in \Delta(V \times V)\) and a negative pair distribution \(D_- \in \Delta(V \times V)\). Given i.i.d. samples from both distributions, the trained model is encouraged to embed two elements sampled from a positive pair \((x,y) \sim D_+\) close together in Euclidean space, while embedding two elements sampled from a negative pair \((x,x') \sim D_-\) far apart in Euclidean space. These two distributions of pairs of elements are used to define a contrastive loss, and training the model amounts to minimizing an empirical estimate of the contrastive loss from finite samples.

Let the domain \(V\) consist of \(N \in \mathbb{N}\) elements, where \(N\) is large but finite. We will identify \(V\) with \([N]\) here for simplicity. Define \(\mu \in \Delta([N])\) as the base distribution and \(Q \in \mathbb{R}^{N \times N}\) as an augmentation scheme. Overloading notation, we can alternatively view \(Q : [N] \to \Delta(N)\) as a mapping from an element \(x\) to a distribution \(Q(x)\) over augmentations of \(x\). For every \(x \in [N]\), \(Q(x)\), equals the \(x\)-th row of the matrix-representation of \(Q\). For \(h_\theta : V \to \mathbb{R}^k\), define the population contrastive loss \(\mathcal{L}_{\mathrm{cont}}: \mathcal{F}_{V}^{(k)} \to \mathbb{R}\) as

\[\begin{align} \mathcal{L}_{\mathrm{cont}}(h_\theta) := \mathbb{E}_{(x, x^-) \sim D_-} (h_\theta(x)^\top h_\theta(x^-))^2 - 2 \cdot \mathbb{E}_{(x, x^+)\sim D_+}h_\theta(x)^\top h_\theta(x^+)\label{eq:pop-cont-loss} \end{align}\tag{2}\]

Positive pairs \((x, x^+)\sim D_+\) are sampled by first sampling an element from the base distribution, \(z \sim \mu\) and then sampling the pair elements as independent augmentations \(x \sim Q(z)\), \(x^+\sim Q(z)\), returning \((x,x^+)\). Negative pairs \((x,x^-) \sim D_-\) are sampled by first sampling \(z, z^- \sim \mu\) independently and then sampling \(x \sim Q(z), x^- \sim Q(z^-)\), returning \((x,x^-)\).

For a dataset \(\{ \overline{x}_i\}_{i \in [n]} \subset V\), define the empirical contrastive loss \(\hat{\mathcal{L}}_{\mathrm{cont}, n}: \mathcal{F}_{V}^{(k)} \to \mathbb{R}\) as:

\[\begin{align} &\hat{\mathcal{L}}_{\mathrm{cont}, n}(h_{\theta'}) :=\\ &-\frac{2}{n} \sum_{i \in [n]} \mathbb{E}_{\substack{x \sim Q(\cdot | \overline{x}_i),\\ x^+ \sim Q(\cdot | \overline{x}_i)}} (h_{\theta'}(x)^\top h_{\theta'}(x^+)) + \frac{1}{n(n - 1)} \sum_{i,j \in [n], i \neq j}\mathbb{E}_{\substack{x \sim Q(\cdot | \overline{x}_i),\\ x^- \sim Q(\cdot | \overline{x}_j)}} (h_{\theta'}(x)^\top h_{\theta'}(x^-))^2\label{eq:emp-cont-loss-defn} \end{align}\tag{3}\]

Claim D.2 of [30] shows that \(\mathbb{E}_{\{ \overline{x}_i\}_{i \in [n]} \sim \mu} \hat{\mathcal{L}}_{\mathrm{cont}, n}(h_{\theta}) = \mathcal{L}_{\mathrm{cont}}(h_\theta)\), i.e. that \(\hat{\mathcal{L}}_{\mathrm{cont}, n}\) is unbiased. Define the empirical risk minimizer (ERM) as follows.

8 in 8 is an algorithm that learns an embedding model using empirical risk minimization, given i.i.d. sample access to base distribution \(D \in \Delta(V)\) and augmentation function \(Q : V \to \Delta(V)\). To quantify the statistical generalization properties of the ERM, we introduce the following notion of Rademacher complexity.

4 Framework and Random-Exploration Baseline↩︎

4.1 Primitive Assumptions↩︎

With \(t \in \mathbb{N}\) denoting the iteration index, the primary goal of the training algorithm is to produce a prover \(f\) which can prove as many theorems as possible. One way a training algorithm can achieve this is by producing a sequence of provers \(\{ f_t\}_{t \in \mathbb{N}}\) where the prover \(f_{t + 1}\) can prove more theorems than prover \(f_t\) for every \(t \in \mathbb{N}\). The following assumptions define a set of core primitives for designing such a training algorithm.

1 assumes i.i.d. sample access to an initial training distribution \(D_0\) of theorems where for every theorem \(x\) in the support of \(D_0\), the proof of \(x\) is known. This means that we have efficient access to a proof of \(x\), either because it is recorded explicitly in some database of (theorem, proof) pairs, or because we have access to a prover \(f\) where \(\operatorname{succ}(x,f) \geq \Omega(1)\). The latter condition means that given \(x\) and \(f\), the proof of \(x\) can be efficiently sampled in \(O(1)\) calls to \(f\), with high probability.

An example of \(D_0\) would be a distribution of elementary-school-level math problems.

2 describes the ability of a model, trained on a distribution \(D\) of theorems via i.i.d. samples, to generalize in-domain to \(D\). We justify it with statistical learning theory in 10.

The requirement of 2 that the proof of every theorem in \(\operatorname{supp}(D)\) is known can also be thought of as requiring a training distribution of (theorem, proof) pairs, where every theorem in the support of the training distribution must have a correct proof associated with it. This requirement is necessary, as otherwise it would be possible to train a model to have high success rate on arbitrarily hard theorems for which we do not know the proof.

Let \(G = (V,E)\) be the theorem graph. 3 says that the edge set \(E\) is where the success rate of any prover in \(\mathcal{F}_{\mathrm{prover}}\) is not too different between two theorems connected by an edge.

In 4, we assume access to a neighbor oracle \(N\) as a primitive.

Assumptions 2 – 4 enable a training algorithm to run the following at each iteration. First, expand the current set of known theorems by one step via the neighbor oracle \(N\) (4). Second, 3 ensures that unseen theorems have success rate at least \(p/2\) under the current prover, enabling the proofs of the unseen theorems to be efficiently sampled. In general, note that if we have access to a prover \(f\) whose success rate on theorem \(x\) is reasonably high (\(\geq p/2\), where \(p \geq \Omega(1)\) by 2), then the proof of \(x\) can be efficiently sampled and become known. Finally, a new prover is trained on the expanded set of theorems via 2. 3 is necessary to our analysis because standard statistical learning theory arguments rely on exchangeability between training and test distributions and therefore do not by themselves justify this out-of-distribution step.

We do not require the edge set \(E\) to have an interpretable definition. We only require \(E\) to satisfy 3 and 4. One example instantiation of the theorem graph is where \(V\) is the set of theorems corresponding to discrete logarithm instances in a fixed cyclic group. Fix a cyclic group \(\mathbb{G}\) of prime order \(q\) with generator \(g \in \mathbb{G}\). For each \(a\in \mathbb{Z}_q\), let \(h_a=g^a\), and let \(x_a\in V\) denote the theorem: \[\text{``Given cyclic group \mathbb{G} of prime order q, and given g, g^{-1}, h_a \in \mathbb{G},\text{ there exists } z\in \mathbb{Z}_q \text{ such that } g^z=h_a.''}\] The proof of \(x_a\) is the unique exponent \(f_*(x_a)=a\). Define the edge set \(E\) by \((x_a,x_b)\in E \iff b-a\in\{-1,+1\}\pmod q .\) Thus, the theorem graph is a cycle over the discrete logarithm instances. This edge set satisfies 4, since given the theorem \(x_a=(\mathbb{G},g, g^{-1},h_a)\), the neighbor oracle can compute \(N(x_a)=\{x_{a+1},x_{a-1}\}\), where \(x_{a+1}\) has target \(h_a g=g^{a+1}\), and \(x_{a-1}\) has target \(h_a g^{-1}=g^{a-1}\). Finally, 3 amounts to the property that adjacent discrete-log instances have similar success rates for the prover class: \((x_a,x_{a + 1})\in E \implies \forall f\in\mathcal{F}_{\mathrm{prover}}, |\operatorname{succ}(x_a,f)-\operatorname{succ}(x_{a + 1},f)|\leq \frac{p}{2} .\) This property is conceivable for some prover classes since \(x_a\) and \(x_{a+1}\) are not substantially different: given \(g\) and its inverse \(g^{-1}\), an instance with target \(h_{a+1}\) can be reduced to the adjacent instance with target \(h_a\) by multiplying by \(g^{-1}\), i.e. \(h_{a+1}g^{-1}=g^{a+1}g^{-1}=g^a=h_a.\) Thus, any prover that can prove \(h_a\) can prove \(h_{a+1}\) by first reducing \(h_{a+1}\) to \(h_a\), running the original prover, and then adding \(1\) to the resulting exponent. For model classes \(\mathcal{F}_{\mathrm{prover}}\) that can exploit such reductions, it is conceivable that neighboring instances \(x_a\) and \(x_{a\pm 1}\) have similar success rates.

4.2 Random-Walk Conjecturing Algorithm↩︎

4.2.0.1 Conjecturer.

In STP [1], the conjecturer is a mapping that takes as input a theorem \(x\), its proof \(f_*(x)\), a lemma \(l\) used in \(f_*(x)\), and a system prompt; it returns a theorem \(c\) related to \(x\). We study a simplification where the conjecturer maps a theorem to a distribution of theorems.

For instance, when \(\forall x \in V, z \in N(x), w(x,z) = 1\) and for \(z \notin N(x), w(x,z) = 0\), then \(C_w(x) = \mathrm{Unif}(N(x))\), so that \((C_w, P_w, w)\) defines a simple random walk over \(G\), with \(\pi_w(x) \propto \deg(x)\).

4.2.0.2 Prover-Conjecturer System.

This section provides sufficient conditions for a prover-conjecturer system (2) to learn to prove more theorems across iterations. [thm:main] assumes the conjecturer \((C_w, P_w, w)\), defining Markov chain \((V, P_w)\), satisfies a connectivity assumption.

At iteration \(t\in \mathbb{N}\), the prover-conjecturer system (2), initialized with conjecturer \((C_w, P_w, w)\), has i.i.d. sample access to \(D_t \in \Delta(V)\), a training distribution over theorems whose proofs are known. It trains prover \(f_t \in \mathcal{F}_{\mathrm{prover}}\) on \(D_t\) via 2. Finally, it constructs i.i.d. sample access to a new distribution over theorems, \(D_{t + 1} \in \Delta(V)\) using 3. Given \(D_t\), 3 applies the conjecturer \(C_w\) to \(D_t\), yielding \(C_w \# D_t\). Theorems with low pass rate under \(f_t\) are filtered out, yielding \(D_{t + 1}\).

2 uses 3 as a subroutine to construct \(D_{t + 1}\) from \(D_t\). 4 is a practical approximation to 3, and it can be substituted in for 3 in 2. In 4, for a sufficiently large rollout-budget \(m \geq \Theta(\frac{1}{p^2}\log\frac{1}{\delta_{\mathrm{samp}}})\), by standard concentration inequalities [34], [35], we have that \(\forall x \in V\), with probability at least \(1 - \delta_{\mathrm{samp}}\), \(|\frac{1}{m} \sum_{i \in [m]} \mathbf{1}[\mathrm{Ver}(x, \pi_i) = 1] - \operatorname{succ}(x,f) | < p/2\). Thus, with high probability, if \(\operatorname{succ}(x,f) \geq p/2\), then \(\frac{1}{m} \sum_{i \in [m]} \mathbf{1}[\mathrm{Ver}(x, \pi_i) = 1] > 0\), so that at least one empirically-sampled proof \(\pi\) of theorem \(x\) is correct.

Due to the push-forward construction of \(D_{t + 1}\) from \(D_t\) in 2 for every \(t \in \mathbb{N}\), sampling from \(D_t\) requires first sampling \(x_0 \sim D_0\), then applying \(t\) push-forward transformations to yield \(x_i \sim D_j\), for all \(j \in [t]\). In particular, first draw a large number \(N_0\) of i.i.d. samples \(x_0^{(i)} \sim D_0\), \(i \in [N_0]\). At every iteration \(j \in \{ 0\} \cup [t]\), suppose inductively that there are \(N_j\) remaining unused i.i.d. samples from \(D_j\). Use \(\Theta(\frac{\mathcal{C}(\mathcal{F}_{\mathrm{prover}})\log \frac{1}{\delta}}{\epsilon^2 (1 - p)^2})\) of the \(N_j\) samples to train prover \(f_j\) via 2. Of the unused samples, apply the conjecturer to map \(x_j^{(i)}\) to \(y_j^{(i)} \sim C_w(x_j^{(i)})\). Discard \(y_j^{(i)}\) if \(\operatorname{succ}(y_j^{(i)}, f_j) < p/2\), else let \(x_{j + 1}^{(i)} := y_j^{(i)}\). Let \(N_{j + 1}\) denote the number of remaining samples. Note that if prover \(f_j\) is successfully trained according to 2 to where \(\mathbb{P}_{x \sim D_j}[\operatorname{succ}(x,f_j) \geq p] \geq 1 - \epsilon\), then by 3, \(\mathbb{P}_{x \sim D_j, x' \sim C_w(x)}[\operatorname{succ}(x',f_j) \geq p/2] \geq 1 - \epsilon\), so that by standard concentration inequalities, \(N_{j + 1} \gtrapprox (1 - \epsilon)N_j\). In the worst case, we have that \(\forall j \in [t], N_j \approx N_0 (1 - \epsilon)^j\), so that the number of oracle calls to \(D_0\) required to sample from \(D_j\) grows as \((\frac{1}{1 - \epsilon})^j\).

4.3 Expansion Guarantee for 2.↩︎

[thm:main] shows that on an infinite graph, with a reversible conjecturer (1) that induces a random walk that satisfies the Strong Isoperimetric Inequality (5), and for training error threshold \(\epsilon< \frac{1}{2\kappa^2}\), 2 generates a sequence of provers \(\{ f_t\}_{t \in \mathbb{N}}\) such that \(\forall t \in \mathbb{N},\) the size of the \(t\)-th prover’s knowledge set \(| \{ x \in V : \operatorname{succ}(x, f_t) \geq p\} |\) is exponential in \(t\).

To prove [thm:main], we show that for every \(t \in \mathbb{N}\), \(||D_{t + 1}||_{\ell^2(1/\pi)}^2 \leq (\frac{||P_w^\top||_{\ell^2(1/\pi) \to \ell^2(1/\pi)}}{1 - \epsilon})^2\cdot\) \(||D_{t}||^2_{\ell^2(1/\pi)}\), where \(||P_w^\top||_{\ell^2(1/\pi) \to \ell^2(1/\pi)}\) is the operator norm of \(P_w^\top\) in the Hilbert space \(\ell^2(1/\pi)\). By 1, since \((V,P_w)\) satisfies 5, then \(||P_w^\top||_{\ell^2(1/\pi) \to \ell^2(1/\pi)}\leq 1 - \frac{1}{2\kappa^2}\). Finally, [thm:main] follows from 14, which lower bounds \(| \{ x \in V : \operatorname{succ}(x, f_t) \geq p\} |\) using \(\frac{1}{||D_{t}||^2_{\ell^2(1/\pi)}}\). The full proof is in 7.

Thus, if the simple random walk \(P_{\mathrm{s.r.w.}}\) over the theorem graph satisfies \(\mathrm{IS}\) (i.e. for any finite \(A \subset V, \frac{|\{ (e^-, e^+) \in E \;:\; e^- \in A, \;e^+ \notin A\}|}{\sum_{x \in A} \deg(x)} \geq \frac{1}{\kappa}\)), then 2 with a conjecturer, whose transition matrix is \(P_{\mathrm{s.r.w.}}\), generates a sequence of provers \(\{ f_t\}_{t \in \mathbb{N}}\) whose knowledge set grows exponentially.

5 Diversity Measure and an Improved Conjecturing Algorithm↩︎

5.1 Diversity Measure↩︎

Unlike 4, suppose for simplicity the theorem graph has a finite but large number of nodes and \(||\pi||_1 = 1\). ² The following ideas can be instantiated with any \(\tau \in \mathbb{N}\), but practically \(\tau\) should be a small non-zero natural number. The main object of interest in this section is the \(\tau\)-expanded knowledge set of a prover \(f\).

We define an operational notion of diversity of \(f\)’s knowledge as the size of \(K^p_\tau(f)\). \(K^p_\tau(f)\) can be interpreted as the set of theorems that \(f\) can prove by performing \(\tau\) steps of “reasoning" at inference time to reduce the input theorem into one it knows how to prove. 1 depicts two provers \(f_1\), \(f_2\) whose knowledge sets are the same size \(|K^p(f_1)| = |K^p(f_2)|\), but where their \(\tau\)-step expansions are of different sizes: \(|K^p_\tau(f_1)| \ll |K^p_\tau(f_2)|\). Thus, \(f_2\)’s knowledge is more diverse than \(f_1\)’s. Identifying diversity with \(|K^p_\tau(f)|\) reflects the intuition that knowing a diverse set of proof ideas is useful to a prover \(f\) as it increases the set of theorems that \(f\) can prove by combining known proof ideas.

Let \((C_w, P_w, w)\) be a baseline conjecturer satisfying 1 and for convenience denote \(P:= P_w\). Our goal is to design an improved conjecturer that generates a sequence of training distributions \(\{ D_t\}_{t \in \mathbb{N}}\) where at each \(t \in \mathbb{N}\) prover \(f_t\) is trained on \(D_t\), and where \(|K^p_\tau(f_t)|\) increases quickly with \(t\). In fact, [lem:divt-kct-connection] (proved in 11) shows that for each \(t\in \mathbb{N}\) it is reasonable to maximize \(\mathrm{Div}^P_\tau(D_t)\) ([defn:diversity-measure]), a diversity measure of the training distribution \(D_t\).

If prover \(f\) is successfully trained on theorem distribution \(D\) via 2, then \(\mathbb{P}_{x \sim D}[\operatorname{succ}(x,f) \geq p] \geq 1 - \epsilon\). By [lem:divt-kct-connection], \(|K_\tau^p(f)| \geq \frac{(1 - \epsilon)^2}{\sup_{x \in V}\pi(x)} \mathrm{Div}^P_\tau(D)\), so maximizing \(\mathrm{Div}^P_\tau(D)\) of the training distribution is a reasonable proxy for maximizing \(|K_\tau^p(f)|\).

We note that in the setting of 4, where 5 holds for random walk \((V,P)\), then maximizing \(|B(K^p(f), \tau)|\) reduces to maximizing \(|K^p(f)|\). When \(P = P_{\mathrm{s.r.w.}}\), then 5 implies for bounded-degree graphs that there is a reasonable constant \(c\) where for any finite \(A \subset V, |B(A, \tau)| \geq \exp(c\,\tau) |A|\). That is, any finite subset of theorems is diverse. More generally, if 5 holds for \(P\) (not necessarily \(P_{\mathrm{s.r.w.}}\)), then for \(\{ D_t\}_{t \in \mathbb{N}}\) generated as \(D_{t + 1}^\top = D_t^\top P\), we have \(\mathrm{Div}^P_\tau(D_t) = \frac{1}{||D_{t + \tau}||^2_{\ell^2(1/\pi)}}\), where \(\pi^\top P = \pi^\top\). Because the proof of [thm:main] implies fast exponential decay of \(||D_{t}||^2_{\ell^2(1/\pi)}\) as a function of \(t \in \mathbb{N}\) for every \(t\), it follows that \(\mathrm{Div}^P_\tau(D_t)\) grows exponentially for each \(t\). In short, when 5 holds, then the two objectives \(|K^p(f)|\) and \(|K^p_\tau(f)|\) are aligned. As such, the more interesting setting for studying diversity is when 5 does not hold for the baseline random walk \(P\). When \(P=P_{\mathrm{s.r.w.}}\), some intuitive graphs where 5 does not hold are graphs consisting of multiple poorly-interconnected clusters, such as that depicted in 1 or 10. For a graph like in 1, the choice of which nodes to include in \(K^p(f)\) will greatly impact \(K^p_\tau(f)\), making the problem of maximizing both \(K^p(f)\) and \(K^p_\tau(f)\) non-trivial.

5.2 Improved Conjecturing Algorithm↩︎

5 is a conjecturer that generates a sequence of training distributions \(\{ D_t\}_{t \in \mathbb{N}}\), with the aim to maximize \(\mathrm{Div}^P_\tau(D_t)\) at each \(t \in \mathbb{N}\), for a chosen hyper-parameter \(\tau \in \mathbb{N}\). This maximization cannot easily be done in closed form, as the conjecturer is restricted to generate \(D_{t + 1}\) from \(D_t\) by one step of a nearest-neighbor-type random walk. Instead, fixing \(\tau \in \mathbb{N}\), 5 defines a push-forward map \(C : V \to \Delta(V)\) where for any \(x \in V\), \(C(x) \in \Delta(N(x))\) is supported on neighbors \(N(x)\) of \(x\). The weighting of \(C(x)\) is determined by maximizing \(\mathrm{Div}^P_\tau(C(x))\).

\[\begin{align} \forall x \in V, \, C(x) &\leftarrow \arg\max_{\mu \in \Delta(N(x))} \mathrm{Div}^P_\tau(\mu) = \arg\min_{\mu \in \Delta(N(x))} \mu^\top P^\tau \mathrm{diag}(1/\pi) (P^\tau)^\top \mu \label{eq:optim-problem-diversity} \end{align}\tag{4}\]

Where \(\forall z \in V, \mathrm{diag}(1/\pi)[z,z] = \frac{1}{\pi(z)}\). This optimization problem can be solved given the matrix, \(M(x, \tau) \in \mathbb{R}^{|N(x)| \times |N(x)|}\) where for any \(y,y' \in N(x)\), the \((y,y')\)-th entry is: \(M(x, \tau) [y,y'] := e_y^\top P^\tau \mathrm{diag}(1/\pi) (P^\tau)^\top e_{y'}\). We can characterize \(M(x, \tau)\) in terms of diffusion embeddings of the neighbors of \(x\), where a diffusion embedding embeds any node \(z \in V\) to a vector \(p^\tau(z)\) representing the probability distribution of a \(\tau\)-step random walk started at \(z\) according to transition matrix \(P\).

For any \(y,y' \in N(x)\), the \((y,y')\)-th entry of \(M(x, \tau)\) is \(\phi^{\mathrm{diff}}_\tau(y,y')\). Note that the diffusion similarity requires computing \(\frac{1}{\pi(z)}\) for relevant \(z \in V\), but the stationary measure \(\pi(z)\) need only be computed up to a normalizing constant for the optimization problem in 4 . For a conjecturer \((C,P,w )\) satisfying 1, \(\forall z \in V, \pi(z) \propto w(z)\). Let \(M'(x, \tau) = P^\tau \mathrm{diag}(1/w) (P^\tau)^\top\) and \(\forall z \in V\), \(\mathrm{diag}(1/w)[z,z] = \frac{1}{w(z)}\). With regularization strength \(\eta \in [0,0.5]\), \(\forall x \in V\), 5 computes:

\[\begin{align} C(x) &\leftarrow \arg\max_{\substack{ \mu \in \Delta(N(x))\\ \mu(y) \geq \eta/\deg(x),\;\forall y \in N(x) }} \mathrm{Div}^P_\tau(\mu) = \arg\min_{\substack{ \mu \in \Delta(N(x))\\ \mu(y) \geq \eta/\deg(x),\;\forall y \in N(x) }} \mu^\top M'(x, \tau) \mu \label{eq:diff-sim-optim} \end{align}\tag{5}\]

This mapping \(C : V \to \Delta(V)\) defined in 5 can be substituted in for \(C_w\) in line 4 of 3, called in line 4 of the prover-conjecturer system (2). If \(G\) is finite, connected, undirected, and non-bipartite, the regularization with \(\eta > 0\) ensures (via 15) the random walk induced by \(C\) converges to a stationary measure, eventually exploring the entire graph. Note that 5 uses 6 to compute diffusion embeddings.

As a concrete guarantee, [prop:e2e-guarantee-alg2] shows that 5 provably explores the theorem graph \(G\) faster than a simple random walk when \(G\) is in a special class of clustered graphs.

In the regime where the clique size \(M\) is much larger than the inter-cluster connectivity (\(M \gg r^2\)), 5 improves over the baseline simple-random-walk-based conjecturing algorithm in that: both conjecturers define a random walk over the meta-graph, but that of 5 has a larger spectral gap [37]. The source of the improvement is that 5 up-weights the probability of making inter-cluster transitions, compared to the simple random walk. This becomes useful when the cluster size \(M\) is large, in which case the simple random walk can become stuck in a cluster for a large number of steps.

[prop:e2e-guarantee-alg2] shows that the diversity of theorem distributions generated under 5 (resp. a simple-random-walk-based conjecturer) can be guaranteed to exceed \(1 - \epsilon\) in \(t_{\mathrm{improved}}\) steps (resp. \(t_{\mathrm{baseline}}\) steps), and where \(t_{\mathrm{improved}} \leq O(\frac{r^2}{M}) \,t_{\mathrm{baseline}}\). Although this does not prove a matching lower-bound to show separation between 5 and the baseline, we believe the bounds used to derive these results are tight so that in the worst case over all possible meta-graphs instantiating [defn:clique-graph], 5 is \(\Theta(\frac{M}{r^2})\) times more efficient than a simple-random-walk-based conjecturer, which is substantial when the clusters are very dense (\(M \gg r^2\)).

The proof of [prop:e2e-guarantee-alg2] is in 9. We think it is plausible that 5 improves over a baseline simple random walk \(P = P_{\mathrm{s.r.w.}}\) for a broader class of clustered graphs (graphs like those depicted in 10) than [defn:clique-graph], but we do not have a formal guarantee. Our intuition of 5 on clustered graphs is that it defines a random walk that, at node \(x\), has a higher chance to transition to neighbors of \(x\) in a different cluster than \(x\). This lets the random walk escape from its starting cluster faster and should enable it to explore the entire theorem graph faster.

In general, \(\tau\) should not be set too small or too big. If \(\tau =0\), the diffusion embedding is not informative since every node \(x \in V\) is embedded as \(e_x \in \mathbb{R}^{|V|}\). If \(\tau\) is larger than the mixing time of \(P\), then \(\forall x \in V,(P^\top )^\tau e_x \approx \pi\), so the diffusion embedding is also not informative. When the theorem graph is a clustered graph consisting of equally sized clusters, there should exist a natural setting for \(\tau\): the number of steps it takes a random walk to “forget" its exact starting node, where it still”remembers" its starting cluster. More precisely, the ideal property of \(\tau\) on a clustered graph is that for two nodes \(x, y\) in the same cluster, their \(\tau\)-step random walk distributions are approximately the same: \(p^\tau(x) \approx p^\tau(y)\), but for \(x, y\) in different clusters, their \(p^\tau(x)\) and \(p^\tau(y)\) differ greatly. Then, \(p^\tau(x)\) serves as an identifier for which cluster \(x\) is in.

5 accepts as input \(\tau \in \mathbb{N}\) and a baseline reversible conjecturer \((C_w, P_w, w)\), satisfying 1. It returns an improved conjecturer. 5 improves the baseline conjecturer by performing a \(\tau\)-step look-ahead over the graph to maximize diversity. In principle, this algorithmic scaffold can be applied to conjecturers trained empirically, if they satisfy 1. The random walk defined by 5 may not be reversible, so the algorithmic scaffold cannot be recursively applied to its own output.

5.3 Computing Diffusion Similarity via Contrastive Learning↩︎

[thm:contembd] shows the diffusion similarity (used in step 4 of 5) can be computed via learned contrastive embeddings. A self-contained summary of contrastive learning is in 8.

The proof of [thm:contembd] is in 8.2. [thm:contembd] shows that the diffusion similarity of any two nodes on the graph (a quantity computed in step 3 of 5) can instead be computed from the Euclidean inner product of their learned embeddings. Given \(n\) samples \(\{ x_i\}_{i \in [n]} \subset V\) drawn i.i.d. from the stationary measure \(\pi \in \Delta(V)\) of \(P\), an embedding model \(\mathcal{F}_{\mathrm{emb}}\ni h_{\hat{\theta}} : V \to \mathbb{R}^{|V|}\) can be learned by computing the empirical risk minimizer (ERM, [defn:erm-cont]) of the empirical contrastive loss \(\hat{\mathcal{L}}_{\mathrm{cont}, n}\) in 3 . Under additional assumptions, we show in [thm:e2e-contrastive-learning-result] an end-to-end result where ERM, in a finite-sample regime with small embedding dimension, yields embeddings that can be used to approximate the diffusion similarity.

[thm:contembd] and [thm:e2e-contrastive-learning-result] motivate 7, a conjecturing algorithm that is analogous to 5, but with 6 replaced by a contrastive-learning procedure.

Finally, we discuss how to instantiate [thm:contembd] and [thm:e2e-contrastive-learning-result] for a local subgraph of \(G\) around the theorems of interest, rather than needing to take \(G\) to be the entire theorem graph, which is impractical. For a theorem graph \(G = (V,E)\), define the following notion of a subgraph of \(G\) supported on the \(T\)-neighborhood of a node \(x \in V\).

A simple observation is that: for any \(x \in V\), on a \(T = \tau + 1\) local subgraph around \(x\), the \(\tau\)-step random walk distribution starting from any neighbor \(z \in N(x)\), \(p^\tau_{G_{x,T}}(z)\) is the same as \(p^\tau(z)\). In addition, for any reversible Markov chain \((V,P)\) on the graph \(G\) with stationary measure \(\pi\), for any \(x \in V\) and \(T \in \mathbb{N}\), the stationary measure \(\pi_{x,T}\) is equal to \(\pi\) restricted to \(B(x,T) \subset V\), up to a multiplicative constant, by the self-loop construction of \(G_{x,T}\). Thus, the diffusion similarity computed on the local subgraph \(G_{x,T}\) differs from that computed on \(G\) by a multiplicative constant, which means the locally-computed diffusion similarity is sufficient for solving the optimization problem in 4 .

To learn the spectral diffusion embedding for reversible Markov chain \((V,P)\), of reversible conjecturer \((C,P,w) := (C_w,P_w,w)\) in a local \(T\)-neighborhood around a node \(x \in V\) via 8, one will require access to the following oracles, defined in [defn:T-neighborhood].

1. The push-forward map \(C_{x,T} : B(x,T) \to \Delta(B(x,T))\) representing the restricted Markov chain \((V_{x,T}, P_{x,T})\), where \(\forall y \in B(x,T)\), \(C_{x,T}(y) = P_{x,T}[y] \in \Delta(B(x,T))\),

2. i.i.d. sample access to \(\pi_{x,T} \in \Delta(B(x,T))\).

The construction of these oracles, given \(x \in V\), \(T \in \mathbb{N}\), and neighbor oracle \(N : V \to 2^V\) of \(G\), is conceptually straightforward. We describe the details of their constructions in 9 of 8.1.5.

6 Conclusion and Limitations↩︎

We formalized the space of theorems as a graph and a conjecturer as a nearest-neighbor-type Markov chain over the theorem graph. [thm:main] shows that under 5, the knowledge of the prover trained via 2 grows exponentially with the number of iterations. For the case where 5 does not hold, we propose a diversity measure ([defn:diversity-measure]) for a training distribution of theorems generated by a conjecturer and an improved conjecturing algorithm (5) that locally maximizes this diversity measure, by computing the diffusion similarity (3) between neighboring theorems in the theorem graph. Finally, we describe a method to compute the diffusion similarity using contrastive learning ([thm:contembd] and [thm:e2e-contrastive-learning-result]).

One limitation of the current framework is that the conjecturer is not adaptive toward the particular prover \(f_t\) at iteration \(t\), but rather adaptive toward the prover class, which determines the edge set \(E\). It defines a time-homogeneous nearest-neighbor random walk, whereas a time-inhomogeneous random walk would be more realistic. Another intuition that is not captured by the current framework is that of theorem compositionality. In particular, one can imagine a conjecturer that has knowledge of two theorems \(X \to Y\) and \(Y \to Z\) may be able to conjecture \(X \to Z\), but this is not easily compatible with the view that a conjecturer maps a single theorem to a distribution of theorems. More broadly, an interesting question is how to extend our analysis to a hypergraph of theorems or dependent types [26]. Finally, we note that although this theoretical framework is instantiated for the setting of formal theorem proving, it could potentially serve as a framework for understanding automated synthetic data generation for other verifiable domains besides formal theorem proving.

Acknowledgements↩︎

TC acknowledges funding from an NSF Graduate Research Fellowship. This work was supported in part by an OpenAI Superalignment Fast Grant and by DARPA AIQ under Agreement No. HR00112520023.

We are deeply grateful to Tengyu Ma for many insightful discussions. We also thank Kaiyue Wen for discussions.

7 Proof of [thm:main]↩︎

The purpose of this section is to eventually prove [thm:main] in 7.2.

7.1 Preliminaries.↩︎

7.1.0.1 Isoperimetric Inequality.

Let \(G = (V, E)\) be an undirected graph with a countable set of vertices, \(V\), and edges \(E\). \(G\) is connected, and is locally finite (every vertex has finite degree). Let \(P\) be a Markov chain transition matrix over \(V\) (We will refer to the pair \((V,P)\) as a Markov chain). The simple random walk is a Markov chain where every node \(x\) transitions uniformly to one of its neighbors in the graph, \(N(x) := \{ x' \in V : (x,x') \in E\}\). In the following, we define some basic properties of Markov chains over graphs.

For \(n \in \mathbb{N}\), let \(p^{(n)}(x,y)\) denote the probability the Markov chain \((V,P)\) initialized at \(x\) is at \(y\) at the \(n\)-th step.

For the remaining definitions, we will assume the Markov chain is irreducible. We define aperiodicity as follows.

Note that if a Markov chain is irreducible and for some \(x \in V\), \(\mathrm{gcd}\{ n \in \mathbb{N}: p^{(n)}(x,x) > 0\} = 1\), then for any \(x' \in V\), \(\mathrm{gcd}\{ n \in \mathbb{N}: p^{(n)}(x',x') > 0\} = 1\).

A stationary measure \(\pi : V \to (0,\infty)\) where \(\pi^\top = \pi^\top P\). If \(||\pi||_1 = 1\), then it is a stationary distribution. The following Theorem shows that irreducibility and aperiodicity imply mixing for finite Markov chains.

The following definitions introduce the notion of reversibility and conductance.

Now, we define the Isoperimetric Inequality for a Markov chain over a graph, which will generalize [defn:IS]. Let \((V,P)\) be a reversible, irreducible Markov chain with total conductance \(\pi(\cdot)\), edge conductance \(a(\cdot, \cdot)\). Define the following quantities.

\[\begin{align} \pi(A) &:= \sum_{x \in A} \pi(x), \quad \forall A \subset V\\ a(D) &:= \sum_{e \in D} a(e^-, e^+), \quad \forall D \subset E(P)\\ \partial A &:= \mathrm{set of all edges in E(P) with}\\ &\mathrm{one endpoint in A and the other in V - A} \end{align}\]

For the definition of \(\partial A\), note that the graphs we study in this work are all undirected. We now define the Isoperimetric Inequality.

The particular function \(\mathscr{F}: \mathbb{R}_+ \to \mathbb{R}_+\) we care about in this work is \(\mathscr{F}(t) = t\), corresponding to the Strong Isoperimetric Inequality defined in [defn:IS]. However, for the proofs of some of the following Lemmas, it is useful to define, for \(1 \leq d \leq \infty\), the \(d\)-dimensional Isoperimetric Inequality \(\mathrm{IS}_d\) as 8 with \(\mathscr{F}(t) = t^{1 - 1/d}\). The strong Isoperimetric Inequality \(\mathrm{IS}\) can be thought of as \(\mathrm{IS}_d\) with \(d = \infty\).

7.1.0.2 Hilbert Spaces and Norms.

With \((V,P)\) being an irreducible, reversible Markov chain with stationary measure \(\pi : V \to (0,\infty)\), let \(\ell_0(V)\) denote the linear space of finitely supported functions on \(V\) (i.e. functions that are non-zero only on a finite number of elements of \(V\)). For an (undirected) edge \(e = (e^-, e^+) \in E\), define the resistance as \(r(e) := \frac{1}{a(e^-, e^+)}\). The following defines Hilbert spaces of functions, relevant to [thm:main].

We introduce the following difference operator

\[\begin{align} \nabla : \ell^2(V, \pi) \to \ell^2(E, r), \quad \nabla f(e) = \frac{f(e^+) - f(e^-)}{r(e)} \end{align}\]

Define the following norms:

7.1.0.3 Preliminary Lemmas.

The next few Lemmas will be used to prove 3, which is key to proving the final [thm:main].

Note that \(\ell_0(V) \subset \mathcal{D}(P)\).

Now, we recall some facts of linear operators. Let \(Q = (q(i,j))_{i,j \in I}\) be a non-negative real matrix over a countable set. \(Q\) acts on functions (vectors) \(I \to \mathbb{R}\) in the usual way by matrix multiplication on the left. Define the operator norm:

Define the adjoint of a linear operator:

If \(Q = Q^*\), it is self-adjoint, and its operator norm has the following Rayleigh characterization.

7.1.0.4 Key Theorem.

3 is the key theorem which enables us to prove [thm:main].

Consider an irreducible, reversible Markov chain \((V, P)\) that satisfies the strong Isoperimetric inequality with Isoperimetric constant \(\kappa\):

\[\begin{align} \mathrm{For every finite } A \subset V, \quad \pi(A) \leq \kappa \cdot a(\partial A) \end{align}\]

Then, the operator norm of \(P\) in \(\ell^2(V,\pi)\) is at most \(1 - \frac{1}{2\kappa^2}\). That is, \(||P||_{\ell^2(V, \pi) \to \ell^2(V, \pi)} \leq 1 - \frac{1}{2\kappa^2}\).

The following Corollary establishes a one-step contraction due to the random walk according to \(P\) on a graph satisfying \(\mathrm{IS}\).

7.2 Proof of [thm:main]↩︎

8 Theorems about Diffusion Similarity and Contrastive Learning↩︎

The purpose of this section is to show the connection between contrastive learning and diffusion similarity, and show how an embedding model learned by minimizing a contrastive loss can be used to compute the diffusion similarity (and diffusion distance) between points on a graph. Our main results, in 8.2, include [thm:contembd], an infinite-sample and large embedding dimension learning result, and [thm:e2e-contrastive-learning-result], a finite-sample and small embedding dimension learning result.

8.1 Preliminary Lemmas↩︎

8.1.1 Setup↩︎

Contrastive learning defines an algorithm for learning an embedding model that maps elements from a domain \(V\) (e.g. the set of real-world images) into Euclidean space \(\mathbb{R}^k\) for some \(k \in \mathbb{N}\). It is most notably used for training neural networks as embedding models, and we let \(\mathcal{F}_{\mathrm{emb}}\) denote the hypothesis class of models \(h_\theta : V \to \mathbb{R}^k\) which we assume contains the ground-truth embedding model that we must learn. The core idea of contrastive learning is to define two distributions of pairs of elements in \(V\): a positive pair distribution \(D_+ \in \Delta(V \times V)\) , and a negative pair distribution \(D_- \in \Delta(V \times V)\). Given i.i.d. samples from both distributions, the trained model is encouraged to embed two elements sampled from a positive pair \((x,y) \sim D_+\) close together in Euclidean space, while embedding two elements sampled from a negative pair \((x,x') \sim D_-\) far apart in Euclidean space. These two distributions of pairs of elements are used to define a contrastive loss, and training the model amounts to minimizing an empirical estimate of the contrastive loss from finite samples.

In fact, contrastive learning can be described mathematically through the lens of matrix factorization, as articulated in [30]. The benefit of this viewpoint of contrastive learning is that it enables us to provably characterize the learned embeddings and the sample complexity of learning them. In the following, we will describe and use the mathematical setup for contrastive learning of [30].

Let the domain \(V\) consist of \(N \in \mathbb{N}\) elements, where \(N\) is large but finite. We will identify \(V\) with \([N]\) here for simplicity. Define \(\mu \in \Delta([N])\) as the base distribution and \(Q \in \mathbb{R}^{N \times N}\) as an augmentation scheme. Alternatively, overloading notation, we can view \(Q : [N] \to \Delta(N)\) as a mapping from an element \(x\) to a distribution over augmentations of \(x\), \(Q(x)\). For every \(x \in [N]\), this distribution of augmentations, \(Q(x)\), equals the \(x\)-th row of the matrix-representation of \(Q\).

We will first introduce the matrix factorization viewpoint of contrastive learning, and we will from this how to define the positive and negative pair distributions \(D_+, D_- \in \Delta([N]\times [N])\) from \(\mu\) and \(Q\) and the final learning algorithm. Let \(A \in \mathbb{R}^{N \times N}\) and its normalization \(\overline{A}\) be positive semi-definite (p.s.d.) matrices of the form,

\[\begin{align} A &= Q^\top \,\mathrm{diag}(\mu) \,Q\\ D &= \mathrm{diag}(A \mathbf{1})\\ \overline{A} &= D^{-1/2} A D^{-1/2} \end{align}\]

For rank-\(k\) factor \(F_\theta \in \mathbb{R}^{N \times k}\), let \(\mathcal{L}_{\mathrm{mf}}(F_\theta) := ||\overline{A} - F_\theta F_\theta^\top||_F^2\) be the matrix factorization loss for matrix \(\overline{A} \in \mathbb{R}^{N \times N}\). Let \(\mathcal{F}_{\mathrm{emb}}\) be the class of embedding models. We will parameterize \(F_\theta\) by an embedding model \(h_\theta : [N] \to \mathbb{R}^k\). Towards this, if we let \(\sigma_{xy}\) denote the \((x,y)\)-th entry of \(A\),

\[\begin{align} A &= [\sigma_{xy}]_{x,y \in [N]}\\ \mathrm{With } \sigma_x &:= \sum_{y \in [N]} \sigma_{xy}\label{eq:wx-defn} \end{align}\tag{11}\]

and we parameterize \(F_\theta \in \mathbb{R}^{N \times k}\) where \(\forall x \in [N], F_\theta[x] = \sqrt{\sigma_x} h_\theta(x)^\top\) for \(h_\theta : [N] \to \mathbb{R}^k\), then \(\mathcal{L}_{\mathrm{mf}}(F_\theta) = \mathcal{L}_{\mathrm{mf}}(h_\theta)\) (overloading notation) is expressible in the following form.

\[\begin{align} \mathcal{L}_{\mathrm{mf}}(h_\theta) &:= ||\overline{A} - F_\theta F_\theta^\top||_F^2\\ &= \sum_{x,y \in [N]} \Big(\frac{\sigma_{xy}}{\sqrt{\sigma_x} \sqrt{\sigma_y}} - \sqrt{\sigma_x}\sqrt{\sigma_y}h_\theta(x)^\top h_\theta(y) \Big)^2\\ &= \mathrm{const} + \sum_{x,y \in [N]}\sigma_x \sigma_y (h_\theta(x)^\top h_\theta(y))^2 - 2\sum_{x,y \in [N]}\sigma_{xy} h_\theta(x)^\top h_\theta(y)\tag{12}\\ &= \mathrm{const} + \mathbb{E}_{x, x^-} (h_\theta(x)^\top h_\theta(x^-))^2 - 2 \cdot \mathbb{E}_{x, x^+}h_\theta(x)^\top h_\theta(x^+)\\ &= \mathrm{const} + \mathcal{L}_{\mathrm{cont}}(h_\theta)\tag{13}\\ \mathrm{Where } \mathcal{L}_{\mathrm{cont}}&: \mathcal{F}_V^{(k)} \to \mathbb{R}\\ \mathcal{L}_{\mathrm{cont}}(h_\theta) &:= \mathbb{E}_{x, x^-} (h_\theta(x)^\top h_\theta(x^-))^2 - 2 \cdot \mathbb{E}_{x, x^+}h_\theta(x)^\top h_\theta(x^+)\tag{14} \end{align}\]

Where \(\mathcal{F}_{V}^{(k)}\) denotes the class of all functions mapping \(V\) to \(\mathbb{R}^{k}\). Amazingly, \(\mathcal{L}_{\mathrm{cont}}(h_\theta) := \mathbb{E}_{x, x^-} (h_\theta(x)^\top h_\theta(x^-))^2 - 2 \cdot \mathbb{E}_{x, x^+}h_\theta(x)^\top h_\theta(x^+)\) is one version of the (population) contrastive loss function, similar to what is used empirically.

12 in the derivation above naturally defines the positive pair distribution as where \((x,y) \in [N]\times[N]\) has marginal probability of \(\sigma_{xy}\) of being sampled. This corresponds to the sampling process of first sampling an element from the base distribution first, \(z \sim \mu\), and then sampling the pair elements as independent augmentations \(x \sim Q(z)\), \(y\sim Q(z)\), returning \((x,y)\). Similarly, since a negative pair \((x,y) \in [N]\times[N]\) has marginal probability of \(\sigma_x \sigma_y\) in 12 , the natural negative pair distribution corresponds to first sampling \(z_x, z_y \sim \mu\) independently, and then sampling \(x \sim Q(z_x), y \sim Q(z_y)\), returning \((x,y)\).

Crucially, since \(\mathcal{L}_{\mathrm{cont}}(h_\theta)\) and \(\mathcal{L}_{\mathrm{mf}}(h_\theta)\) differ by only an additive constant independent of \(h_\theta\), we can understand the global minimizers of \(\mathcal{L}_{\mathrm{cont}}\) via the global minimizers of \(\mathcal{L}_{\mathrm{mf}}\). In particular, the Eckart-Young-Mirsky Theorem characterizes the global minimizers of \(\mathcal{L}_{\mathrm{mf}}\) via the spectrum of \(\overline{A}\) [40]. In the case \(\overline{A} = U \Sigma U^\top\) is p.s.d., then the global minimizer \(F_k \in \mathbb{R}^{N \times k}\) is of the form

\[\begin{align} F_k = U_k \Sigma_k^{1/2}R \end{align}\]

Where \(R \in O^{k \times k}\) is any \((k \times k)\) orthogonal matrix.

In addition to having an analytic characterization of the global minima, one other useful property of \(\mathcal{L}_{\mathrm{cont}}\) is that it is written as an expectation, and so can be approximated by an empirical risk. For a dataset \(\{ \overline{x}_i\}_{i \in [n]} \subset V\), define the empirical contrastive loss as:

\[\begin{align} &\hat{\mathcal{L}}_{\mathrm{cont}, n}(h_{\theta'}) :=\\ &-\frac{2}{n} \sum_{i \in [n]} \mathbb{E}_{\substack{x \sim Q(\cdot | \overline{x}_i),\\ x^+ \sim Q(\cdot | \overline{x}_i)}} (h_{\theta'}(x)^\top h_{\theta'}(x^+)) + \frac{1}{n(n - 1)} \sum_{i,j \in [n], i \neq j}\mathbb{E}_{\substack{x \sim Q(\cdot | \overline{x}_i),\\ x^- \sim Q(\cdot | \overline{x}_j)}} (h_{\theta'}(x)^\top h_{\theta'}(x^-))^2 \label{mtnixgye} \end{align}\tag{15}\]

Claim D.2 of [30] shows that \(\mathbb{E}_{\{ \overline{x}_i\}_{i \in [n]} \sim \mu} \hat{\mathcal{L}}_{\mathrm{cont}, n}(h_{\theta}) = \mathcal{L}_{\mathrm{cont}}(h_\theta)\), i.e. that \(\hat{\mathcal{L}}_{\mathrm{cont}, n}\) is unbiased. Define the empirical risk minimizer (ERM) as follows.

8 describes a procedure to use empirical risk minimization to learn an embedding model from finite samples from the base distribution.

As we will later see in 6 and [lem:contrastive-learning], under some assumptions, the empirical risk minimizer (ERM) will be also approximately minimize the population contrastive loss. The assumptions necessary for that result are expressed in terms of Rademacher complexity, a core concept of Statistical Learning Theory. For \(k \in \mathbb{N}\), we use the definition of empirical Rademacher complexity of a function class \(\mathcal{F}\) of models \(\mathcal{F}\ni h: V \to \mathbb{R}^k\) used in [30].

Note this definition takes a \(\max\) over the \(n\) datapoints \(x_1, \ldots, x_n\) rather than an expectation, as is usual [35]. 6 analyzes the generalization error of the ERM, using Statistical Learning Theory.

8.1.2 Lemmas on Contrastive Learning↩︎

[30] say, as a comment immediately after their Theorem 4.1, that \(\hat{\mathcal{R}}_{n}(\mathcal{F})\) typically looks like \(\sqrt{\frac{\mathcal{C}(\mathcal{F})}{n}}\) where \(\mathcal{C}(\mathcal{F})\) is an \(\mathcal{F}\)-dependent constant. Assuming this is the case, then as a consequence of 6, the minimizer of the empirical contrastive loss, with \(n = \Theta(\frac{\mathcal{C}(\mathcal{F}_{\mathrm{emb}})\, \mathrm{poly}(k, \chi)}{\epsilon^2}\log \frac{1}{p_{\mathrm{erm fails}}})\) i.i.d. samples, is \(\epsilon\)-minimizer embedding model with probability at least \(1 - p_{\mathrm{erm fails}}\). We write this explicitly in the following Lemma.

Note that as the proof of 6 bounds the excess test loss of the ERM with uniform convergence, this result can actually be strengthened: any \(\frac{\epsilon}{2}\)-minimizer of the empirical contrastive loss, with \(n = \Theta(\frac{\mathcal{C}(\mathcal{F}_{\mathrm{emb}}) \, \mathrm{poly}(k, \chi)}{\epsilon^2}\log \frac{1}{p_{\mathrm{erm fails}}})\) i.i.d. samples, is \(\epsilon\)-minimizer embedding model with probability at least \(1 - p_{\mathrm{erm fails}}\).

8.1.3 The Connection Between Diffusion Embeddings and Contrastive Learning↩︎

In the following, assume the graph \(G = (V,E)\) is finite (\(|V| < \infty\)), undirected, and connected.

[lem:diff-dist] establishes a connection between diffusion similarity and Euclidean inner product of the spectral diffusion embeddings.

As a corollary, for any \(u,v \in V\), the diffusion distance \(||p^t(u)- p^t(v)||_{\ell^2(1/\pi)} = ||\Phi_t(u)- \Phi_t(v)||_2\). For more about diffusion distance, see [29] and [36].

The following Lemma describes the approximation properties of a diffusion embedding with small embedding dimension \(k \in [|V| - 1]\) (rather than the full \(|V|\)-dimensional embedding), when \(\lambda_{k + 1}^{2t}\) is small.

We will now describe how to learn the embeddings \(\{ \Phi_t^{\leq k}(u)\}_{u \in V}\) for general \(k \in [|V|]\) and \(t \in \mathbb{N}\). [lem:cont-learn-min-general] shows the global minimizers of the contrastive loss recover \(\{ \Phi^{\leq k}_t(u)\}_{u \in V}\) up to an orthogonal transformation.

8.1.4 Matrix Factorization Lemmas↩︎

[lem:diff-dist] and [lem:cont-learn-min-general] motivate the idea of using embeddings learned via contrastive learning to compute the diffusion similarity and distance. [lem:contrastive-learning] shows that finding the ERM (or \(\frac{\epsilon}{2}\)-ERM) suffices, with high probability, to find an \(\epsilon\)-minimizer of the population contrastive loss \(\mathcal{L}_{\mathrm{cont}}\). [lem:eps95close95to95opt], a Lemma about matrix-factorization, is useful in quantifying how close an embedding corresponding to such an \(\epsilon\)-minimizer is to a ground-truth embedding, up to a rotation.

To start, 10, 9, and 8 are introduced here to prove [lem:eps95close95to95opt]. Note that for two matrices \(A, B \in \mathbb{R}^{n \times n}, \langle A,B \rangle := \mathrm{tr}(A^\top B)\) denotes the Hilbert-Schmidt inner product of the two matrices, with \(||A||_F^2 = \langle A, A\rangle\).

11 is a simple Lemma that converts the guarantee from [lem:eps95close95to95opt] into one about the embedding functions parameterizing matrices \(F_\theta\) and \(F_*\).

8.1.5 Learning Contrastive Embeddings on Local Subgraphs↩︎

In addition, we would like the embeddings to be learned locally, not for the entire graph simultaneously. For a theorem graph \(G = (V,E)\), define the following notion of a subgraph of \(G\) supported on the \(T\)-neighborhood of a node \(x \in V\). In the following, we will denote \((C,P,w) := (C_w, P_w, w)\) as a reversible conjecturer satisfying 1, to simplify notation.

On a \(T = \tau + 1\) local subgraph centered at \(x \in V\), the \(\tau\)-step random walk distribution of \(x\) and any neighbor \(y \in N(x)\) is the same as that on the entire graph.

12 shows the scale-\(\tau\) diffusion embedding can be computed locally, in a \((\tau+1)\) neighborhood around the queried node. In addition, for any reversible Markov chain \((V,P)\) on the entire graph \(G\) with stationary measure \(\pi\), for any \(x \in V\) and \(T \in \mathbb{N}\), the stationary measure \(\pi_{x,T}\) is equal to \(\pi\) restricted to \(B(x,T)\), up to a multiplicative constant, by the self-loop construction of \(G_{x,T}\). Thus, the diffusion similarity and distance computed locally differs from that computed globally by a multiplicative constant, which means the locally-computed diffusion similarity is sufficient for solving the optimization problem in 4 .

To learn the spectral diffusion embedding for reversible Markov chain \((V,P)\), of conjecturer \((C,P,w)\) in a local \(T\)-neighborhood around a node \(x \in V\) via 8, one will require access to the following oracles, defined in [defn:T-neighborhood].

1. The push-forward map \(C_{x,T} : B(x,T) \to \Delta(B(x,T))\) of the restricted Markov chain \((V_{x,T}, P_{x,T})\), where \(\forall y \in B(x,T)\), \(C_{x,T}(y) = P_{x,T}[y] \in \Delta(B(x,T))\),

2. i.i.d. sample access to \(\pi_{x,T} \in \Delta(B(x,T))\).

For \((V_{x,T}, P_{x,T})\), it suffices to have access to the original conjecturer \((C,P,w) := (C_w, P_w, w)\) on \(G\) and the neighbor oracle \(N_{G_{x,T}} : V \to 2^V\) of the local graph \(G_{x,T}\) supported on \(B(x, T)\). This is because for any \(y \in B(x,T)\), to sample \(z \sim C_{x,T}(y)\), one can first sample \(z' \sim C(y)\). Then, if \(z' \in N_{G_{x,T}}(y)\), set \(z = z'\). Else, set \(z = y\). \(z\) will be a sample from \(C_{x,T}(y)\) with the correct distribution.

9 describes how to compute \(N_{G_{x,T}} : V \to 2^V\) and \(\pi_{x,T}\). It involves first performing a \(T\)-step BFS starting from node \(x\). Once the set of all theorems in the \(T\)-neighborhood of \(x\) is collected, it is straightforward to create an oracle for \(N_{G_{x,T}}\). Regarding the sampler for \(\pi_{x,T}\), because \(\forall y \in B(x,T), \pi_{x,T}(y) \propto \pi(y) \propto w(y)\), then \(\pi_{x,T}(y) = \frac{w(y)}{\sum_{z \in B(x,T)} w(z)}\). It suffices to compute the vector \(\pi_{x,T}\) for all \(y \in B(x,T)\).

8.2 Main Theorems↩︎

Below is our end-to-end learning result, which can be viewed as a finite-sample, small-embedding dimension version of [thm:contembd].

9 Instantiating 5 on Clustered Graphs↩︎

In this section, we first describe a concrete end-to-end result for how 5 improves over a simple random walk, in terms of diversity ([defn:diversity-measure]), on a special class of clustered graphs.

9.1 End-to-End Result of 5 on Clique Graphs↩︎

[prop:e2e-guarantee-alg2] is an end-to-end result for 5, showing that on a special class of theorem graphs ([defn:clique-graph]), that 5 explores the graph faster than a simple random walk. The final guarantee is in terms of the spectral gaps of the random walks, and the diversity of the distributions they generate, according to [defn:diversity-measure].

10 Justification of 2↩︎

The core result of this section is [lem:567-imply-1-4], which justifies 2 by showing that finer-grained assumptions inspired from statistical learning theory implies 2.

10.1 Statistical Learning Theory Inspired Assumptions↩︎

First, we introduce Assumptions 6 - 8. Let \(\mathrm{Ver}: V \times \{ 0,1\}^* \to \{ 0,1\}\) be a formal verifier where for theorem \(x \in V\), then \(\mathrm{Ver}(x,y) = 1\) iff \(y \in \{0,1\}^*\) is a correct proof of \(x\). The first assumption assumes the function class \(\mathcal{F}_{\mathrm{prover}}\) of provers \(\mathcal{F}_{\mathrm{prover}}\ni f : V \to \Delta(\{ 0,1\}^*)\) can express the ground-truth function.

Each \(f \in \mathcal{F}_{\mathrm{prover}}\) maps a theorem to a distribution of proofs (\(f : V \to \Delta(\{ 0,1\}^*)\), where \(V\) is the set of theorems). Thus we can define a notion of the success rate of a prover on a theorem as the probability that the prover outputs a correct proof. Formally, let \(f(x,r)\) be the output of prover \(f\) on theorem \(x\) and random seed \(r\), where \(r \sim D_r\). Define the following loss function over \(\mathcal{F}_{\mathrm{prover}}\) (which abstracts away the randomness \(r \sim D_r\) into a success rate):

We define the empirical risk minimizer (ERM) as follows.

The Rademacher complexity⁴ is defined as follows.

Upper bounding the Rademacher complexity of \(\ell(\mathcal{F}_{\mathrm{prover}})\) will upper bound the generalization error of the ERM. In particular,

In this context, we assume an upper bound on the Rademacher Complexity of the function class \(\ell(\mathcal{F}_{\mathrm{prover}})\).

The next assumption describes under what conditions it is efficient to find the ERM from the model class \(\mathcal{F}_{\mathrm{prover}}\), on a size \(n\) dataset of i.i.d. theorems from a distribution of theorems. In particular, a necessary condition for such a procedure to find the ERM is that each theorem in the training distribution has a proof that can be efficiently found.

Note that in practice, we may only be able to efficiently find an \(\epsilon_{\mathrm{opt}}\)-ERM, for any reasonable \(\epsilon_{\mathrm{opt}} > 0\), where an \(\epsilon_{\mathrm{opt}}\)-ERM is a prover \(\tilde{f}^{(n)}\) where

\[\begin{align} \mathcal{L}_n(\tilde{f}^{(n)}, \{ x_i\}_{i \in [n]}) \leq \min_{f \in \mathcal{F}_{\mathrm{prover}}} \mathcal{L}_n(f, \{ x_i\}_{i \in [n]}) + \epsilon_{\mathrm{opt}} \end{align}\]

However, the remaining analysis only requires \(\mathcal{L}(\tilde{f}^{(n)},D) - \mathcal{L}(f^*, D) \leq \epsilon_{\mathrm{opt}} + 2 \cdot \sup_{f \in \mathcal{F}_{\mathrm{prover}}} |\mathcal{L}(f, D) - \mathcal{L}_{n}(f, \{ x_i\})|\). With \(n = \Theta(\frac{\mathcal{C}(\mathcal{F}_{\mathrm{prover}})}{\epsilon_{\mathrm{gen}}^2})\) samples, we get \(L(\tilde{f}^{(n)},D) - L(f^*, D) \leq \epsilon_{\mathrm{opt}} + \epsilon_{\mathrm{gen}}\) with high probability. Thus, for any reasonable desired accuracy level \(\epsilon\), we can set \(\epsilon_{\mathrm{opt}}, \epsilon_{\mathrm{gen}} = \epsilon/2\), finding the \(\epsilon_{\mathrm{opt}}\)-ERM with generalization gap of \(\epsilon_{\mathrm{gen}}\). The necessary sample complexity would only increase by a factor of 4, a constant factor which we neglect. With this understanding, we keep the current phrasing of 8 of assuming the ERM is tractable.

10.2 Proof of [lem:567-imply-1-4]↩︎

We now prove the main result of this section.

11 Auxiliary Lemmas↩︎

12 Figures↩︎

References↩︎

---

1. To further motivate diffusion similarity, note it is closely related to diffusion distance, used for graph partitioning [7].↩︎

2. We believe the following analysis can be extended to infinite graphs.↩︎

3. Alternatively, note that since \(P\) is reversible, \(\mathrm{diag}(\pi)P\) is symmetric. Let symmetric matrix \(\overline{A} = \mathrm{diag}(\pi)^{1/2}P \mathrm{diag}(\pi)^{-1/2} = \sum_{i}\lambda_i v_i v_i^\top\) with \(\{ v_i\}_{i \in [|V|]}\) being orthonormal. Then \(\forall i \in [|V|], \, \phi_i = \mathrm{diag}(\pi)^{-1/2} v_i\).↩︎

4. This definition is different than [defn:rad-complexity], previously defined and used in the context of [30] in 8↩︎