Models That Prove Their Own Correctness

## Abstract

Abstract How can we trust the correctness of a learned model on a particular input of interest? Model accuracy is typically measured on average over a distribution of inputs, giving no guarantee for any fixed input.
This paper proposes a theoretically-founded solution to this problem: to train Self-Proving models that prove the correctness of their output to
a verification algorithm V 𝑉 V italic_V via an Interactive Proof. Self-Proving models satisfy that, with high probability over an input sampled from a given distribution, the model generates a correct output and successfully proves its correctness to V 𝑉 V\! italic_V . The soundness property of V 𝑉 V italic_V guarantees that, for every input, no model can convince V 𝑉 V italic_V of the correctness of an incorrect output. Thus, a
Self-Proving model proves correctness of most of its outputs, while all incorrect outputs (of any model) are detected by V 𝑉 V italic_V . We devise a generic methods for learning
Self-Proving models, and prove its
convergence under certain assumptions. The theoretical framework and results are complemented by experiments on an arithmetic capability:
computing the greatest common divisor (GCD) of two integers. Our learning method is used to train a Self-Proving transformer that computes the GCD and proves the correctness of its answer.

## 1 Introduction

Bob is studying for his algebra exam and stumbles upon a question $Q$ that he cannot solve. He queries a Large Language Model (LLM) for the answer, and it responds with a number: 42. Bob is aware of recent research showing that the LLM attains a 90% score on algebra benchmarks (cf. Frieder et al. ), but should he trust that the answer to his particular question $Q$ is indeed 42?

Bob could ask the LLM to explain its answer in natural language. Though he must proceed with caution, as the LLM might try to convince him of an incorrect answer (Turpin et al., ). Moreover, even if 42 is the correct answer, the LLM may fail to produce a convincing proof (Wang et al., ). If only the LLM could formally prove its answer, Bob would verify the proof and be convinced.

This paper initiates the study of *Self-Proving models* (Fig. 1) that prove the correctness of their answers via an Interactive Proof system (Goldwasser et al., ). Self-Proving models successfully convince a verification algorithm $V$ with *worst-case soundness guarantees*: for any question, $V$ rejects all incorrect answers with high probability over the interaction. This guarantee holds even against provers that have access to $V$’s specification, and unbounded computational power.

Figure: Figure 1: Self-Proving models. For input $x$, Self-Proving model $P_{\theta}$ generates an output $y$ and sends it to a Verification Algorithm $V$. Then, over $i\in[R]$ rounds, $V$ sends query $q_{i}$, and receives an answer $a_{i}$ from $P_{\theta}$. Finally, $V$ decides (“accept/reject”) whether it is convinced that $y$ is a correct output for $x$.
Refer to caption: extracted/5650103/figs/main.png

Our contributions are as follows.

- •
We define Self-Proving models (Section 3).
- •
We propose two methods for learning Self-Proving models in Section 4. The first, *Transcript Learning (TL)*, relies on access to transcripts of accepting interactions and is the focus of this paper; we prove convergence bounds for TL under convexity and Lipschitzness assumptions. The second method, *Reinforcement Learning from Verifier Feedback (RLVF)*, trains a model by emulating interaction with the verifier. We also present variants of these algorithms that use *Annotations* to improve learning in practice.
- •
We empirically study TL and Annotated-TL (ATL) for training Self-Proving transformers that compute the Greatest Common Divisor (GCD) of two integers. Table 2 demonstrates the efficacy of our methods, with additional experiments in Section 5. Our results may be of independent interest for research on the arithmetic capabilities of transformers (e.g. Charton ; Lee et al. ). Code, data and models will be made available upon publication.

#### Scope.

This paper contains a theory of learned models that prove their own correctness via an Interactive Proof system. The fascinating and well-studied question of *which* settings are verifiable in an Interactive Proof system is beyond our scope. Our theory is general in that it pertains to *any* such setting, e.g., any decision problem solvable in polynomial space (Shamir, ). See Goldreich () for a primer on Proof systems more broadly.

**Table 2: Self-Proving transformers computing the GCD. We train a 6.7M parameter GPT to compute the GCD of two integers sampled log-uniformly from $[10^{4}]$. Vanilla GPT correctly generates the GCD for almost all inputs, but does not prove correctness to a simple verification algorithm. GPT trained with Transcript Learning (GPT+TL) proves its answer 60.3% of the time; training with Annotated Transcript Learning (GPT+ATL) increases this to 96.7%. See Section 5 for details.**
| Learning method | Correctness | Verifiability |
| --- | --- | --- |
| GPT (baseline) | $99.8\%$ | - |
| GPT+TL | $98.8\%$ | $60.3\%$ |
| GPT+ATL | $98.6\%$ | $96.7\%$ |

## 2 Related Work

This paper is situated at the intersection of machine learning (ML) theory and Interactive Proof systems (IPs). We briefly discuss recent relevant work from these literatures.

#### ML and IPs.

IPs have found numerous applications in ML towards a diverse set of goals.
Anil et al. () introduce Prover–Verifier Games, a game-theoretic framework for learned provers and verifiers. Wäldchen et al. () cast the problem of model interpretability as a Prover–Verifier interaction between a learned feature selector and a learned feature classifier. Debate systems (Condon et al., ), a multiprover variant of IPs, were considered for aligning models with human values (Irving et al., ; Brown-Cohen et al., ). In such Debate systems, two competing models are each given an alleged answer $y\neq y^{\prime}$, and attempt to prove the correctness of their answer to a (human or learned) judge.
Lastly, Murty et al. () define Pseudointelligence: a model learner $L_{M}$ and an evaluator learner $L_{E}$ are each given samples from a ground-truth; $L_{M}$ learns a model of the ground-truth, while $L_{E}$ learns an evaluator of such models; the learned evaluator then attempts to distinguish between the learned model and the ground-truth in a Turing Test-like interaction.

All of these works consider *learned verifiers*, whereas our work focuses on training models that interact with a manually-defined verifier. More related in this regard is IP-PAC (Goldwasser et al., ), in which a learner proves that she learned a model that is Probably Approximately Correct (Valiant, ). We, however, consider *models* that prove their own correctness on a *per-input basis*, rather than *learners* that prove *average-case correctness* of a model.

#### Models that generate formal proofs.

Self-Proving models are verified by an algorithm with formal completeness and soundness guarantees (see Definition 3.2). In this sense, Self-Proving models generate a formal proof of the correctness of their output. Several works propose specialized models that generate formal proofs.

AlphaGeometry (Trinh et al., ) is capable of formally proving olympiad-level geometry problems; Gransden et al. (); Polu and Sutskever (); Yang et al. () and others train models to produce proofs in Coq, Metamath and Lean (de Moura et al., ); FunSearch (Romera-Paredes et al., ) evolves LLM-generated programs by systematically evaluating their correctness. Indeed, all of these can be cast as Self-Proving models developed for *specific proof systems*. Meanwhile, this work defines and studies the class of such models *in general*. Several works (e.g. Welleck et al. ) consider models that generate natural language proofs or explanations, which are fundamentally different from formal proofs (or provers) verified by an algorithm.

#### Training on intermediate steps.

Chain-of-Though (CoT, Wei et al. ) refers to additional supervision on a model in the form of intermediate reasoning steps. CoT is known to improve model performance whether included in-context (Wei et al., ) or in the training phase itself (Yang et al., ). Transcript Learning (TL, Section 4.1) can be viewed as training the model on a Chain-of-Thought induced by the interaction of a verifier and an honest prover (Definition 3.2).

To complete the analogy, let us adopt the terminology of Uesato et al. (), who consider *outcome supervision* and *process supervision*. In our case, the *outcome* is the decision of the verifier, and the *process* is the interaction between the verifier and the model. Thus, Reinforcement Learning from Verifier Feedback (RLVF, Section 4.2) is outcome-supervised while TL is process-supervised. In a recent work, Lightman et al. () find that process-supervised transformers outperform outcome-supervised ones on the MATH dataset (Hendrycks et al., ).

#### Transformers for arithmetic.

In Section 5 we train and evaluate Self-Proving transformers to generate the GCD of two integers and prove its correctness to a verifier. These experiments leverage a long line of work on neural models of arithmetic tasks originating with Siu and Roychowdhury (). Of particular relevance is the recent paper of Charton (), who trains transformers to generate the GCD—without a proof of correctness. We benefit from conclusions suggested in their work and start from a similar (scaled-down) experimental setup. Our main challenge (obtaining *Self-Proving* models) is overcome by introducing Annotated Transcript Learning (ATL).

We conduct ablation experiments to find two deciding factors in ATL. First, we study the effect of the amount of annotation given in the form of intermediate steps (Lee et al., ), which is related to autoregressive length complexity (Malach, ). Second, we characterize ATL efficacy in terms of an algebraic property of the tokenization scheme (cf. Nogueira et al. ; Charton , ).

## 3 Self-Proving models

We introduce and formally define our learning framework in which models prove the correctness of their output. We start with preliminaries from the learning theory and proof systems literatures in Section 3.1. We then introduce our main definition in Section 3.2.

### 3.1 Preliminaries

Let $\Sigma$ be a set of finite tokens and $\Sigma^{\ast}$ denote the set of finite sequences of such tokens. We consider sequence-to-sequence models $F_{\theta}\colon\Sigma^{\ast}\to\Sigma^{\ast}$, which are total functions that produce an output for each possible sequence. A model is parameterized by a real-valued, finite dimensional vector $\theta$. We consider models as *randomized* functions, meaning that $F_{\theta}(x)$ is a random variable over $\Sigma^{\ast}$, of which samples are denoted by $y\sim F_{\theta}(x)$.

Before we can define models that prove their own correctness, we must first define correctness. Correctness is defined with respect to an input distribution $\mu$ over $\Sigma^{\ast}$, and a ground-truth $F^{\ast}$ that defines correct answers.
For simplicity of presentation, we focus on the case that each input $x\in\Sigma^{\ast}$ has exactly one correct output $F^{\ast}(x)\in\Sigma^{\ast}$, and a zero-one loss function on outputs (the general case is left for future work). The fundamental goal of machine learning can be thought of as learning a model of the ground truth $F^{\ast}$. Formally,

###### Definition 3.1 (Correctness) .

Let $\mu$ be a distribution of input sequences in $\Sigma^{\ast}$ and let $F^{\ast}\colon\Sigma^{\ast}\to\Sigma^{\ast}$ be a fixed (deterministic) ground-truth function. For any $\alpha\in[0,1]$, we say that model $F_{\theta}$ is $\alpha$-correct (with respect to $\mu$) if

$$ $\Pr_{\begin{subarray}{c}x\sim\mu\\ y\sim F_{\theta}(x)\end{subarray}}[y=F^{\ast}(x)]\geq\alpha.$ $$

An *interactive proof system* (Goldwasser et al., ) is a protocol carried out between an efficient *verifier* and a computationally unbounded *prover*. The prover attempts to convince the verifier of the correctness of some assertion, while the verifier accepts only correct claims. The prover is powerful yet untrusted; in spite of this, the verifier must reject false claims with high probability.

In the context of this work, it is important to note that the verifier is *manually-defined* (as opposed to learned). Formally, the verifier is a probabilistic polynomial-time algorithm tailored to a particular ground-truth capability $F^{\ast}$. Informally, the verifier is the anchor of trust: think of the verifier as an efficient and simple algorithm, hosted in a trustworthy environment.

Given an input $x\in\Sigma^{\ast}$, the model $F_{\theta}$ “claims” that $y\sim F_{\theta}(x)$ is correct. We now define what it means to *prove* this claim. We will use $P_{\theta}$ to denote Self-Proving models, noting that they are formally the same object(^1^11Both are randomized mappings from $\Sigma^{\ast}$ to $\Sigma^{\ast}$.) as non-Self-Proving (“vanilla”) models $F_{\theta}$. This notational change is to emphasize that $P_{\theta}$ first outputs $y\sim P_{\theta}(x)$ *and is then prompted by the verifier*, unlike $F_{\theta}$ who only generates an output $y\sim F_{\theta}(x)$.

A Self-Proving model proves that $y\sim P_{\theta}(x)$ is correct to a verifier $V$ over the course of $R$ rounds of interaction (Figure 1). In each round $i\in[R]$, verifier $V$ queries $P_{\theta}$ on a sequence $q_{i}\in\Sigma^{\ast}$ to obtain an answer $a_{i}\in\Sigma^{\ast}$; once the interaction is over, $V$ accepts or rejects. For fixed $x,y\in\Sigma^{\ast}$, the decision of $V$ after interacting with $P_{\theta}$ is a random variable over $V$’s decision (accept/reject), determined by the randomness of $V$ and $P_{\theta}$. The decision random variable is denoted by $\left<V,P_{\theta}\right>(x,y)$.

We present a definition of Interactive Proofs restricted to our setting.

###### Definition 3.2 .

Fix a soundness error $s\in(0,1)$, a finite set of tokens $\Sigma$ and a ground truth $F^{\ast}\colon\Sigma^{\ast}\to\Sigma^{\ast}$. A *verifier $V$ (in an Interactive Proof) for $F^{\ast}$* is a probabilistic polynomial-time algorithm that is given explicit inputs $x,y\in\Sigma^{\ast}$ and black-box (oracle) query access to a prover $P$.(^2^22We intentionally write $P$ rather than $P_{\theta}$: Interactive Proofs are defined with respect to all possible provers, not just parameterized ones.) It *interacts* with $P$ over $R$ rounds (see Figure 1) and outputs a decision $\left<V,P\right>(x,y)\in\{0,1\}$. Verifier $V$ satisfies the following two guarantees:

- •
*Completeness:* There exists an *honest prover* $P^{\ast}$ such that, for all $x\in\Sigma^{\ast}$,
$\Pr[\left<V,P^{\ast}\right>\!(x,F^{\ast}(x))\ \mathrm{accepts}]=1,$
where the probability is over the randomness of $V$.(^3^33WLOG, the honest prover is deterministic by fixing the optimal randomness of a randomized prover.)
- •
*Soundness:* For all $P$ and for all $x,y\in\Sigma^{\ast}$, if $y\neq F^{\ast}(x)$ then
$\Pr[\left<V,P\right>(x,y)\ \mathrm{accepts}]\leq s,$
where the probability is over the randomness of $V$ and $P$, and $s$ is the soundness error.

###### Remark 3.3 (Verifier efficiency) .

Definition 3.2 requires that $V$ is a polynomial-time algorithm whereas provers are unbounded. This captures a requirement for *efficient verification*. We chose polynomial time as a measure of efficiency because it is common Proof systems literature. That said, one could adapt Definition 3.2 to fit alternative efficiency measures, such as space complexity (Condon and Lipton, ) or circuit depth (Goldwasser et al., ). Regardless of which measure is taken, to avoid a trivial definition it is crucial that $V$ should be more efficient than the honest prover $P^{\ast}$; else, $V$ can simply execute $P^{\ast}$ to perform the computation itself.

By definition, the soundness error $s$ of a verifier $V$ bounds the probability that it is mistakenly convinced of an incorrect output; in that sense, the smaller $s$, the “better” the verifier $V$. In our setting, we think of a manually-defined verifier $V$ who is formally proven (by a human) to have a small soundness error by analysis of $V$’s specification.

As depicted in Figure 1, each of the model’s answers depends on all previous queries and answers in the interaction. This captures the setting *stateful models*, e.g. a session with a chatbot.

Towards defining Self-Proving models (Section 3.2), let us observe the following. Completeness and soundness are *worst-case guarantees*, meaning that they hold for all possible inputs $x\in\Sigma^{\ast}$. In particular, completeness implies that for all $x\in\Sigma^{\ast}$, the honest prover $P^{\ast}$ convinces $V$ of the correctness of $F^{\ast}(x)$; in classical proof systems there is no guarantee that an “almost honest” prover can convince the verifier (cf. Paradise ()). Yet, if we are to *learn* a prover $P_{\theta}$, we cannot expect it to agree with $P^{\ast}$ perfectly, nor can we expect it to always output $F^{\ast}(x)$. Indeed, Self-Proving models will have a *distributional guarantee* with respect to inputs $x\sim\mu$.

###### Definition 3.1 (Correctness) .

###### Definition 3.2 .

###### Remark 3.3 (Verifier efficiency) .

### 3.2 Self-Proving models

We define the *Verifiability* of a model $P_{\theta}$ with respect to an input distribution $\mu$ and a verifier $V$. Intuitively, Verifiability captures the ability of the model to prove the correctness of its answer $y\sim P_{\theta}(x)$, when the input $x$ is sampled from $\mu$. We call models capable of proving their own correctness as *Self-Proving models*.

###### Definition 3.4 (Self-Proving model) .

Fix a verifier $V$ for a ground-truth $F^{\ast}\colon\Sigma^{\ast}\to\Sigma^{\ast}$ as in Definition 3.2, and a distribution $\mu$ over inputs $\Sigma^{\ast}$. The *Verifiability* of a model $P_{\theta}\colon\Sigma^{\ast}\to\Sigma^{\ast}$ is defined as

$$ $\mathrm{ver}_{V,\mu}(\theta)\coloneqq\Pr_{\begin{subarray}{c}x\sim\mu\\ y\sim P_{\theta}(x)\end{subarray}}\left[\left<V,P_{\theta}\right>(x,y)\ \mathrm{accepts}\right].$ (1) $$

We say that model $P_{\theta}$ is *$\beta$-Self-Proving* with respect to $V$ and $\mu$ if $\mathrm{ver}_{V,\mu}(\theta)\geq\beta$.

###### Remark 3.5 (Verifiability $\implies$ correctness) .

Notice that the ground-truth $F^{\ast}$ does not appear in Definition 3.4 except for the first sentence. Indeed, once it is established that $V$ is a verifier for $F^{\ast}$ (as per Definition 3.2), then Verifiability w.r.t $V$ implies correctness w.r.t $F^{\ast}$: Consider any input distribution $\mu$, ground-truth $F^{\ast}$, and a verifier $V$ for $F^{\ast}$ with soundness error $s$. By a union bound, if model $P_{\theta}$ is $\beta$-Verifiable, then it is $(\beta-s)$-correct. That is to say, Verifiability is formally a stronger guarantee than correctness when $V$ has small soundness error $s$.

As depicted in Figure 1, a Self-Proving model $P_{\theta}$ plays a dual role: first, it generates an output $y\sim P_{\theta}(x)$, and then it proves the correctness of this output to $V$. Note also that Self-Provability is a feature of a *model*, unlike completeness and soundness which are features of a *verifier* (see Table 1).

The benefit of Verifiability over correctness is captured by the following scenario. Alice wishes to use a model $P_{\theta}$ to compute some functionality $F^{\ast}$ on an input $x_{0}$ in a high risk setting. Alice generates $y_{0}\sim P_{\theta}(x_{0})$. Should Alice trust that $y_{0}$ is correct? If Alice has a held-out set of labeled samples, she can estimate $P_{\theta}$’s average correctness on $\mu$. Unfortunately, (average) correctness provides no guarantee regarding for the correctness of the particular $(x_{0},y_{0})$ that Alice has in hand. If, however, Alice has access to a verifier $V$ for which $P_{\theta}$ is Self-Proving, then she can trust the model on an input-by-input (rather than average-case) basis: Alice can execute $V$ on $(x_{0},y_{0})$ and black-box access to $P_{\theta}$. Soundness of $V$ guarantees that if $y_{0}$ is incorrect, then $V$ rejects with high probability, in which case Alice should either generate $P_{\theta}(x_{0})$ again—or find a better model.

###### Definition 3.4 (Self-Proving model) .

###### Remark 3.5 (Verifiability ⟹ \implies ⟹ correctness) .

## 4 Learning Self-Proving Autoregressive Models

With a sound verifier $V$ at hand, obtaining Self-Proving models with respect to $V$ holds great promise: a user that prompts the model with input $x$ does not need to take it on good faith that $P_{\theta}(x)$ is correct; she may simply verify this herself by executing the verification protocol.
How, then, can we learn models that are not just approximately-correct, but Self-Proving as well?

The challenge is to align the model with
a verifier. We assume that the learner has access to input samples $x\sim\mu$ and correct outputs $F^{\ast}(x)$, as well as the verifier specification (code). Additionally, the learner can emulate the verifier, as the latter is computationally efficient (Remark 3.3).

Our focus is on autoregressive sequence-to-sequence (Self-Proving) models $P_{\theta}$ (Elman, ). Such models generate their output by recursively prompting a randomized sampling from a base distribution $p_{\theta}$ over tokens $\Sigma$. For an input $z\in\Sigma^{\ast}$, the output $w\sim P_{\theta}(z)$ is generated as follows:

- •
Sample $w_{1}\sim p_{\theta}(z)$.
- •
Let $j=1$. While $w_{j}$ is not the end-of-sequence token $\mathtt{EOS}\in\Sigma^{\ast}$:
–
Sample $w_{j+1}\sim p_{\theta}(zw_{1}\cdots w_{j})$.
- •
Output $w=w_{1}w_{2}\cdots w_{j}$.

For any $z\in\Sigma^{\ast}$, it is useful to consider the vector of log-proabilities over $\Sigma$, denoted by $\log p_{\theta}(z)\in\mathbb{R}^{|\Sigma|}$. We assume that each coordinate in this vector is differentiable with respect to $\theta$.

Our general approach is inspired by Reinforcement Learning from Human Feedback (Christiano et al., ), a method for aligning models with human preferences, which has recently been used to align sequence-to-sequence models (Ouyang et al., ).
However, there are two important differences between humans and algorithmic verifiers: (1) Verifiers are efficient algorithms which may be emulated by the learner. This is unlike humans, whose preferences are costly to obtain. On the other hand, (2) verifiers make a single-bit decision at the end of an interaction, but cannot guide the prover (model) in intermediate rounds. In RL terms, this is known as the *exploration problem* for sparse reward signals (e.g. Ladosz et al. ).

Section 4.1 introduces *Transcript Learning* (TL), a learning algorithm that overcomes the exploration problem mentioned in the second point under the assumption that the learner has access to transcripts of interactions in which the verifier accepts. We prove convergence bounds for TL (Section A.1) and analyze it experimentally (Section 5).

Access to accepting transcripts is a reasonable assumption, for example, when there is an efficient honest prover that can generate such transcripts (Goldwasser et al., ). When there is no access to accepting transcripts, we propose *Reinforcement Learning from Verifier Feedback* (Section 4.2).

### 4.1 Transcript Learning

We present an algorithm for learning Self-Proving models which uses access to a distribution of accepting transcripts. This is a reasonable assumption to make when the honest prover $P^{\ast}$ (see Definition 3.2) is efficient, as in the case in Doubly-Efficient Interactive Proof systems as defined by Goldwasser et al. () and developed in other theoretical (e.g. Goldreich and Rothblum ) and applied (e.g. Zhang et al. ) works. In this case, an honest prover $P^{\ast}$ can be run by the learner during training to collect accepting transcripts without incurring heavy computational cost.

The intuition behind Transcript Learning is that the interaction of the verifier and prover can be viewed as a sequence itself, which is called the *transcript* $\pi\in\Sigma^{\ast}$. The idea is to learn a model not just of $x\mapsto y^{\ast}$ for a correct output $y^{\ast}$, but of $x\mapsto y^{\ast}\pi^{\ast}$, where $\pi^{\ast}$ is a transcript of an interaction in which the verifier accepted.

In more detail, Transcript Learning requires access to an *(honest) transcript generator* $\mathcal{T}^{\ast}$. Given an input $x$, the generator $\mathcal{T}^{\ast}(x)$ samples a sequence $P^{\ast}\!(x)\pi^{\ast}\in\Sigma^{\ast}$ such that $\pi^{\ast}$ is an accepted transcript. The generator is autoregressive, meaning that for any prefix of an accepted transcript $\pi^{\ast}_{\leq t}\in\Sigma^{t}$, the learner has access to the distribution over next tokens $\mathcal{T}^{\ast}(\pi_{\leq t})\in\Sigma$.(^4^44Formally, if the generator is prompted with any string that cannot be completed to an accepted transcript, it outputs a dummy symbol $\bot\in\Sigma$.)

Transcript Learning (TL) trains a Self-Provable model by autoregressively optimizing towards generating accepting transcripts. It is described in Algorithm 1. At a very high level, it works by repeatedly sampling $x\sim\mu$ and transcript $y^{\ast}\pi^{\ast}\sim\mathcal{T}^{\ast}(x)$, and updating the logits $\log p_{\theta}$ towards agreeing with $y^{\ast}\pi^{\ast}$ via Gradient Ascent.
We prove that, under certain conditions, it is expected to output a Self-Provable model.

###### Theorem 4.1 ( Theorem A.5 , informal) .

Fix an input distribution $\mu$, a verifier $V$, a transcript generator $\mathcal{T}^{\ast}$, an autoregressive model family $\{P_{\theta}\}_{\theta}$ parameterized by $\theta\in\mathbb{R}^{d}$ for some $d\in\mathbb{N}$, and a norm $||\cdot||$ on $\mathbb{R}^{d}$. Assume that the *agreement function* $A\colon\mathbb{R}^{d}\to[0,1]$ defined by

$$ $A(\theta)\coloneqq\Pr_{\begin{subarray}{c}x\sim\mu\\ {\pi^{\ast}\sim\mathcal{T}^{\ast}(x)}\end{subarray}}[\mathrm{Transcript}(\left <V,P_{\theta}\right>(x))=\pi^{\ast}]$ $$

is concave and differentiable in $\theta$. For any $\varepsilon>0$, let $B_{\mathrm{Norm}}$, $B_{\mathrm{Lip}}$ and $C$ be upper-bounds such that the following conditions hold.

- •
There exists $\theta^{\ast}\in\mathbb{R}^{d}$ with $||\theta^{\ast}||<B_{\mathrm{Norm}}$ such that $A(\theta^{\ast})\geq 1-\varepsilon/2$.
- •
For all $\theta$, the logits of $P_{\theta}$ are $B_{\mathrm{Lip}}$-Lipschitz in $\theta$.
- •
The total number of tokens sent by the prover to the verifier $V$ in any interaction is at most $C$.

Denote by $\bar{\theta}$ the output of TL running for number of iterations

$$ $N\geq 4\cdot C^{2}\cdot\frac{B_{\mathrm{Norm}}^{2}\cdot B_{\mathrm{Lip}}^{2}}{ \varepsilon^{2}}$ (2) $$

and learning rate $\lambda=B_{\mathrm{Norm}}/CB_{\mathrm{Lip}}\sqrt{N}$. Then the expected Verifiability of $\bar{\theta}$ is at least $1-\varepsilon$.

The proof (Appendix A) goes by reduction to Stochastic Gradient Descent (SGD). We show that the learner can use only its available tools—sampling honest transcripts, emulating the verifier, and differentiating the logits—to estimate the agreement gradient $\nabla A(\theta)$. Since the agreement $A(\theta)$ lower bounds the Verifiability of $P_{\theta}$, the former can be used as a surrogate objective for the latter.

The conditions for Theorem 4.1 can be split into two. First, the standard conditions used to prove SGD convergence: convexity,(^5^55Theorem 4.1 requires concavity because it guarantees maximization, rather than minimization. We leave it for future work to relax the differentiability assumption.) $B_{\mathrm{Norm}}$-boundedness, and $B_{\mathrm{Lip}}$-Lipschitzness. Second, there is a bound $C$ on the *communication complexity* of the prover in the Interactive Proof system.

Quantitatively, the efficiency of TL is captured by the *number of iterations* $N$. It is desirable to minimize $N$, which is also the *number of samples* needed from the distribution $\mu$ and the transcript generator $\mathcal{T}^{\ast}$. Like the conditions on the theorem, the bound on $N$ can too be decomposed into two factors: The right factor is the complexity of SGD ($B_{\mathrm{Norm}}^{2}B_{\mathrm{Lip}}^{2}/\varepsilon^{2}$), and the left factor $O(C^{2})$ is the communication complexity of the proof system. Minimizing communication complexity has been an overarching goal in the study of proof systems (e.g. Goldreich and Håstad ; Goldreich et al. ; Reingold et al. ). Theorem 4.1 formally shows the benefit of communication-efficient proof systems in the context of Self-Proving models.

###### Theorem 4.1 ( Theorem A.5 , informal) .

### 4.2 Reinforcement Learning from Verifier Feedback (RLVF)

As mentioned in Section 4.1, Transcript Learning uses access to an honest transcript generator to estimate gradients of (a lower bound on) the Verifiability of a model $P_{\theta}$.

*Reinforcement Learning from Verifier Feedback (RLVF, Algorithm 2)* estimates this gradient without access to a transcript generator. RLVF can be viewed as a modification of TL in which the learner emulates the interaction of the verifier with its own model $P_{\theta}$. Rather than directly sampling from the generator as in TL, it collects accepting transcripts by rejection sampling on emulated transcripts.

This rejection sampling means that RLVF requires its initial model $P_{\theta_{0}}$ to have Verifiability bounded away from 0, so that accepting transcripts are sampled with sufficient probability. Fortunately, such a Self-Proving base model can be learned using TL. This gives a learning paradigm in which a somewhat-Self-Proving base model is first learned with TL (with Verifiability $\delta>0$), and then “amplified” to a fully Self-Proving model using RLVF (cf. Nair et al. ).

We prove that RLVF learner can estimate the Verifiability gradient of $P_{\theta}$ using emulation alone in Lemma A.6.
From a broader perspective, RLVF can be derived by viewing Self-Proving as a reinforcement learning problem in which the agent (prover) is rewarded when the verifier accepts. Indeed, RLVF is the Policy Gradient method (Sutton et al., ) for a verifier-induced reward. Convergence bounds for Policy Gradient methods are a challenging and active area of research (e.g. Agarwal et al. ), and so we leave the full analysis to future work.

### 4.3 Learning from annotated transcripts

To minimize the length of messages exchanged in an Interactive Proof system, the honest prover is designed to send the shortest possible message to the verifier, containing only essential information.

However, when training Self-Proving model, it may be useful for it to first generate an “annotated” answer $\widetilde{a}$ which is then trimmed down to the actual answer $a$ to be sent to the verifier. We adapt Sections 3 and 4 to this setting in Appendix C, where we present *Annotated Transcripts*. This can be viewed as adding Chain-of-Thought (Wei et al., ) to the model. The Transcript Learning algorithm naturally extends to annotated transcripts as well.

## 5 Experimental Results

We describe our experimental setup, and present ablation studies that shed additional light on the effect of *annotation* and *representation* on Verifiability.

### 5.1 Setup: Training transformers to predict the GCD of two integers

Charton () empirically studies the power and limitations of learning GCDs with transformers. We follow their setup and two conclusions on settings that make for faster learning: Training from the log-uniform distribution, and choosing a base of representation with many prime factors.

We fix a base of representation $B=210$ and use $\mathbf{x}$ to denote an integer $x$ encoded as a $B$-ary string.(^6^66$B=210$ is chosen following Charton () to be an integer with many prime factors.) For sequences of integers, we write $\mathbf{(x_{1}x_{2})}$ to denote the concatenation of $\mathbf{x_{1}}$ with $\mathbf{x_{2}}$, delimited by a special token. The vocabulary size is needed for this representation is $|\Sigma|\approx 210$.

We choose the input distribution $\mu$ to be the log-uniform distribution on $[10^{4}]$, and train the transformer on sequences of the form $\mathbf{(x_{1}x_{2}y)}$, where $x_{1},x_{2}\sim\mu$ and $y=GCD(x_{1},x_{2})$.
This is a scaling-down of Charton (), to allow single GPU training of Self-Proving transformers. In all of our experiments, we use a GPT model (Vaswani et al., ) with 6.3M parameters trained on a dataset of 1024K samples in batches of 1024. Full details are deferred to Appendix E.

#### Proving correctness of GCD.

Following Charton () as a baseline, we find that transformers can correctly compute the GCD with over $99\%$ probability over $(x_{1},x_{2})\sim\mu$. To what extent can they *prove* their answer? To answer this question, we first devise a natural proof system based on Bézout’s theorem. Its specification and formal guarantees are deferred to Appendix D. We denote its verification algorithm by $V$, and highlight some important features of the experimental setup:

- •
The proof system consists of one round ($R=1$). The verifier makes no query, and simply receives a proof $\mathbf{\pi}$ from the prover.
- •
*Completeness:* For any $x_{1},x_{2},y\in[10^{4}]$ such that $y=GCD(x_{1},x_{2})$, there exists a proof $\mathbf{\pi}$ such that $V(\mathbf{x_{1}x_{2}y\pi})$ accepts. As detailed in Appendix D, the proof $\pi$ consists of a pair of integers who are *Bézout coefficients* for $x_{1},x_{2}$.
- •
*Soundness:* If $y\neq GCD(x_{1},x_{2})$, then $V(\mathbf{x_{1}x_{2}y\pi})$ rejects for any alleged proof $\mathbf{\pi}\in\Sigma^{\ast}$.

To measure Verifiability, we train a Self-Proving transformer using Transcript Learning on sequences $\mathbf{(x_{1}x_{2}y\pi)}$ and estimate for how many inputs $x_{1},x_{2}\sim\mu$ does the model generate both the correct GCD $\mathbf{y}$ and a valid proof $\mathbf{\pi}$. We test on 1000 pairs of integers $x_{1}^{\prime},x_{2}^{\prime}\sim\mu$ held-out of the training set, prompting the model with $\mathbf{(x_{1}^{\prime}x_{2}^{\prime})}$ to obtain $\mathbf{(y^{\prime}\pi^{\prime})}$, and testing whether $V(\mathbf{x_{1}^{\prime}x_{2}^{\prime}y^{\prime}\pi^{\prime}})$ accepts.

Table 2 on the second page of this paper shows that Transcript Learning for 100K iterations ($\approx\!$100M samples) results in a Self-Proving transformer that correctly proves 60.3% of its answers; there is an additional 38.5% answers which are correct, but the transformer fails to generate an accepted proof. Annotated Transcript Learning all but closes this gap, proving 96.7% of its answers. We further investigate the effect of annotations next.

### 5.2 Models generalize beyond annotations

Figure: Figure 2: Verifiability with increasing amounts of annotation. $T$ is the number of steps added in Annotated Transcript Learning. Dashed lines indicate *Euclidean depth*, that bound the Verifiability of models that prove *only* for integers up to a certain number of steps. Each $T$ was run with three seeds, with mean $\pm$ standard error depicted.
Refer to caption: x1.png

The proof $\mathbf{\pi}$ is annotated by including intermediate steps in its computation. Details are deferred to Appendix D;
roughly speaking, we observe that the proof $\mathbf{\pi}$ for input $\mathbf{(a,b)}$ is obtained as the last element in a sequence $\mathbf{a,b,\pi_{1},\pi_{2},\dots}$ computed by the Euclidean algorithm.
We annotate the proof $\mathbf{\pi}$ by prepending to it the sequence of *Euclidean steps* $\mathbf{(\pi_{1},\dots,\pi_{T})}$ up to some fixed cutoff $T$.

Figure 2 shows how $T$ affects the Verifiability of the learned model. As suggested by Lee et al. (), training the model on more intermediate steps results in better performance; in our case, increasing the number of intermediate steps $T$ yields better Self-Proving models.
One might suspect that models only learn to execute the Euclidean algorithm in-context. To rule out this hypothesis, we derive an upper bound on the possible efficacy of such limited models. This bound is based on the *Euclidean depth* of integers $(x_{1},x_{2})$, which we define as the number of intermediate steps that the Euclidean algorithm makes before terminating on input $(x_{1},x_{2})$. Indeed, a model that only learns the to compute (in-context) the simple arithmetic of the Euclidean algorithm would only be able to prove the correctness of inputs $(x_{1},x_{2})$ whose depth does not exceed the annotation cutoff $T$.

Figure 2 tells a different story: For each cutoff $T$, we estimate the probability that integers $x_{1},x_{2}\sim\mu$ have Euclidean depth at most $T$ on $10^{5}$ sampled pairs. Larger annotation cutoff $T$ increases Verifiability, but all models exceed their corresponding Euclidean depth bound.

### 5.3 Base of representation

Figure: Figure 3: The number of prime divisors of a base $\omega(B)$ determines Verifiability. For each $o\in[4]$, we sampled 17 bases $B\in\{2,\dots,1386\}$ such that $\omega(B)=o$. A Self-Proving transformer was trained via Transcript Learning for twenty epochs on an identical dataset of 1024K samples encoded in base $B$. For each $\omega(B)$ we depict the mean $\pm$ standard error.
Refer to caption: extracted/5650103/figs/bases.png

As mentioned previously, Charton () concludes that, for a given base of representation $B$, transformers correctly compute the GCD of integers $x_{1},x_{2}$ that are products of primes dividing $B$. Simply put, choosing a base $B$ with many different prime factors yields models with better correctness (accuracy), which suggests why base $B=210=2\cdot 3\cdot 5\cdot 7$ yielded the best results.

To test whether the factorization of $B$ has a similar effect on Verifiability as well, we train transformers on 68 bases varying the number of prime divisors $\omega(B)$ from $\omega(B)=1$ (i.e., $B$ is a prime power) to $\omega(B)=4$. Figure 3 shows that $\omega(B)$ correlates not just with correctness (Charton, ), but also with Verifiability. Although the finding is statistically significant (no overlapping error margins), the overall difference is by a few percentage points; we attribute this to the smaller (10%) number of samples on which models were trained, relative to our other experiments.

## 6 Conclusions

Trust between a learned model and its user is fundamental. In recent decades, Interactive Proofs (Goldwasser et al., ) have emerged as a general theory of trust established via verification algorithms. This work demonstrates that models can learn to formally prove their answers in an Interactive Proof system. We call models that possess this capability *Self-Proving*.

The definition of Self-Proving models forms a bridge between the rich theory of Interactive Proofs and the contemporary topic of Trustworthy ML. Interactive Proofs offer formal *worst-case soundness guarantees*; thus, users of Self-Proving models can be confident when their models generate correct answers—and detect incorrect answers with high probability.

We demonstrate the theoretical viability of our definition with two generic learning algorithms: Transcript Learning (TL) and Reinforcement Learning from Verifier Feedback (RLVF). The analyses of these algorithms is informed by techniques from theories of learning, RL, and computational complexity. This work can be extended in several directions: finding conditions for the convergence of RLVF, improving sample complexity bounds for TL, or designing altogether different learning algorithms (for example, by taking advantage of properties of the verifier).

To better understand the training dynamics of (Annotated) TL, we train Self-Proving transformers for the Greatest Common Divisor (GCD) problem.
We train a small (6.3M parameter) transformer that learns to generate correct answers *and proofs* with high accuracy. Facing forward, we note that Interactive Proofs exist for capabilities far more complex than the GCD (Shamir, ); scaling up our experiments is the next step towards bringing Self-Proving models from theory to practice.

## Acknowledgments

We are grateful to Micah Carroll and Avishay Tal for their helpful comments. This research was supported by DARPA-TA1 under grant no. HR001119S0076, and by the Simons Collaboration on the Theory of Algorithmic Fairness.

## Appendix A Theoretical analyses for Section 4

In this section we provide a formal description and analysis of Transcript Learning (TL, Section 4.1) and Reinforcement Learning from Verifier Feedback (RLVF, Section 4.2). In Section A.1 we prove a convergence theorem for TL under convexity and Lipschitzness assumptions. Obtaining an analogous result for RLVF is more challenging; in lieu of a full analysis, we provide a lemma showing that the gradients estimated in the algorithm approximate the Verifiability of the model in Section A.2.

#### Specification of the learning model.

We must first fully specify the theoretical framework in which our results reside. Continuing from Section 3, we define a *learner* as an algorithm $\Lambda$ with access to a family of autoregressive models $\{P_{\theta}\}_{\theta}$ and samples from the input distribution $x\sim\mu$. In our setting of Self-Proving models (and in consistence with the Interactive Proofs literature), we give the learner the full specification of the verifier $V$. More formally,

###### Definition A.1 (Self-Proving model learner) .

A *(Self-Proving model) learner* is a probabilistic oracle Turing Machine $\Lambda$ with the following access:

- •
A family of *autoregressive models* $\{P_{\theta}\}_{\theta\in\mathbb{R}^{d}}$ where $d\in\mathbb{N}$ is the number of parameters in the family. Recall (Section 4) that for each $\theta$ and $z\in\Sigma^{\ast}$, the random variable $P_{\theta}(z)$ is determined by the logits $\log p_{\theta}(z)\in\mathbb{R}^{|\Sigma|}$. For any $z\in\Sigma^{\ast}$ and $\sigma\in\Sigma$, the learner $\Lambda$ can compute the gradient of the $\sigma^{\text{th}}$ logit, that is, $\nabla_{\theta}\log\Pr_{\sigma^{\prime}\sim p_{\theta}(z)}[\sigma=\sigma^{
\prime}]$.
- •
Sample access to a the *input distribution* $\mu$. That is, $\Lambda$ can sample $x\sim\mu$.
- •
The full specification of the verifier $V$, i.e., the ability to emulate the verification algorithm $V$. More specifically, $\Lambda$ is able to compute $V$’s decision after any given interaction; that is, given input $x$, output $y$, and a sequence of queries and answers $(q_{i},a_{i})_{i=1}^{R}$, the learner $\Lambda$ can compute the decision of $V$ after this interaction.

We remark that analysis of Transcript Learning will require a slight strengthening of the final item above. This is discussed in Section A.1.

Throughout this section, we will refer to the *transcript* of an interaction between a verifier and a prover (see Figure 1). We will this transcript by $\pi=(y,q_{1},a_{1},\dots,q_{R},a_{R})$, and for any index $s\in|\pi|$ we will write $\pi_{<s}\in\Sigma^{s-1}$ to denote the $s$-long prefix of $\pi$.

###### Definition A.1 (Self-Proving model learner) .

### A.1 Transcript Learning

Recall that Transcript Learning requires access to an *honest transcript generator*. Before we can formally define this object, it will be useful to define a *query generator* for a verifier $V$.

###### Definition A.2 (Query generator) .

Fix a verifier $V$ in a proof system with $R\in\mathbb{N}$ rounds, where the verifier issues queries of length $L_{q}=|q_{i}|$ and the prover (model) responses with answers of length $L_{a}=|a_{i}|$.(^7^77We can assume that queries (resp. answers) all have the same length by padding shorter ones.)
The *query generator* $V_{q}$ corresponding to $V$ takes as input a partial interaction and samples from the distribution over next queries by $V$. Formally, for any $r\leq R$, given input $x$, output $y$, and partial interaction $(q_{i},a_{i})_{i=1}^{r}$, $V_{q}(x,y,q_{1},a_{1},\dots,q_{r},a_{r})$ is a random variable over $\Sigma^{L_{q}}$.(^8^88For completeness’ sake, we can say that when prompted with any sequence $z$ that does not encode an interaction, $V_{q}(z)$ is fully supported on a dummy sequence $\bot\cdots\bot\in\Sigma^{L_{q}}$.)

We assume that access to the verifier specification (Definition A.1) includes access to the query generator. After all, the verifier—who is assumed to be efficient—samples from $V_{q}$ during the interaction. Moreover, we will assume that for any partial interaction and any sequence $q^{\prime}$, the learner is able to compute the probability that $q^{\prime}$ was the next query. In other words, we assume the learner can compute the probability density function of $V_{q}$.

A *transcript generator* is a random variable over transcripts that faithfully represents the interaction of the verifier with some prover for a given input. An *honest transcript generator* is one who is fully supported on transcripts accepted by the verifier.

###### Definition A.3 (Honest transcript generator) .

Fix a verifier $V$ in a proof system of $R\in\mathbb{N}$ rounds. A transcript generator $\mathcal{T}_{V}$ for $V$ is a randomized mapping from inputs $x\in\Sigma^{\ast}$ to transcripts $\pi=(y,q_{1},a_{1},\dots,q_{R},a_{R})\in\Sigma^{\ast}$. For any input $x$, $\mathcal{T}_{V}(x)$ satisfies that for each $r\leq R$, the marginal of $\mathcal{T}_{V}(x)$ on the $r^{\text{th}}$ query $q_{r}$ agrees with the corresponding marginal of the query generator $(V_{q})_{r}$.

A transcript generator $\mathcal{T}^{\ast}_{V}\coloneqq\mathcal{T}_{V}$ is *honest* if it is fully supported on transcripts $\pi^{\ast}$ for which the verifier accepts.

Notice that for any verifier $V$, there is a one-to-one correspondence between transcript generators and (possibly randomized) provers. We intentionally chose *not* to specify a prover in Definition A.3 to emphasize that transcripts can be “collected” independently of the honest prover (see completeness in Definition 3.2). As long as the generator is fully supported on honest transcripts, it can be used for Transcript Learning (Algorithm 1 described below).

Figure: Algorithm 1 Transcript Learning (TL)

Convergence of TL is proven by a reduction to Stochastic Gradient Descent (SGD). Essentially, we are tasked with proving that TL estimates a surrogate of the Verifiability-gradient of its model $P_{\theta}$. More precisely, TL estimates the gradient of a function that bounds the Verifiability from below. Maximizing this function therefore maximizes the Verifiability.

The lower-bounding function is the agreement of the transcript generator induced by $P_{\theta}$ with the provided honest transcript generator $\mathcal{T}^{\ast}_{V}$. More formally, we let $\mathcal{T}^{\theta}_{V}$ denote the transcript generator induced by the model $P_{\theta}$: for each $x$, $\mathcal{T}^{\theta}_{V}(x)$ is simply the distribution over transcripts of interactions between $V$ and $P_{\theta}$ on input $x$. We first prove TL correctly estimates the gradient of $A(\theta)$ in its update step.

###### Lemma A.4 (TL gradient estimation) .

Fix an input distribution $\mu$ over $\Sigma^{\ast}$ and a verifier $V$ with round complexity $R$ and answer length $L_{a}$. Fix an honest transcript generator $\mathcal{T}_{V}^{\ast}$.
Let $\theta$ be the parameters of a model $P_{\theta}$ such that

$$ $A(\theta)\coloneqq\Pr_{\begin{subarray}{c}x\sim\mu\\ \pi^{*}\sim\mathcal{T}^{\ast}_{V}(x)\\ \pi\sim\mathcal{T}^{\theta}_{V}(x)\end{subarray}}\left[\pi=\pi^{*}\right]$ $$

is differentiable in $\theta$. Then

$$ $\nabla A(\theta)=\operatorname*{\mathbb{E}}_{\begin{subarray}{c}x\sim\mu\\ \pi^{\ast}\sim\mathcal{T}^{\ast}_{V}\end{subarray}}\left[\alpha_{0}(\theta) \cdot\left(\prod_{\begin{subarray}{c}r\in[R]\\ s\in S(r)\end{subarray}}\beta_{r}(\theta)\cdot\alpha_{s}(\theta)\right)\cdot \sum_{\begin{subarray}{c}r\in[R]\cup\{0\}\\ s\in S(r)\end{subarray}}\vec{d}_{s}(\theta)\right]$ $$

where $S(r)$, $\beta_{r}(\theta)$, $\alpha_{s}(\theta)$ and $\vec{d}_{s}(\theta)$ are as defined in Algorithm 1.

Note that Lemma A.4 is true for *any* model $P_{\theta}$. Moreover, the random vector over which the expectation is taken (in the right hand side) is precisely the direction of the update performed in Algorithm 1. We now prove Lemma A.4, from which we derive Theorem 4.1.

###### Proof.

Throughout this proof, expectations and probabilities will be over the same distributions as in the lemma statement.
First, by the law of total probability, and linearity of the gradient,

$$ $\nabla A(\theta)\coloneqq\nabla_{\theta}\left(\Pr_{x,\pi^{*},\pi}\left[\pi=\pi ^{*}\right]\right)=\nabla_{\theta}\left(\operatorname*{\mathbb{E}}_{x,\pi^{*}} \left[\Pr_{\pi}\left[\pi=\pi^{*}\right]\right]\right)=\operatorname*{\mathbb{E }}_{x,\pi^{*}}\left[\nabla_{\theta}\left(\Pr_{\pi}\left[\pi=\pi^{*}\right] \right)\right].$ $$

Next, we use the law of total probability together with the autoregressive property of $P_{\theta}$ (Section 4) to switch from probabilities on transcripts, to products of next-token probabilities.
Formally, consider any fixed input $x$, honest transcript $\pi^{\ast}=(y^{\ast},q_{1}^{\ast},a_{1}^{\ast},\dots,q_{R}^{\ast},a_{R}^{\ast})$, and denote a random transcript sampled from $\mathcal{T}_{V}^{\theta}(x)$ by $\pi=(y,q_{1},a_{1},\dots,q_{R},a_{R})$. For any $r\in[R]$ denote the random variables $V_{q}^{<r}\coloneqq V_{q}(y,q_{1},a_{1},\dots,q_{r-1},a_{r-1})$ and $\mathcal{T}^{\theta,<r}_{V}\coloneqq\mathcal{T}^{\theta}_{V}(yq_{1}a_{1}\cdots
a
_{r-1}q_{r})$. Then,

$$ $\displaystyle\Pr_{\pi}\left[\pi=\pi^{*}\right]$ $\displaystyle\coloneqq\Pr_{\pi}[(y^{\ast},q_{1}^{\ast},a_{1}^{\ast},\dots,q_{R }^{\ast},a_{R}^{\ast})=(y,q_{1},a_{1},\dots,q_{R},a_{R})]$ (3) $\displaystyle=\Pr_{y\sim P_{\theta}(x)}[y=y^{\ast}]\cdot\prod_{\begin{subarray }{c}r\in[R]\end{subarray}}\Pr_{q\sim V_{q}^{<r}}[q=q_{r}^{\ast}]\cdot\Pr_{a \sim\mathcal{T}^{\theta,<r}_{V}}[a=a_{r}^{\ast}]$ $\displaystyle=\Pr_{y\sim P_{\theta}(x)}[y=y^{\ast}]\cdot\prod_{\begin{subarray }{c}r\in[R]\\ s\in S(r)\end{subarray}}\Pr_{q\sim V_{q}^{<r}}[q=q_{r}^{\ast}]\cdot\Pr_{\sigma \sim p_{\theta}(\pi^{\ast}_{<s})}[\sigma=\pi^{\ast}_{s}]$ (4) $\displaystyle=\alpha_{0}(\theta)\cdot\left(\prod_{\begin{subarray}{c}r\in[R]\\ s\in S(r)\end{subarray}}\beta_{r}(\theta)\cdot\alpha_{s}(\theta)\right),$ (5) $$

where Equation 3 uses independence of the verifier and model’s randomness, Equation 4 uses the autoregressive property of $P_{\theta}$ (Definition A.1), and Equation 5 is by definition of $\alpha_{s}$ and $\beta_{r}$.

Next, a basic calculus identity gives

$$ $\nabla_{\theta}\left(\Pr_{\pi}\left[\pi=\pi^{*}\right]\right)=\Pr_{\pi}\left[ \pi=\pi^{*}\right]\cdot\nabla_{\theta}\log\left(\Pr_{\pi}\left[\pi=\pi^{*} \right]\right).$ (6) $$

Let us focus on the rightmost factor. By Equation 5,

$$ $\displaystyle\nabla_{\theta}\log\left(\Pr_{\pi}\left[\pi=\pi^{*}\right]\right)$ $\displaystyle=\nabla_{\theta}\log\alpha_{0}(\theta)\cdot\left(\prod_{\begin{ subarray}{c}r\in[R]\\ s\in S(r)\end{subarray}}\beta_{r}(\theta)\cdot\alpha_{s}(\theta)\right)$ $\displaystyle=\nabla\log_{\theta}\alpha_{0}(\theta)+\sum_{\begin{subarray}{c}r \in[R]\\ s\in S(r)\end{subarray}}\nabla_{\theta}\log\beta_{r}(\theta)+\nabla_{\theta} \log_{\theta}\alpha_{s}(\theta)$ $\displaystyle=\nabla\log_{\theta}\alpha_{0}(\theta)+\sum_{\begin{subarray}{c}r \in[R]\\ s\in S(r)\end{subarray}}\nabla_{\theta}\log_{\theta}\alpha_{s}(\theta)$ (7) $\displaystyle=\sum_{\begin{subarray}{c}r\in[R]\cup\{0\}\\ s\in S(r)\end{subarray}}\nabla_{\theta}\log_{\theta}\alpha_{s}(\theta)=\sum_{ \begin{subarray}{c}r\in[R]\cup\{0\}\\ s\in S(r)\end{subarray}}\vec{d}_{s}(\theta)$ (8) $$

where Equation 7 is because $\log\beta_{r}(\theta)\coloneqq\log\Pr_{q^{\prime}\sim V_{q}(x\pi^{\ast}_{<t})}
[q^{\prime}=q]$ is a constant and therefore has a gradient of zeros, and Equation 8 is by definition of $\vec{d}_{s}(\theta)$.
Combining Equations 5, 6 and 8 concludes the proof.
∎

We are now ready to prove Theorem 4.1. We restate it below in full formality.

###### Theorem A.5 ( Theorem 4.1 , formal) .

Fix a verifier $V$, an input distribution $\mu$, and an autoregressive model family $\{P_{\theta}\}_{\theta\in\mathbb{R}^{d}}$, and a norm $||\cdot||$ on $\mathbb{R}^{d}$. Fix an honest transcript generator $\mathcal{T}^{\ast}_{V}$, and assume that the *agreement function*

$$ $A(\theta)\coloneqq\Pr_{\begin{subarray}{c}x\sim\mu\\ \pi^{*}\sim\mathcal{T}^{\ast}_{V}(x)\\ \pi\sim\mathcal{T}^{\theta}_{V}(x)\end{subarray}}\left[\pi=\pi^{*}\right]$ $$

is concave and differentiable in $\theta$.
For any $\varepsilon>0$, let $B_{\mathrm{Norm}}$, $B_{\mathrm{Lip}}$ and $C$ be upper-bounds such that the following conditions hold.

- •
There exists $\theta^{\ast}\in\mathbb{R}^{d}$ with $||\theta^{\ast}||<B_{\mathrm{Norm}}$ such that $A(\theta^{\ast})\geq 1-\varepsilon/2$.
- •
For all $\theta$, the logits of $P_{\theta}$ are $B_{\mathrm{Lip}}$-Lipschitz in $\theta$. That is,
$\sup_{\begin{subarray}{c}\theta\in\mathbb{R}^{d}\\
z\in\Sigma^{\ast}\end{subarray}}||\nabla_{\theta}\log p_{\theta}(z)||\leq B_{
\mathrm{Lip}}.$
- •
In the proof system defined by $V$, the total number of tokens (over all rounds) is at most $C$.

Denote by $\bar{\theta}$ the output of TL running for number of iterations

$$ $N\geq 4\cdot C^{2}\cdot\frac{B_{\mathrm{Norm}}^{2}\cdot B_{\mathrm{Lip}}^{2}}{ \varepsilon^{2}}$ $$

and learning rate $\lambda=B_{\mathrm{Norm}}/CB_{\mathrm{Lip}}\sqrt{N}$. Then the expected Verifiability (over the randomness of the samples collected by TL) of $\bar{\theta}$ is at least $1-\varepsilon$. That is,

$$ $\operatorname*{\mathbb{E}}_{\bar{\theta}}[\mathrm{ver}_{V,\mu}(\bar{\theta)}] \geq 1-\varepsilon.$ $$

###### Proof.

Our strategy is to cast TL as Stochastic Gradient Ascent and apply B.2.
Let $\varepsilon$, $B_{\mathrm{Norm}}$, $B_{\mathrm{Lip}}$ and $C$ as in the theorem statement be given. Let $\theta^{\ast}$ be such that $A(\theta^{\ast})\geq 1-\varepsilon/2$ and $||\theta^{\ast}||\leq B_{\mathrm{Norm}}$.

First, notice that

$$ $\operatorname*{\mathbb{E}}_{\bar{\theta}}\left[\mathrm{ver}_{V,\mu}(\bar{ \theta})\right]\geq\operatorname*{\mathbb{E}}_{\bar{\theta}}[A(\bar{\theta})],$ $$

This is because, for any $x$ and model $P_{\theta}$, whenever the transcript generated by $\mathcal{T}^{\theta}(x)$ agrees with $\pi^{\ast}$, then the verifier accepts (because $\pi^{\ast}$ is honest). Therefore, to prove the theorem it suffices to show that

$$ $\operatorname*{\mathbb{E}}_{\bar{\theta}}[A(\bar{\theta})]\geq 1-\varepsilon.$ $$

Following the notation in Algorithm 1, in every iteration $i\in[N]$ the norm of the update step is

$$ $\left\lVert\alpha_{0}(\theta_{i})\cdot\left(\prod_{\begin{subarray}{c}r\in[R] \\ s\in S(r)\end{subarray}}\beta_{r}(\theta_{i})\alpha_{s}(\theta_{i})\right) \cdot\sum_{\begin{subarray}{c}r\in[R]\cup\{0\}\\ s\in S(r)\end{subarray}}\vec{d}_{s}(\theta_{i})\right\rVert\\ =\left|\alpha_{0}(\theta_{i})\cdot\prod_{\begin{subarray}{c}r\in[R]\\ s\in S(r)\end{subarray}}\beta_{r}(\theta_{i})\alpha_{s}(\theta_{i})\right| \cdot\left\lVert\sum_{\begin{subarray}{c}r\in[R]\cup\{0\}\\ s\in S(r)\end{subarray}}\vec{d}_{s}(\theta_{i})\right\rVert\\ \leq 1\cdot\sum_{\begin{subarray}{c}r\in[R]\cup\{0\}\\ s\in S(r)\end{subarray}}\left\lVert\vec{d}_{s}(\theta_{i})\right\rVert,$ $$

where the inequality is because $\alpha_{s}(\theta_{i})$ and $\beta_{r}(\theta_{i})$ are probabilities, so $\leq 1$. Continuing, we have

$$ $\sum_{\begin{subarray}{c}r\in[R]\cup\{0\}\\ s\in S(r)\end{subarray}}\left\lVert\vec{d}_{s}(\theta_{i})\right\rVert\leq\sum _{\begin{subarray}{c}r\in[R]\cup\{0\}\\ s\in S(r)\end{subarray}}B_{\mathrm{Lip}}\leq C\cdot B_{\mathrm{Lip}}.$ $$

The first inequality is by definition of $B_{\mathrm{Lip}}$ as an upper-bound on the gradient of $P_{\theta}$’s logits. The second is because, by definition, $C$ is an upper bound on the number of tokens sent by the prover in the proof system, which is exactly the number of terms in the sum: $r$ indexes rounds, and $s$ indexes tokens sent in each round.

To conclude, Lemma A.4 shows that TL samples from a gradient estimator for $A(\theta)$, while the above equation shows that the gradient is upper-bounded by $C\cdot B_{\mathrm{Lip}}$. We can therefore apply B.2 to obtain

$$ $\operatorname*{\mathbb{E}}_{\bar{\theta}}\left[A\left(\bar{\theta}\right) \right]\geq A(\theta^{\ast})-\varepsilon/2\geq(1-\varepsilon/2)-\varepsilon/2= 1-\varepsilon,$ $$

where the inequality is by definition of $\theta^{\ast}$.

∎

###### Definition A.2 (Query generator) .

###### Definition A.3 (Honest transcript generator) .

###### Lemma A.4 (TL gradient estimation) .

###### Proof.

###### Theorem A.5 ( Theorem 4.1 , formal) .

###### Proof.

### A.2 Reinforcement Learning from Verifier Feedback

Our second learning method, Reinforcement Learning from Verifier Feedback (RLVF, Algorithm 2), does not require access to an honest transcript generator. Instead, the learner learns $P_{\theta}$ generates transcripts herself by emulating the interaction of the verifier with the current Self-Proving model $P_{\theta}$. When an accepting transcript is generated, the learner updates the parameters $\theta$ towards generating such transcript.

Figure: Algorithm 2 Reinforcement Learning from Verifier Feedback (RLVF)

Before we continue with formal analysis of Algorithm 2, let us make a few observations.

Firstly, the parameters are updated (line 11) only when an accepting transcript was generated. This means that the learner can first fully generate the transcript (lines 6-7), and then take backwards passes (line 9) only if the transcript was accepted by $V$. This is useful in practice (e.g. when using neural models) as backwards passes are more computationally expensive than forwards passes.

On the other hand, this means that RLVF requires the parameter initialization $\theta_{0}$ to have Verifiability bounded away from 0, so that accepting transcripts are sampled with sufficient probability. Fortunately, such a Self-Proving base model can be learned using TL. This gives a learning paradigm in which a somewhat-Self-Proving base model is learned with TL (with Verifiability $\delta>0$), and then “amplified” to a fully Self-Proving model using RLVF. This can be seen as an adaptation of the method of Nair et al. [] to the setting of Self-Proving models.

Secondly, in comparing Algorithms 1 and 2, we see that the latter (RLVF) does not keep track of the probabilities $\alpha_{s}$ and $\beta_{r}$. This is because, in RL terms, RLVF is an *on-policy* algorithm; it generates transcripts using the current learned model, unlike TL which samples them from a distribution whose parameterization is unknown to the learner. Hence, the update step in RLVF is simpler than TL. Furthermore, the RLVF learner does not require access to the density function of the query generator $V_{q}$ (Definition A.2) unlike its TL counterpart.

We now prove that the update step in RLVF maximizes the Verifiability of $P_{\theta}$; this is analogous to Lemma A.4 for TL. We leave it for future work to use Lemma A.6 to obtain convergence bounds on RLVF (analogous to Theorem A.5). As mentioned in Section 4.2, the gap between the lemma and a full convergence theorem (informally) reduces to the problem of obtaining convergence bounds for Policy Gradient methods, a challenging and active research direction (e.g. Agarwal et al. ).

###### Lemma A.6 (RLVF gradient estimation) .

Fix an input distribution $\mu$ over $\Sigma^{\ast}$ and a verifier $V$ with round complexity $R$ and answer length $L_{a}$. For any transcript $(x,y,q_{1},\dots,a_{R})$ we let $\mathrm{Acc}_{V}(x,y,q_{1},\dots,a_{R})$ denote the indicator random variable which equals 1 if and only if $V$ accepts the transcript.
For any model $P_{\theta}$, denote by $\mathrm{ver}(\theta)$ the verifiability of $P_{\theta}$ with respect to $V$ and $\mu$ (Definition 3.4). For any $\theta$, if $\mathrm{ver}(\theta)$ is differentiable in $\theta$, then

$$ $\nabla\mathrm{ver}(\theta)=\operatorname*{\mathbb{E}}_{\begin{subarray}{c}x \sim\mu\\ y\sim P_{\theta}(x)\\ (q_{r},a_{r})_{r=1}^{R}\end{subarray}}\left[\mathrm{Acc}_{V}(x,y,q_{1},\dots,a _{R})\cdot\sum_{\begin{subarray}{c}r\in[R]\cup\{0\}\\ s\in[L_{a}]\end{subarray}}\vec{d}_{s}(\theta)\right]$ $$

where $(q_{r},a_{r})_{r=1}^{R}$ are as sampled in lines 5-6 of Algorithm 2, and $\vec{d}_{s}(\theta)$ is as defined in line 8 therein.

###### Proof.

Recall the *transcript generator of $P^{\theta}$*, denoted by $T^{\theta}_{V}$ (see Lemma A.4). By the definitions of Verifiability in Definition 3.4 and $V(x,y,q_{1},\dots,a_{R})$ in the lemma statement,

$$ $\displaystyle\mathrm{ver}(\theta)$ $\displaystyle\coloneqq\Pr_{\begin{subarray}{c}x\sim\mu\\ y\sim P_{\theta}(x)\end{subarray}}\left[\left<V,P_{\theta}\right>(x,y)\ \mathrm{accepts}\right]$ $\displaystyle=\operatorname*{\mathbb{E}}_{\begin{subarray}{c}x\sim\mu\\ y\sim P_{\theta}(x)\\ (q_{r},a_{r})_{r=1}^{R}\end{subarray}}\left[\mathrm{Acc}_{V}(x,y,q_{1},\dots,a _{R})\right]$ $\displaystyle=\operatorname*{\mathbb{E}}_{x\sim\mu}\left[\Pr_{\pi\sim\mathcal{ T}^{\theta}_{V}}[\mathrm{Acc}_{V}(x,\pi)\ ]\right]$ (9) $$

Now, for every input $x$, let $\Pi^{\ast}(x)\subset\Sigma^{\ast}$ denote the set of accepting transcripts:

$$ $\Pi^{\ast}(x)\coloneqq\left\{\pi^{\ast}\in\Sigma^{\ast}:\mathrm{Acc}_{V}{x,\pi ^{\ast}}\ \mathrm{accepts}\right\}.$ $$

Noting that $\Pi^{\ast}(x)$ has finite or countably infinite cardinality, for any fixed input $x$ we can write

$$ $\Pr_{\pi\sim\mathcal{T}^{\theta}_{V}}[\mathrm{Acc}_{V}(x,\pi)]=\sum_{\pi^{\ast }\in\Pi^{\ast}(x)}\Pr_{\pi\sim\mathcal{T}^{\theta}_{V}(x)}[\pi=\pi^{\ast}].$ (10) $$

We will use Equations (3) through (8) in the proof of Lemma A.4. Up to a change in index notation, these show that, for any $\pi^{\ast}$,

$$ $\nabla_{\theta}\Pr_{\pi\sim\mathcal{T}^{\theta}(x)}[\pi=\pi^{\ast}]=\Pr_{\pi \sim\mathcal{T}^{\theta}(x)}[\pi=\pi^{\ast}]\cdot\sum_{\begin{subarray}{c}r\in R \cup\{0\}\\ s\in[L_{a}]\end{subarray}}\nabla_{\theta}\vec{d}_{s}(\theta).$ $$

Combining Equations 9 and 10, by linearity of expectation we have that

$$ $\displaystyle\nabla_{\theta}\mathrm{ver}(\theta)$ $\displaystyle=\sum_{\pi^{\ast}\in\Pi^{\ast}(x)}\nabla_{\theta}\Pr_{\pi\sim \mathcal{T}^{\theta}(x)}[\pi=\pi^{\ast}]$ $\displaystyle=\operatorname*{\mathbb{E}}_{x\sim\mu}\left[\sum_{\pi^{\ast}\in \Pi^{\ast}(x)}\Pr_{\pi\sim\mathcal{T}^{\theta}(x)}[\pi=\pi^{\ast}]\cdot\sum_{ \begin{subarray}{c}r\in R\cup\{0\}\\ s\in[L_{a}]\end{subarray}}\nabla_{\theta}\vec{d}_{s}(\theta)\right]$ $\displaystyle=\operatorname*{\mathbb{E}}_{x\sim\mu}\left[\operatorname*{ \mathbb{E}}_{\pi\sim\mathcal{T}^{\theta}(x)}\left[\mathrm{Acc}_{V}(x,\pi)\cdot \sum_{\begin{subarray}{c}r\in R\cup\{0\}\\ s\in[L_{a}]\end{subarray}}\nabla_{\theta}\vec{d}_{s}(\theta)\right]\right]$ $\displaystyle=\operatorname*{\mathbb{E}}_{\begin{subarray}{c}x\sim\mu\\ \pi\sim\mathcal{T}^{\theta}(x)\end{subarray}}\left[\mathrm{Acc}_{V}(x,\pi) \cdot\sum_{\begin{subarray}{c}r\in R\cup\{0\}\\ s\in[L_{a}]\end{subarray}}\nabla_{\theta}\vec{d}_{s}(\theta)\right]$ $\displaystyle=\operatorname*{\mathbb{E}}_{\begin{subarray}{c}x\sim\mu\\ y\sim P_{\theta}(x)\\ (q_{r},a_{r})_{r=1}^{R}\end{subarray}}\left[\mathrm{Acc}_{V}(x,y,q_{1},\dots,a _{R})\cdot\sum_{\begin{subarray}{c}r\in R\cup\{0\}\\ s\in[L_{a}]\end{subarray}}\nabla_{\theta}\vec{d}_{s}(\theta)\right],$ $$

where in the last equality, the probability is over $(q_{r},a_{r})$ sampled as in Algorithm 2, and it follows from the definition of the transcript generator $\mathcal{T}^{\theta}(x)$.
∎

###### Lemma A.6 (RLVF gradient estimation) .

###### Proof.

## Appendix B Preliminaries on Stochastic Gradient Ascent

For convenience of the reader, we provide a description of Stochastic Gradient Ascent and quote a theorem on its convergence. We adapt the presentation in Shalev-Shwartz and Ben-David [], noting that they present Stochastic Gradient Descent in its more general form for non-differentiable unbounded functions.

Stochastic Gradient Ascent (SGA) is a fundamental technique in concave optimization. Given a concave function $f\colon\mathbb{R}^{d}\to[0,1]$, SGA starts at $w_{0}=\vec{0}\in\mathbb{R}^{d}$ and tries to maximize $f(w)$ by taking a series of “steps.” Than directly differentiating $f$, SGA instead relies on an estimation $\nabla f(w)$: in each iteration, SGA takes a step in a direction that estimates $\nabla f(w)$.

###### Definition B.1 (Gradient estimator) .

Fix a differentiable function $f\colon\mathbb{R}^{d}\to\mathbb{R}$ for some $d$. A *gradient estimator* for $f$ is a randomized mapping $D_{f}\colon\mathbb{R}^{d}\to\mathbb{R}^{d}$ whose expectation is the gradient of $f$. That is, for all $w\in\mathbb{R}^{d}$,

$$ $\operatorname*{\mathbb{E}}_{v\sim D_{f}(w)}[v]=\nabla f(w).$ $$

Note that this is an equality between $d$-dimensional vectors.

Figure: Algorithm 3 Stochastic Gradient Ascent

Theorem 14.8 in Shalev-Shwartz and Ben-David [] implies the following fact.

###### Fact B.2 .

Fix a concave $f\colon\mathbb{R}^{d}\to[0,1]$, a norm $||\cdot||$ on $\mathbb{R}^{d}$, and upper-bounds $B_{\mathrm{Norm}},B_{\mathrm{Lip}}>0$. Let

$$ $w^{\ast}\in\operatorname*{\mathrm{argmax}}_{w:||w||<B_{\mathrm{Norm}}}f(w),$ $$

and let $\bar{w}$ denote the output of Algorithm 3 run for $N$ iterations with learning rate

$$ $\lambda=\frac{B_{\mathrm{Norm}}}{B_{\mathrm{Lip}}\sqrt{N}}.$ $$

If at every iteration it holds that $||d_{i}||<B_{\mathrm{Lip}}$, then

$$ $\operatorname*{\mathbb{E}}_{\bar{w}}\left[f(\bar{w})\right]\geq f(w^{\ast})- \frac{B_{\mathrm{Norm}}\cdot B_{\mathrm{Lip}}}{\sqrt{N}}.$ $$

###### Definition B.1 (Gradient estimator) .

###### Fact B.2 .

## Appendix C Annotations

We formally capture the modification described in Section 4.3 by introducing a *transcript annotator* and an *answer extractor* incorporated into the training and inference stages, respectively.

Fix a verifier $V$ in an $R$-round proof system with question length $L_{q}$ and answer length $L_{a}$. An *annotation system* with annotation length $\widetilde{L_{a}}$ consists of a *transcript annotator* $A$, and an *answer extractor* $E$.

In terms of efficiency, think of the annotator as an algorithm of the same computational resources as an honest prover in the system (see Definition 3.2, and the answer extractor as an extremely simple algorithm (e.g., trim a fixed amount of tokens from the annotation).

To use an annotation system the following changes need to be made:

- •
At training time, an input $x$ and transcript $\pi$ is annotated to obtain $\widetilde{\pi}\coloneqq A(x,\pi)$, e.g. before the forwards backwards pass in TL (line 3 in Algorithm 1).
- •
At inference time (i.e., during interaction between $V$ and $P_{\theta}$), the prover keeps track of the annotated transcript, but in each round passes the model-generated (annotated) answer through the extractor $E$ before it is sent to the verifier. That is, in each round $r\in[R]$, the prover samples
$\widetilde{a_{r}}\sim P_{\theta}(x,y,q_{1},\widetilde{a_{1}},\dots,\widetilde{
a_{r-1}},q_{r}).$
The prover then extracts an answer $a_{r}\coloneqq E(\widetilde{a_{r}})$ which is sent to the verifier.

## Appendix D A simple proof system for the GCD

The Euclidean algorithm for computing the Greatest Common Divisor (GCD) of two integers is possibly the oldest algorithm still in use today [Knuth, ]. Its extended variant gives a simple proof system.

Before we dive in, let us clarify what we mean by *a proof system for the GCD*. Paul has two integers $212$ and $159$; he claims that $GCD(212,159)=53$. An inefficient way for Veronica to check Paul’s answer is by executing the Euclidean algorithm on $(212,159)$ and confirm that the output is $53$. In an efficient proof system, Veronica asks Paul for a short string $\pi^{\ast}$ (describing two integers) with which she can easily compute the answer—without having to repeat Paul’s work all over. On the other hand, if Paul were to claim that “$GCD(212,159)=51$” (it does not), then for any alleged proof $\pi$, Veronica would detect an error and reject Paul’s claim.

The verifier in the proof system relies on the following fact.

###### Claim D.1 (Bézout’s identity [Bezout, 1779 ] ) .

Let $x_{0},x_{1}\in\mathbb{N}$ and $z_{0},z_{1}\in\mathbb{Z}$. If $z_{0}\cdot x_{0}+z_{1}\cdot x_{1}$ divides both $x_{0}$ and $x_{1}$,
then $z_{0}\cdot x_{0}+z_{1}\cdot x_{1}=GCD(x_{0},x_{1})$.

Any coefficients $z_{0},z_{1}$ satisfying the assumption of D.1 are known as *Bézout coefficients* for $(x_{0},x_{1})$. D.1 immediately gives our simple proof system: For input $x=(x_{0},x_{1})$ and alleged GCD $y$, the honest prover sends (alleged) Bézout coefficients $(z_{0},z_{1})$. The Verifier accepts if and only if $y=z_{0}\cdot x_{0}+z_{1}\cdot x_{1}$ and $y$ divides both $x_{0}$ and $x_{1}$.

In this proof system the Verifier does not need to make any query; to fit within Definition 3.2, we can have the verifier issue a dummy query. Furthermore, by D.1 it is complete and has soundness error $s=0$. Lastly, we note that the Verifier only needs to perform two multiplications, an addition, and two modulus operations; in that sense, verification is more efficient than computing the GCD in the Euclidean algorithm as required by Remark 3.3.

###### Claim D.1 (Bézout’s identity [Bezout, 1779 ] ) .

#### Annotations.

To describe how a proof $z=(z_{0},z_{1})$ is annotated, let us first note how it can be computed.
The Bézout coefficients can be found by an extension of the Euclidean algorithm. It is described in Algorithm 4.(^9^99Our description is the same as [https://en.wikipedia.org/wiki/Extended_Euclidean_algorithm](https://en.wikipedia.org/wiki/Extended_Euclidean_algorithm).)

Figure: Algorithm 4 Extended Euclidean algorithm

Referring to Algorithm 4, the annotation of a proof $z=(z_{0},z_{1})$ will consist of intermediate steps in its computation. Suppose that in each iteration of the While-loop, the algorithm stores each of $r_{0}$, $s_{0}$ and $q$ in an arrays $\vec{r_{0}}$, $\vec{s_{0}}$ and $\vec{q}$. The annotation $\tilde{z}$ of $z$ is obtained by concatenating each of these arrays. In practice, to avoid the transformer block (context) size from growing too large, we fix a cutoff $T$ and first trim each array to its first $T$ elements.

We formalize this in the terminology of Appendix C by defining a Transcript Annotator and Answer Extractor. Note that, since our proof system consists only of one “answer” $z$ send from the prover to the verifier, the entire transcript $\pi$ is simply $z=(z_{0},z_{1})$. Since the verification is deterministic, this means that the proof system is of an $\mathsf{NP}$ type (however, note that the search problem of finding the “$\mathsf{NP}$-witness” $z=(z_{0},z_{1})$ is in fact in $\mathsf{P}$).

- •
*Transcript Annotator $A$:* For a fixed cutoff $T$ and given input $x=(x_{0},x_{1})$ and transcript $z=(z_{0},z_{1})$, $A$ executes Algorithm 4 on input $x=(x_{0},x_{1})$. During the execution, $A$ stores the first $T$ intermediate values of $r_{0}$, $s_{0}$ and $q$ in arrays $\vec{r_{0}}$, $\vec{s_{0}}$ and $\vec{q}$. It outputs $A(x,z)\coloneqq(\vec{r_{0}},\vec{s_{0}},\vec{q},z)$.
- •
*Answer Extractor $E$:* Given an annotated transcript $\tilde{z}=(\vec{r_{0}},\vec{s_{0}},\vec{q},z)$, outputs $E(\tilde{z})\coloneqq z$.

We note that the computational complexity of $A$ is roughly that of the honest prover, i.e., Algorithm 4 (up to additional space due to storing intermediate values). As for $E$, it can be implemented in logarithmic space and linear running time in $|\tilde{z}|$, i.e., the length of the description.(^10^1010That is, if integers are represented by $n$-bits, then $E$ has space complexity $O(\log n+\log T)$ and running time $O(n\cdot T)$.)

## Appendix E Experiment details

We provide details of how we implemented the experiments in Section 5 and additional figures for each experiment.

#### Model architecture.

We use Karpathy’s *nanoGPT*.(^11^1111[https://github.com/karpathy/nanoGPT](https://github.com/karpathy/nanoGPT).) We use a 6.7M parameter architecture of $8$ layers, $8$ attention heads, and $256$ embedding dimensions. We optimized hyperparameters via a random hyperparameter search, arriving at learning rate $0.0007$, AdamW $\beta_{1}=0.733$ and $\beta 2=0.95$, $10\%$ learning rate decay factor, no dropout, gradient clipping at $2.0$, no warmup iterations, and $10\%$ weight decay.

#### Data.

We sample integers from the $\log_{10}$-uniform distribution over $\{1,\dots,10^{4}\}$. Models in Tables 2 and 2 are trained for 100K iterations on a dataset of of $\approx$10M samples. For Figure 3 (base ablation) we train for 20K iterations on a dataset of $\approx$1M samples; this is because this setting required 68 many runs in total, whereas the annotation-cutoff ablation required 18 longer runs.

#### Compute.

All experiments were run on a machine with an NVIDIA A10G GPU, 64GB of RAM, and 32 CPU cores. Longer runs (annotation-cutoff ablation) took about 75 minutes each. Shorter runs (base ablation) took about 15 minutes. The total running time of our experiments was approximately 40 hours, excluding time dedicated to a random hyperparameter search. The overall disk space needed for our models and data (to be made available upon publication) is 4GB.

#### Representing integers.

We fully describe how integer sequences are encoded. As a running example, we will use base $210$. To encode a sequence of integers, each integer is encoded in base $210$, a sign is prepended and a delimiter is appended, with a unique delimiter identifying each component of the sequence. For example, consider the input integers $x_{0}=212$ (which is $12$ in base 210) and $x_{1}=159$. Their GCD is $y=53$, with Bézout coefficients $z_{0}=1$ and $z_{1}=-1$. Therefore, the sequence $(212,159,53,1,-1)$ is encoded as

+,1,2,x0,+,159,x1,+,53,y,+,1,z0,-,1,z1

where commas are added to distinguish between different tokens. Null tokens are appended to pad all sequences in a dataset to the same length. Both the input and the padding components are ignored when computing the loss and updating parameters.

#### Annotations

Annotations are encoded as above, with each component in an intermediate step $\pi_{t}$ delimited by a unique token. Since different integer pairs may require a different number of intermediate steps to compute the Bézout coefficients, we chose to pad all annotaitons to the same length $T$ by the last step $\pi_{T}$ in the sequence (which consists of the final Bézout coefficients). This ensures that the final component output by the model in each sequence should be the Bézout coefficient, and allows us to batch model testing (generation and evaluation) resulting in a 1000x speed-up over sequential testing.

As an example, consider the inputs $x_{0}=46$ and $x_{1}=39$. Tracing through the execution of Algorithm 4, we have

$$ $\begin{array}[]{c|c|c|c|c|c|c|c|c}&x_{0}&x_{1}&y&\vec{s_{0}}&\vec{r_{0}}&\vec{ q}&z_{0}&z_{1}\\ \hline\cr&46&39&&1&46&1&&\\ &&&&0&39&5&&\\ &&&&1&7&1&&\\ &&&&-5&4&1&&\\ &&&&6&3&3&&\\ &&&1&&&&-11&13\\ \end{array}$ $$

To encode this as an annotated transcript for the transformer, we must specify a base of representation and an annotation cutoff. Suppose that we wish to encode this instance in base $B=10$ and cutoff $T=3$. Then the input with the annotated transcript is encoded as

+,4,6,x0,+,3,9,x1,+,1,y,
+,1,z0’,+,4,6,z1’,+,1,q’,
+,0,z0’’,+,3,9,z1’’,+,5,q’’
+,1,z0’’’,+,7,z1’’’,+,1,q’’’,
-,1,1,z0,+,1,3,z1

where commas are used to separate between tokens, and linebreaks are added only for clarity. Notice the three types of tokens: signs, digits, and delimiters. Notice also that the output $y$ is added immediately after the input, followed by the annotated transcript (whose six tokens comprise the proof itself). Since the Self-Proving model we train has causal attention masking, placing the output $y$ before the proof means that the model “commits” to an output and only then proves it.

Figure: Figure 4: Verifiability as a function of the number of samples $N$. Each iteration (X axis) is a batch of 1024 samples from a dataset of $\approx$10M sequences. Every 10k iterations, Verifiability was evaluated on a held-out dataset of 1k inputs (as described in Section 5). $T$ is the number of steps in Annotated Transcript Learning (Figure 2), and $T=0$ is non-annotated Transcript Learning. Each $T$ was run with three seeds, with mean depicted by the curve and standard error by the shaded area.
Refer to caption: extracted/5650103/figs/annot_curves.png

## Peer Reviews

confidence: 4
contribution: 4
initial_rating: 8
presentation: 4
questions: The only question that I have is related to what I said in the second point in the weakness box. My understanding is that Algorithm 1 uses the expected probability as a training objective, instead of expected log probability. Is there a reason for this? Is this due to the consistency with Theorem 4.1?

Here are some minor typos.

(1) L284 : EOS in Sigma^* ===> EOS in Sigma

(2) L391 : Giving examples of annotations may help some readers.

(3) L510 : Have you tried more samples in some cases and checked your conjecture?

(4) L926 : a_0 := y ===> a_0 := y^*

(5) L928 : (y,q_1^*,..., q_r^*,a_r) ===> (y^*,q_1^*,...,q_r^*)

(6) L1150 : Maybe it is better to break a line before "for s in [L_a] do"
soundness: 3
strengths: 1. The idea of using a verifier from the theory of interactive proof systems for learning a self-proving model is very nice. It may lead to further interesting research activities that address the AI safety issue using several related tools from theoretical computer science, such as PCP and property testing etc. 

2. The paper is written well. The discussion on related work helped me to understand what people had explored in the past, and to see the contributions of the paper more clearly. Also, the background materials are covered nicely so that I can follow most of the formal developments in the paper although I am not familiar with, for instance, interactive proof systems.

3.  The paper contains a theoretical justification, namely, Theorem 4.1. I am less confident that this theorem is useful in practice, but it is good that the authors makes an effort for proving a theoretical result. Also, their comment on the proof using the reduction to SGD and the communication complexity by a verifier (captured by the constant C) helped me to see what goes on more clearly.
summary: In this paper, the authors propose a new type of self-proving models that not just predict an output for a given input but also a proof for the correctness of the output. One of the main ideas of the paper is to use a particular notion of proof from the work of interactive proof systems in theoretical computer science, where a proof means a sequence of answers to a verifier's questions that can convince the verifier of the correctness of the output. The authors compare their approach with other similar proposals for self-proving models, and emphasise the benefit of having an instance-specific proof in their approach. They then describe two algorithms for learning such a proof-producing transformer model, namely, Transcript Learning (TL) that assumes strong supervision via successful question-answer sequences, and Reinfocement Learning from Verifier Feedback (RLVF) that does not assume such strong supervision. Their experiments with learning the GCD algorithm with a small version of GPT show the promise of their approach.
weaknesses: I support the acceptance of this paper. The following points are mostly minor.

1. Having an example in addition to GCD would have convinced me of the promise of the authors' approach far more. As the authors pointed out, the proofs in this GCD case do not involve questions from the verifier, and so they are simple. Also, the annotated transcript learning is only vaguely defined, and it is only explained in terms of illustration in the example via the intermediate steps of the Euclid algorithm. Seeing one more example would have helped me to grasp what annotations would mean in other problems.

2. I suggest to include Algorithms 1 and 2 into the main text, instead of including them in the appendix. They are more or less standard, but I feel that they are one of the main contributions of the paper. Also, one unexpected thing that I found is that Algorithm 1 is derived by maximising theta over the expected probability E_{trace ~ p(trace)}[q_theta(trace)], instead of the expected log probability E_{trace ~ p(trace)}[log q_theta(trace)] (i.e., cross entropy loss). Some subtleties like this deserve the attention of the reader, I think.

---

confidence: 3
contribution: 3
initial_rating: 6
presentation: 3
questions: What are your views on probalistic gurantees for mathematical statement? Do you consider them useful, or is this setup a step along the way to a different application where probabilistic guarantees are more meaningful?

Can you comment on the importance and derivation of the verifier and highlight the ease or difficulty in deriving them for the problem in hand in combination with or independently of the self-proving model?

What are your thoughts on moving beyond GCD for a mathematical theory and beyond this other mathematical challenges?

Edits post review:

1. I acknowledge you might not agree with my comment of this being a "well-known set up". This was not meant as a criticism to the work. I think you are well aware that the general concept of prover/disprover set up has been long been around in logic (indeed, general philosophy before then) and theoretical computer science including in synthesis. The setup has also been used in AI Argumentation and many other areas. I understand that here the emphasis is different and so is the generality of the overall task. Note that pretty general theorem provers such as Isabelle have also been used in similar setups to aid computer proofs. In any case this was not a criticism but a request for clarification. I do not believe we fundamentally disagree here.
2. To me the role of the verifier appears to be pretty important. So I would encourage to explore this issue more. The concern I have is that a lot of the problem here has been pushed onto the (derivation of) the verifier). I agree with the authors, but only to some extent, that the work explores a somewhat different dimension. My point was and to some extent still is that whole apparatus appears to reside on the verifier but its construction is not necessarily obvious and not explored here. I accept that my suggestions can be left for further work.
3. I do appreciate the attempt to run further experiments on a different challenge, particularly given, as reported another referee, perhaps GCD is not entirely illustrative to show the advantages of the present approach.
soundness: 3
strengths: I find the overall approach principled and welcome. Moving the assessment of the answer of a model from test results to an estimate of the correctness on the individual query (and this not being provided by the model itself) is certainly welcome. 

I am not sure the overall setup is novel as such (see below); however I believe the error bounds on the two learning approaches are. The results are well backed by theory and the paper does a good job at making this challenging subject as accessible as possible without trivialising the contribution.
Some experiments, although perhaps limited, are provided supporting the results.
summary: The paper develops the concept of self-proving models that justify (or "prove" in the authors language) their answers to a trusted and pre-built verifier. The process results in a probablistic guarantee on the correctness of the answer provided by the self-proving model.  Transcript learning and RL are proposed as methods to derive a self-proving model. Experiments are conducted on a Greatest Common Divisor problem.
weaknesses: It was not clear to me the extent to novelty of the overall setup of the pair prover/disprover. Obviously this is a well-known setup in many applications including those cited in the literature (perhaps the whole area of "Argumentation" in AI should also be included as it is not very far from here), but this particular instantiation with ML models and a formal verifier could be clarified.

The verifier obviously has a fundamental role here. I might have missed this but the implications of this were not clear to me (how can they be derived and at what costs). 

I think the authors realise that their experimentation on GCD are limited even from a purely algebraic perspective. I think this is OK, but more thoughts into how this might or might not scale to more challenging problems or more general ones might be beneficial.

Fundamentally, the end result obtained by the method, if I understand the paper, is a probabilistic guarantee that the answer provided is correct (following a sequence of challenges to the verifier). In the domain explored (algebra) we tend to deal with true/false propositions.

---

confidence: 3
contribution: 2
initial_rating: 3
presentation: 2
questions: 1. I think this type of theoretical bound needs a confidence parameter $\delta$. Since we estimate parameter $\theta$ from a finite set of $N$ samples instead of accessing the distribution $\mu$,  it is possible that the drawn samples are "bad" and that we cannot estimate suitable parameters from the samples. Could you please explain why we do not need a confidence parameter $\delta$?
2. The paper says that completeness and soundness are properties of a verifier (Definition 3.2). However, it seems unrealistic to imagine a probabilistic verifier whose soundness error is always smaller than $s$ for *any* $x, y$ and $P$, unless $s = 0$. How can we obtain such a verifier? Where does the probability come from?  Moreover, I think it is possible to reduce false positive errors (line 208) arbitrarily by running a probabilistic verifier $V$ for multiple times for the same $(x, y, P)$. It is more realistic for me to assume that there are specific $(x, y, P)$ that causes a false-positive error for the verifier $V$, and thus it depends on the distribution $\mu$. 
3. Related to the above point, Definition 3.2 assumes the randomness of $V$ and $P$ line 209, but the definition of soundness assumes the condition holds for all $P$. Is $P$ random?
soundness: 2
strengths: 1. This is a well-motivated work. The use case shown in the introduction of the paper is attractive. 

2. The proposed self-proving framework that proves the correctness of the answer by interactions between an autoregressive model and an external verifier seems a natural setting.
summary: This paper proposes a self-proving model, a new learning paradigm that a model outputs both a prediction $y$ and a proof for the correctness of the prediction by interacting with a verifier. A self-proving model is useful for users since it can ensure that the output of a model is correct. The paper proposes a self-proving model and defines some metrics for evaluating the performance of a self-proving model. The paper also gives learning algorithms for learning a self-proving model and theoretical analyses on the convergence of the transcript learning algorithm. The experiments evaluate the performance of self-proving models on a GCD task.
weaknesses: 1. Theorem 4.1, one of the major theoretical contributions of the paper, makes some strong assumptions. Therefore, I think the contribution of the theorem is limited.  Firstly, it assumes that $A(\theta)$ is concave. I think this assumption does not hold for the typical autoregressive models used today, including the GPT model used in experiments. Moreover, the theorem assumes the existence of $\theta^\ast$ satisfying $A(\theta^\ast) \geq 1 - \epsilon/2$. This is also a strong assumption since it is currently not clear whether such self-proving models exist or not. 
2. The paper evaluates the self-proving model's performance on a GCD task. However, I feel that GCD would not be appropriate as a use case for a self-proving model since it is an easy task, and we do not need any machine-learning techniques to solve it. It is reasonable that Carton (2024) solved a GCD task since the paper's main objective is to understand how a transformer works. On the other hand, I think that this paper should show the effectiveness of the proposed self-proving model, and the experiments with a GCD task are not sufficient.
3. The paper emphasizes the use-case that self-proving models can guarantee the correctness of a specific $x_0, y_0$. (line 262). This feature depends on  the $s$-soundness defined for a probabilistic verifier. However, the assumption that $s$-soundness holds for any $x, y, P$ is unrealistic (See the question 2 below). It is more natural to assume that a false-positive error (line 207) depends on the distribution over $x, y$. However, if we make such an assumption, then it is difficult to give a guarantee for specific $x_0, y_0$. Therefore, I think the self-proving model does not work as stated in the use case.

---

confidence: 4
contribution: 3
initial_rating: 8
presentation: 3
questions: No questions.
soundness: 3
strengths: I find the topic of the paper quite interesting.

 The paper seems to provide a nice framework to combine interactive proof systems with techniques from learning theory. Although formal verification has been widely studied in connection with learning theory, the disadvantage is that, in most of the approaches, the goal is to construct a proof of correctness in some fixed proof system. The use of interactive proof systems adds a lot of flexibility to the process, besides giving an avenue for a theoretical analysis related to the convergence of the learning process etc.
summary: In this work, the authors propose a methodology to learn models that can provide evidence about the correctness of their answers. 
Given a function F:Sigma*->Sigma*, a model for F is a function F_theta that assigns to each x\in Sigma^* a probability distribution F_theta(x). 

A model is alpha-correct if on a random input x, the output F_{theat}(x) is equal to F(x) with probability at least \alpha. 
Given a function F and a verifier V, a model F_theta is beta-self proving if V(x,y)=1 with hight probability, where x is an input sampled at random and y is sampled at random from F_theta(x). 

The goal is to learn a model that has a high degree of correctness (\alpha close to 1) and a high degree of verifiability (\beta close to 1). The authors develop a methodology for this task, and use learning models that compute the GCD of two numbers as an example.
weaknesses: The disadvantage of the approach is that it requires access to the implementation of a previously existing verifier. I find that the paper lacks a discussion about the usefulness of trying to learn a function for which we already have an implementation.

Meta-review: The paper introduces a framework when ML models can prove the correctness of their output. The notion of proof here is "interactive proofs" as studied in computational complexity, with a polynomially-bounded verifier and a potentially unbounded prover that can interact. When the answer is correct, then the prover should be able to convince the verified with high probability of its correctness, on the other hand when the answer is wrong the verifier should not accept the answer with high probability. The contribution of this paper is not related to interactive proof systems, they are using the standard notion. The contribution is mainly to introduce this framework to modern ML settings. This requires the training process to be aware of a specific verifier that will be used and the training process needs to be augmented with transcripts. The authors propose a gradient-descent based approach as well as an RLVF approach. The paper definitely introduces new ideas, however, the assumptions required for learning algorithms to converge are fairly strong -- this is to be expected-- and also unrealistic. Thus, there needs to be a thorough empirical evaluation. The authors have presented experiments with GCD in the main paper, and subsequently performed experiments with discrete square root during the rebuttal period.

Decision: Reject