A Theory for Worst-Case vs. Average-Case Guarantees for LLMs
Authors: Noga Amit
Shafi Goldwasser
Orr Paradise
Guy N. Rothblum
Venue: NeurIPS 2025 poster ()
Keywords: Trustworthy ML
Interactive Proofs
Computational Complexity Theory
Primary area: theory
TL;DR: Introducing models that prove their own correctness via an Interactive Proof, and how to learn such models.

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$ 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$. The *soundness* property of $V$ guarantees that, for *every* input, no model can convince $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$. We devise and analyze two generic methods for learning Self-Proving models: *Transcript Learning (TL)* which relies on access to transcripts of accepting interactions, and *Reinforcement Learning from Verifier Feedback (RLVF)* which trains a model by emulating interactions with the verifier.

distribution of in- A Theory for Worst-Case vs. Average-Case Guarantees for LLMs
Noga Amit UC Berkeley
Shafi Goldwasser* UC Berkeley
Orr Paradise" UC Berkeley
Guy N. Rothblum Apple
Abstract
How can we trust the correctness of a learned model on a particular input of in- terest? Model accuracy is typically measured average puts, giving no guarantee for any fixed input. This paper proposes a theoretically- founded solution to this problem: train Self-Proving models that prove the cor- rectness of their output to a verification algorithm V via an Interactive Proof. Self- Proving models satisfy that, with high probability over input sampled from given distribution, the model generates a correct output and successfully proves correctness to The soundness property of V guarantees that, for every in- put, no model can convince V of the correctness of an incorrect output. Thus, a Self-Proving model proves correctness of most its outputs, while all incorrect outputs (of any model) are detected by V. We devise and analyze two generic methods for learning Self-Proving models: Transcript Learning (TL) which relies on access to transcripts of accepting interactions, and Reinforcement Learning from Verifier Feedback (RLVF) which trains model by emulating interactions with the verifier.
Introduction
Bob is studying for his algebra exam and stumbles upon question Q that he cannot solve. He queries Large Language Model (LLM) for the answer, and responds with number: 42. Bob aware of recent research showing that the LLM attains 90% score algebra benchmarks (cf. Frieder et al. 2023), but should trust that the answer to his particular question Q is indeed 42?
Bob could ask the I.LM to explain its answer in natural language. Though he must proceed with cau- tion, the LLM might try to convince him of incorrect answer (Turpin et al. [2023. Moreover, even if 42 is the correct answer, the LLM may fail to produce convincing proof (Wang et al. 2023). If only the LLM could formally prove its answer, Bob would verify the proof and be convinced.
This paper initiates the study of Selv-nroving models (Fig. T that prove the correctness of their answers via Interactive Proof system [Goldwasser et al. 1985]. Self-Proving models successfully convince a verification algorithm rejects all incorrect answers with high probability over the interaction. This guarantee holds against provers that have access to V's specification, and unbounded computational power.
with worst-case soundness guarantees: for any question, V
Our contributions are as follows.
We define Self-Proving models (Section
We propose two methods for learning Self-Proving models (Section The first, Tran- script Learning (TL.), relies on access to transcripts of accepting interactions. The second method, Reinforcement Learning from Verifier Feedback (RIVF), trains model by emu- lating interactions with the verifier.
AAtthors listed alphabetically.
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

Before we can define models that prove their own correctness, we must first define correctness. Correctness is defined with respect to an input distribution μ over Σ", and ground-truth F* that defines correct answers. For simplicity of presentation, we focus on the case that each input x E Input x
Self- Prov-rr Model
Output y
Verification
q1
Algorithm
a1
P i
qR
ag
accept/reject
Figure 1: Self-Proving models. For input Self-Proving model Po generates output y and sends a Verification Algorithm V. Then, over [R]] rounds, sends query qi and receives an answer a; from Pa. Finally, V decides ("accept/reject") whether it is convinced that y correct output for z.
We prove gradient approximation lemmas for both methods (Lemmas 3.2 and 3.3 and
convergence bounds for TL under convexity and Lipschitzness assumptions (Section These are supplemented by empirical validation on simple arithmetic capability (Ap- pendix F). Code and data are at authtts:/ htt//gttttuu.... com/ orrp/ self proving models
This paper develops theory of learned models that prove their own correctness via interactive proof system, and thus lies at the intersection of machine learning and Interactive Proof systems. We defer the diseussion of relevant prior work from these areas the related work section in Ap- pendix [A] The rich and well-studied question of which settings are verifiable within an interactive proof system is beyond our scope. Our theory is general in that applies any setting which ver- ifiable within an interactive proof system, e.g., any decision problem solvable in polynomial space For broader introduction proof systems, see Goldreich 20088
Shamir 1992.
2 Defining 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 2.1
We then introduce our main definition in Section 2.2
2.1
Preliminaries
Let Σ be finite set of tokens and " denote the set of finite sequences of such tokens. We consider sequence-to-sequene models F9: + Σ", which are total functions that produce an output for each possible input sequence. A model is parameterized by real-valued, finite dimensional vector We consider models as randomized functions, meaning that F& (z()) a random variable over Σ", of which samples denoted by Fo(x).
has exactly one correct output F* (x:) E Σ', and zero-one loss function on outputs (the general case is deferred to Appendix C The fundamental goal machine learning can thought of as learning model of the ground-truth F*, Formally,
Definition 2.1 (Correctness). Let be distribution of input sequences in E" and let F* Σ* + Σ* be fixed (deterministic) ground-truth function. For any a E [0, 1}. we say that model Fo is a- correct (with respect to p) if
Pr Fo(r)
FF=F F*) a.
interactive proof system [Goldwasser al. 1985 protocol carried out between an efficient verifier and computationally unbounded prover. 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 probabilistic polynomial-time algorithm tailored particular ground-truth capability F". 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 Σ", the model Fe "claims" that y ~ (a( is correct. We now define what it means to prove this claim. We will use Po to denote Self-Proving models, noting that they formally the same object as non-Self-Proe Self---ff-oo ("vanilla") models Fg. This notational change is to emphasize that Po first outputs y ~ (x) and is then prompted by the verifier, unlike F9 who only generates an output y ~ Fx()).
A Self-Proving model proves that y ~ (r(x)) is correct to a verifier V over the course of R rounds of interaction (Figure D. In each round i E Rl. verifier V queries Pa on a sequence q E' to obtain an answer a; E r"; once the interaction is over, V accepts or rejects. For fixed z, y E "", the deci- sion of V after interacting with Pg is a random variable over V's decision (accept/reject), determined by the randomness of V and Po. The decision random variable is denoted by (V, Po) ().
Next, we present a definition of Interactive Proofs restricted our setting.
Definition 2.2. Fix soundness error s (0, 1), finite set of tokens E and ground-truth
F': Σ' + E A verifier V (in an Interactive Proof) for F* is a probabilistic polynomial-tinn algorithu that is given explicit inputs z. E Σ' and black-box (oracle) query access to a prover P It interacts with P over R rounds (see Figure D and outputs a decision (V, P) (xr, v) E (reject, a Verifier V satisfies the following two guarantees:
Completeness: There exists an honest prover P such that, for all x E E",
Pr[[V, (') (= (x)) accepts) = 1,
where the probability is over the randomness of V
Soundness:
For all P and for all x,y y E Σ", if + (x) then Pr[[V, P) (z. y) accepts] S 8,
where the probability is over the randomness of V and P. and is the soundness error.
The efficiency of an interactive proof is usually measured with respect to four parameters: the round complexity R. the communication complexity (the overall number of bits transferred during the interaction), '* efficiency and V's efficiency. These complexity measures scale with the com- putational complexity of computing the ground-truth F", For example, an interactive proof for complex F* may require multiple rounds of interaction.
Remark 2.3 (Verifier efficiency). Definition 2.2 requires that V is a polynomial-time algorithm whereas provers are unbounded. This captures requirement for efficient verification. We chose polynomial time as a measure of efficiency because it is common in the Proof systems literature. That said, one could adapt Definition 2.2 fit alternative efficiency measures, such as space complexity (Condon and Lipton 1989] or circuit depth (Goldwasser et al. 20077.. Regardless of which measure taken, to avoid a trivial definition it is crucial that V should be more efficient than the honest prover P* else, V can simply execute Pa to perform the computation itself.
By definition, the soundness error s of 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 manually-definet 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 's answers depends all previous queries and answers in the interaction. This captures the setting of stateful models, e.g. a session with a chatbot.
2 Both are randomized mappings from M to V"
P We intentionally write P rather than Ps: Interactive Proofs are defined with respect to all possible provers, not just parameterized ones.
WLOG, the honest prover deterministic by tixing the optimal randomness of randomized prover.
3

---

Table 1: Formal guarantees. Completeness and soundness are fundamental guarantees of veri- fication algorithm V. Verifiability (novel in this work) is a feature of a model Po with respect to verifier V and input distribution μs. Importantly, V's soundness holds for any input x and output y,-
Guarantee
Type
Def.
V
Completeness & Soundness
Worst-case: Va, y Average-case: I ~ p4 y (o(x)
2.2 2.4
Po
Verifiability
Towards defining Self-Proving models (Section 2.2). let observe the following. Completeness and soundness are worst-case guarantees, meaning that they hold for all possible inputs x E E" In particular, completeness implies that for all x D", the honest prover P convinces V of the correctness of F* (z)) in classical proof systems there is no guarantee that an "almost honest" prover can convince the verifier (cf. Paradise 202T). Yet, if we are to learn a prover Po. cannot expect it to agree with P* perfectly, nor can we expect it to always output F* (x)). Indeed, Self-Proving mod- els will have distributional guarantee with respect to inputs x p.. This distinction is summarized in T
2.2 Self-Proving Models
We define the Verifiability of a model Pg with respect to input distribution and a verifier V. Intuitively, Verifiability captures the ability of the model to prove the correctness of answer y (x). when the imput is sampled from μ. We refer models capable of proving their own correctness as Self-Proving models. Notice that, as in Definition 2.2 the verifier is fixed and agnostic to the choice of the Self-Proving model.
Definition 2.4 (Self-Proving model). Fix a verifier V for a ground-truth F": E - Σ as in Definition 2.2 and distribution μ over inputs E'. The Verifiability of model Pa: E" E is
defined as
verv. (0)
Pr [(V, Po) (2,y) v) accepts].
y~Pa(
We say that model Po is 3-Self-Proving with respect to V and p. if verv. (0) 2 B.
Remark 2.5 (Verifiability = correctness). Notice that the ground-trucd F does not appear in Definition 2.4 except for the first sentence. Indeed, once it is established that V is a verifier for F (as per Definition 2.2 then Verifiability w.r. V implies correctness w.r. F* Consider any input distribution ground-truth F", and a verifier V for F with soundness error By union bound, if a model Pg is 3- --Verifiblle then (3 s)-correct. That is to say, Verifubillt is formally stronger guarantee than correctness when V has small soundness error
As depicted Figure 1 a Self-Proving model Pa plays a dual role: first, it generates an output y Pa (z)), and then it proves the correctness of this output to V. Note also that Verifiability is feature of model, unlike completeness and soundness which are features of a verifier (see Table
The benefit of Verifiability over correctness is captured by the following scenario. Alice wishes to use a model Pe compute some functionality F on an input 2o in a high risk setting. Alice generates yo (r(z)) Should Alice trust that 30 is correct? If Alice has a held-out set of la- beled samples, she can estimate Po average correctness on μ. Unfortunately, (average) correctness provides no guarantee regarding the correctness of the particular (Zo, Bo) that Alice has in hand. If, however, Alice has access to verifier V for which Py Self-Proving, then she can trust the model on an input-by-input (rather than average-case) basis: Alice can execute V on (In, Bo) and black-box access Pg. Soundness of V guarantees that if yo is incorrect, then V rejects with high probability, in which case Alice should either generate Po(xa) again-or find better model.
3 Algorithms for Learning Self-Proving 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 Po(x)) correct; she may simply verify this herself by executing the verification protocol. How, then, can we learn models that are not just approximately-corees but Self-Provine as well?

---

We focus on differentiable autoregressive models, and assume that the learner has access to input samples x ~ I and correct outputs F (x), as well as the verifier's specification (code), Additionally, the learner can emulate the verifier, as the latter is computationally efficient (Remark 2.3
Importantly, may not assume that the verifier V is differentiable--it it is an arbitrary (efficient oracle) Turing machine-and so we cannot directly compute gradients of its decision with respect to model parameters. The challenge is align the model with a verifier. Algorithms | and address this challenge by (essentially) computing unbiased estimators for the Verifiability verv or a surrogate (lower-bound) thereof. We formally prove these properties in Lemmas 3.2 and
Our approach is inspired by Reinforcement Learning from Human Feedback [Christiano et al. 2017]. method for aligning models with human preferences, which has recently been used to align Seguence-to-sequenee
models [Quyang et al.] 2022]. However, there are two important differ- ences 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 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 al. 2022).
The full specification of the learning model can be found in Appendix D.I to the transcript of interaction between verifier and a prover (see Figure []. π = (y. 91, .1,...,,..,..................... aR). . Let T<s E = denote the s-token long prefix of π.
We will refer denoted by
3.1 Transcript Learning
We first present an algorithm for learning Self-Proving models which relies on access to a distribu- tion of accepting transcripts. We focus on the algorithm first, and then discuss how the learner may obtain accepting transcripts in Section 3.1.I The idea is to learn a model not just of I + y² for a correct output y", but of x + y n², where accepted. Formally, Transcript Learning assumes access to a transcript generator-a random vari- able over transcripts that faithfully represents the interaction of the verifier with some prover for a given input. An honest transcript generator is one which is fully supported on transcripts accepted by the verifier. These are defined next.
transcript of an interaction which the verifier
Definition 3.1 (Transcript generator). Fix a verifier V in a proof system of R E N rounds. A transcript generator Tv for V is randomized mapping from inputs x E Σ* to transcripts (y. q1 01,.... IR; aR) Σ². For any input x, (v(x) satisfies that for each r S R, the marginal of Tv (z) the rt query qr agrees with the corresponding marginal of the query generator (Va)r A transcript generator TV = Tv is honest if it is fully supported on transcripts n²' for which the verifier accepts.
Notice that for any verifier V, there is one-to-one correspondence between transcript generators and (possibly randomized) provers. We intentionally chose not to specify prover in Definition [3. to emphasize that transcripts can be "collected" independently of the honest prover (see complete- ness in Definition 2.2), and in fact can collected "in advance" prior to learning (see Figure 2 As long as the generator is fully supported on honest transcripts, it can be used for Transcript Learning as depicted in Algorithm|] aand Figure
TL trains a Self-Proving model by autoregressively optimizing towards generating accepting tran- scripts. At high level, works by repeatedly sampling x ~ μ and y x* ~ Txx),, and updating the logits log Pe towards agreeing with y TT" via Gradient Ascent. While TL does not directly estimate the Verifiability gradient Vovery (f), we are able to show that it estimates gradient of lower- bounding function A(0) < very (0). Therefore, as it ascends the gradient, it optimizes very (0) via the surrogate. Formally, the lower-bounding function A(0) is the agreement of the transcripts generated by the current model Ps. with the transcripts generated by the honest transcript generator. That is, A(0)= == Pr(sT = π') where the probability over x ~ μ4, Fg ~ T (xx), and R* ~ (T))..
AA query generator Va corresponding to V takes as input partial interaction and samples from the dis- tribution over next queries by V. Formally, for any < R, given input x, output y, and partial interaction (g, a.)=1 V,(2, y, Q1, 01.--., Ir, (r) is a random variable over E For completeness' sake, we can say that when prompted with any sequence z that does not encode an interaction, V2(2)) fully supported on a dummy sequence 1... ..... E Lbg
5

---

Algorithm 1: Transcript Learning (TL)
Hyperparameters:
Learning rate À E (0. 1) and number of samples N N.
Input: An autoregressive model family (Po) foeas, verifier specification (code) V. and sample access an imput distribution js and an accepting transcript generator (+).)
Output: vector of parameters 0 E R
Initialize 0g = 0.
for i = ., N
do Sample x ~ μ and π -² (y" qi aj.- foreach Round of interaction
0, Th. (n))
(T)).. Denote dg := y²
do Let (r) denote the indices of the nThh answer a, in n", and let Tea denote the prefix of the partial transcript (y, qi, aj. ai....,, ..)).
for & E S(r do Compute
Forwards and backwards pass
a,(O,)= = Pr
10 =T
a~po (wT)cc)
d0,) = Vo log Cr (0:) Vo log
Pr
(0 nT/
omppo (aTT
Update
0i+1 == 0 A
II
(.))
Σ
d.().).
rE[n]uç(} *ES(r)
( .ES(r)
Output 0 = N EiEMM Oz.
Lemma 3.2 (TL gradient estimation). Fix an input distribution i over Σ* and a verifier with round complexity I and answer length La. Fix honest transcript generator Tý. Let 0 denote the parameters of the model Po. let A()) be as defined above and let the terms S(r), (o))), and (0) be as defined in Algorithm Then,
VA(0)-
E and
II (1)
de(0) ({))
Σ
rE(R]u(0) sES(r)
eES(r)
The proof is deferred to Appendix [.2 Note that Lemma 3.2 is true for any model Pg. Moreover, the random vector over which the expectation is taken (in the right hand side) is precisely the direction of the update performed Algorithm Section 4 bounds for TL under certain conditions.
we will use Lemma 3.2 to prove convergence
3.1.1 Access Accepting Transcripts
As mentioned, Transcript Learning relies on access to accepting transcripts. In this section we discuss how such access can be realized (grounded in the theory of Interactive Proofs).
Doubly-Efficient Interactive Proofs. When the honest prover P is efficient (polynomial time), the learner (who has the code for p and V) can execute p on input I to collect accepting transcripts-asumini no distribution shift at inference time. This setting is formalized by the notion of CouullyEffficier Interactive Proofs (DEIPs), introduced in the foundational work of Gollwasser al. [2013], who construct DEIPs for all problems computable by log-space uniform families of polynomial-size circuits with polylogarithmic depth. Their protocols ensure that the verifier runs in nearly linear time, while the prover operates in polynomial time or more generally, in time pro- portional to the circuit size. Later, Reingold et al. [2016] showed that any problem computable by a Turing machine running in polynomial time and sublinear space admits a constant-round DEIP. Subsequent theoretical works (e.g., Goldreich and Rothblum 2018a b) have constructed DEIPs for specific problems, while applied works (e.g., ZZhng et al. 2021 Thaler 2013) have improved the time and space complexity of such protocols in practice.

---

Phase 1: Collect honest transcripts
Phase 2: Transcript Learning
For each honest transcript n²: For each honest transcript prefix Tes!
Iuput distribution
x
y
41
a1
qR
ag
Honest Leanstript prefix
Next
Homest Prover
Verifecation Algorithm
Self-Proving Autoregreeive Model
Forwards pass
P
6a
Logit
a,(0) = (x) =
P
logit
accept
x²
yz
qi
a
q
Backwards pass d,(0;) = VelogP(Po = =x]]
N
yM
Update params 0t11 + 8, +
a (,)))) _
-.
Figure 2: Transcript Learning, visualized. To understand Algorithm 1 consider the above visu- alization. In Phase 1, .N honest transcripts collected by interacting honest prover with the Verifier; these serve as samples from the transcript generator (z)).. Phase 2 runs Algorithm [ for each transcript x" (lines 2-3) and each prefix (lines 4-6), the values (0:) and di (0:) are computed via forward and backward passes (line 7), followed by parameter update (line 8).
Backward Data Generation. Recent works on "AI for advanced mathematical problems" [Char- ton et al. | et al.] [2024] propose to reverse the generation process of croblem-solution pairs as follows: rather than sampling problems and searching for solutions, one first samples so- lutions and then constructs the corresponding problems. In our setting, this inspires the following approach. Suppose computationally hard the worst case to start with the input and generate an accepting transcript or first sample a transcript x and then extract the input x for which π is an accepting transcript? As long the resulting x's distributed the same inference time, this would enable Transcript Learning of such instances.
(y, Q1, ......:: qn, aR) for x. Could we instead jointly sample (æ;, T),
We explain the idea further with cryptographic example. Setting up a Lifie-Hellman key- exchange scheme for security parameter 1º requires producing as a public parameter a prime p in factored form, namely erally hard. Instead, one could go "backwards:" first generate (p 1) in factored form by choosing primes q and exponents a; [Kalai] 2003) and then testing if + IIg; d is prime. By the prime number theorem, p is likely be prime after few attempts. In the context of our paper, one may ask Self-Proving model to produce certified primes, training it on tuples (xr p. a (q,, a4).)
1 = IIg; "N where qi are primes. However, factoring (p - 1) is gen-
3.2 Reinforcement Learning from Verifier Feedback (RLVF)
As mentioned in Section 3.1 Transcript Learning uses access to an honest transcript generator to estimate gradients of (a lower bound on) the Verifiability of model Pg. Next we present Reinforce- ment Learning from Verifier Feedback (RIVF, Algorithm 2h. which estimates this gradient without access transcript generator.
Note that 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 the transcript was accepted by V. This useful practice (e.g. when using neural models) as backwards passes
computationally expensive than forwards passes.
On the other hand, this means that RLVF requires the parameter initialization 0g to have Verifiability bounded away from 0, so that accepting transcripts are sampled with sufficient probability. Fortu- nately, such a Self-Proving base model can be learned using TL. This gives a learning paradigm in which somewhat-Self Seeewhaat-Sef-Prvviinn Proving base model is learned with TL (with Verifiability 8 > 0), and
7

---

Algorithm 2: Reinforcement Learning from Verifier Feedback (RLVF)
Hyperparameters: Learning rate À E (0. 1) and number samples N N. Input: An autoregressive model family {P' foeas, initial parameters 0 E Rd verifier specification (code) V, and sample access to an input distribution Output: vector of parameters 0 Rd
for i .N do
Sample ~ μ. Initialize og == Pe. (z).
foreach Round of interaction 1,... do Sample the ymh query
# Emulate the verifier
9r Vg 00, ............... 10.......,........ 11
Sample the nth answer
# Forwards pass
a, ~ Po. (0, .1.
91,
Let Tr == (oo, Q1, ar 1. for [L, do
Let dr,s denote the th token in dr- Compute
Backwards pass
(..) = Vo log ampe, (MT,))
Pr
10 ar,s).
if V1, ",, ,,, an) accepts then Update
01+1 = 0; A
Σ
d....).
(E(R)
(E(La)
Output 0 N EiEIN O,.
then "amplified" to fully Self-Proving model using RLVF. This can be seen as an adaptation of the method of Nair et 2018 the setting of Self- Self-Proving models.
When comparing Algorithms | and 2 we see that the latter (RLVF) does not keep track of the prob- abilities 0gg. This is because, in RL terms, RLVF is on-policy algorithm; it generates transcripts using the current learned model, unlike TL that samples them from a distribution whose parameter- ization is unknown to the learner. Hence, the update step RLVF is simpler than TL.
We show that the update step in RLVF maximizes the Verifiability of Pg-
Lemma 3.3 (RLVF gradient estimation). Fix an input distribution μ over Σ' and a verifier V with round complexity R. and answer length La- For any transcript (x, 3. "...9....... ax) we let Accy (z, y, ......,ap.. denote the indicator random variable which equals if and only if V ac- cepts the transcript. For any model Po, denote by ver(f) the verifiability of Po with respect V and μ. (Definition 2.4 Then, for any 0,
V Vover(()
E arouu y- Po (ge.
Accy RR)
d.())
EE (R BE [L(
where (gr, R as in lines 5-6 of Algorithm 2 and d,()) is defined in line 8 therein.
Note that, because A-cy(.) is 0-1 indicator of whether a transcript was accepted, then the right hand side of the above equation precisely the direction of the step taken in RLVF (line 9). The proof of Lemma 3.3 can be found in Appendix D.3

---

4 Convergence of Transcript Learning
As an application of Lemma 3.2 we prove that, under certain conditions, Transeript Learning (TL, Algorithm T is expected to output a Self-Proving model. While the theorem relies on simplifying assumptions such as convexity and Lipschitzness, offers clean mathematical guarantees that illu- minate the core dynamics of Transcript Learning. As we discuss following the theorem statement, such conditions are common in theoretical machine learning literature, allowing us to build intuition when the assumptions may not hold in practice.
Theorem 4.1 (informal). Fix verifier V. an input distribution μs, and an autoregressive model family {Po)oe Fix an honest transcript generator Tv. Assume the following:
1. The agreement A(0). informally defined the probability that Pe generates transcripts agreeing with Tý, is concave in 0. Additionally, the logits of Po are Stip-Lipschit in 6.
2. There exist parameters 9" with ||0 S BNorm such that Po- is (1 - --/2)- Proving.
3. The number of tokens sent by the prover in the proof system is at most C.
Then, in expectation, TL run on O Borm Blip/ samples outputs (1-s)-Self Proving model.
The full statement and proof of Theorem 4.1 are deferred to Appendix D.4] Its conditions can be split into two parts. First (item 1), convexity and Lipschitzness, which are simplifying assumptions commonly needed to prove SGD convergence. While convexity does not hold in general for DNNs, analyzing convex settings provides clean mathematical tools for establishing foundational results- an approach commonly used in ML theory, particularly for DNNs. Indeed, several works have addressed the problem proving convergence without convexity [Du et al. 2019 Bartlett et al. 2006 Khaled and Richtárik 2023).
Norn-boundedness (item 2), on the other hand, (necessary) realizability assumption: if the architecture {o oo cannot be instantiated with parameters 0", then it cannot be trained to be Self- Proving- This assumption well well-grounded for transformer architectures, as recent theoretical work has established their completeomplesenesss (Bhattamishra et al. 2020 Dehghani et al. 2019].
Finally (item 3), the bound C on the communication complexity of the prover the Interactive Proof system. This parameter directly affects the efficiency of TL, as reflected in the number of iterations (and sampled transcripts): depends on both the optimization landscape complexity B Bpsp /
and the communication complexity C Reducing communication has long been a central objective in the study of proof systems (e.g., Goldreich and Håstad 1998 Goldreich et al. [2002] Reingold jet al. 2016). Theorem 1.1 formalizes how communication -ffiiiiennefii proof systems improve the per- formance of Self Belf-Proving models.
Remark 4.2 (Towards convergence theorem for RLVF). 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 al. 1999| for verifier- induced reward. Convergence bounds for Policy Gradient methods are a challenging and active area of research (e.g. Agarwal et al. 2021), and so we leave the full analysis to future work.
5
Conclusions
Trust between learned model and its user is fundamental. Interactive Proofs [Goldwasser et al.) 1985) provide a general framework for establishing trust via verification algorithms. This work shows that models can be trained to formally prove their outputs within such systems-we call these Self-Proving models. Self-Proving models connect the theory of Interactive Proofs with the goal of Trustworthy ML: they offer formal worst-case soundness guarantees; enabling users to be confident when their models generate correct answers- and detect incorrect answers with high probability.
We support our definition with two general-purpose training methods: Transcript Learning (TL) and Reinforcement Learning from Verifier Feedback (RLVF), whose analyses draw on learning theory. RI., and computational complexity. This work can be extended in several directions: finding conditions for the convergence of RLVE, improving sample complexity bounds for TL., or designing altogether different learning algorithms (e.g., by taking advantage of properties of the verifier).

---

Acknowledgments and Disclosure of Funding
We grateful to Micah Carroll, Mark Rofin, Avishay Tal, Mojtaba Yaghoobzadeh and anonymous reviewers for their helpful comments. This research was supported by DARPA-TAI under grant no. HR00111950076, and by the Simons Collaboration on the Theory of Algorithmic Fairness.
References
Alckh Agarwal, Sham M. Kakade, Jason D. Lee, and Gaurav Mahajan. On the theory of policy gradient methods: Optimality, approximation, and distribution shift. J. Mach. Learn. Res., 22: 98:1-98:76, 2021. URLpttpp//jmmrr httg:/apprs/v22////
v22////7222/ html
Alberto Alfarano, François Charton, and Amaury Hayat. Global Iyарunov functions: a long- standing open problem in mathematics, with symbolic transformers. In Amir Globersons, Lester Mackey, Danielle Belgrave, Angela Fan, Urrich Paquet, Jakub M. Tomczak, and Cheng Zhang, editors, Advances in Neural Information Processing Systems 38: Annual Conference on Neu- ral Information Processing Systems 2024, NeurlPS 2024, Vancouver, BC, Canada, December 10 15, 2024, 2024. URL http: /app:://apppraaaee nips wwwp:ccc.ppppp....e.eepppppppppe files/papellee httpppppp2///aaa////ee www.aabb--bbsttatt--Coooo
.hmml
Cem Anil, Guodong Zhang, Yuhuai Wu, and Roger B. Grosse. Learning to give checkable answers URL https://aaxiv..r abs/
with prover-verifier games. CoRR, abs/2108. 1122100811099 2099, 2021.
2108. 12099
Peter L Bartlett, Michael Jordan, and Jon D McAuliffe. Convexity, classification, and risk bounds. Journal of the American Statistical Association, 101(473): 2006.
E. Bezout. Theorie Generale Des Equations Algebriques. Kessinger Publishing, 1779. ISBN 9781162056128 URL hwtph:://toookke google co. wtt.:iiooooo.dddd/ssssw...cc.ee
Satwik Bhattamishra, Arkil Patel, and Navin Goyal. On the computational power of transform- and its implications in sequence modeling. In Raquel Fernández and Tal Linzen, editors, Proceedings of the 24th Conference on Computational Natural Language Learning, CoNLL 2020, Online, November 19-20, 2020, pages 455-475 Association for Computational Linguis- tics, 2020. doi: 01.18653/V1/2020.0OM 1.37. URL hhttps://doi. org/ (8653/v1/ conl.c.o1
Jonah Brown-Cohen, Geoffrey Irving. and Georgios Piliouras. Scalable AI safety via doubly- efficient debate. In Forty-first International Conference on Machine Learning, ICML 2024, Vi- enna, Austria, July 21-27, 2024. OpenReview.net, 2024. URL httph: htttps://oppnrevieee net/
jorumiid==jmdOTRn
François Charton. Can transformers learn the greatest common divisor? In The Twelfth Interna- tional Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 6-11, 2024.
OpenReview.net, 2024.
Francois Charton, Amaury Hayat, and Guillaume Lample. Learning advanced mathematical com- putations from examples. In International Conference on Learning Representations, 2021. URI
https://openrevier www.:/eeeeeeeeeeeeee http://drudmd-d---/ gfSSSOXXKK
Paul F. Christiano, Jan Leike, Tom B. Brown, Miljan Martic, Shane Legg, and Dario Amodei. Deep reinforcement learning from human preferences. In Isabelle Guyon, Ulrike von Luxburg. Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Gar- nett, editors, Advances in Neural Information Processing Systems 30: Anmual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA. USA, pages
2017. URL ttttps::/proceedingg pewprcceeinng..euurie. neurips cc/ hacp/papr//// Shaper/2011 2017 20122001////// h dbse20adddd5009119111. 200.000412224000044443 haw.boeceeeee---Abbaaa........ Abstract. html
Anne Condon and Richard J. Lipton. On the complexity of space bounded interactive proofs (ex- tended abstract). In 30th Annual Symposium on Foundations of Computer Science, Research Triangle Park, North Carolina, USA, 30 October- I November 1989, pages 467. IEFE Com- puter Society, 1989. doi: 10. 109/SFCS. 1989.13199996,9.9.9. URL/sttps: /oii org/ /0rgg//0..0 10. 1109/ SFCS.
1989. 63519
10

---

Anne Condon, Joan Feigenbaum, Carsten Lund, and Peter W. Shor. Probabilistically checkable debate systems and nonapproximabilit of pspace-haa hard functions. Chic. Theor. Comput. Sci., 1995, 1995. Uttphtp::////// / cs. uchicago.......
.ttm html
Mostafa Dehghani, Stephan Gouws, Oriol Vinyals, Jakob Uszkoreit, and Lukasz Kaiser. Universal transformers. In 7th Interational Conference on Learning Representations, ICLR 2019, New Orleuns, LA, USA, May 6-9, 2019. OpenReview.net, 2019. URL helL:hhts///pppo https://oppeeeeeieer / Beerumidd-yzdRRaln
Simon S. Du, Jason D. Lee, Haochuan Li, Liwei Wang, and Xiyu Zhai. Gradient descent finds global minima of deep neural networks. In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning. ICML 2019, 9-15 June 2019, Long Beach. Califormia, USA, volume 97 of Proceedings of Machine Learning Research, pages 1675-1685, PMLR, 2019. URL http::ttt:/erre http:://proceeddnggg mlr wwwps/v97 /ttp////d////////// html
Simon Frieder, Luca Pinchetti, Alexis Chevalier, Ryan-Rhys Griffiths, Tommaso Salvatori, Thomas Lukasiewicz, Philipp Petersen, and Julius Berner. Mathematical capabilities of chatgpt. In Al- ice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine, editors, Advances in Neural Information Processing Systems 36: Annual Conference on Neu- ral Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December //ash//
10 16. 2023, 2023. URL http:: nips httpp/pppe.eeeepppppeeeee//////e 581 (61166a9994666663337777000--- aatpsp/peeecccooeeeaaaaaataaaaaa Datasets and _at___and__Beearrseeeeeeee html
Oded Goldreich. Probabilistic proof systems: A primer. Found. Trends Theor. Comput. Sci., 3(1): 1-91, 2008. doi: 1..5661/0400000023. URL http::ttt///ot wtt.://0...111000000000000000000
Oded Goldreich and Johan Håstad. On the complexity of interactive proofs with bounded commu- nication. Inf. Process. Lett.. 67(4) 1998. doi: 10. 00100066502200099099880000 000101661)00011111101011 URL
https:///oi. org/10 10.
Oded Goldreich and Guy Rothblum. Counting t-cliques: Worst-case to average-case reductions and direct interactive proof systems. In 2018 IEEE 59th Annual Symposium on Foundations of Computer Science (FOCS), pages 77-88, 2018a. doi: 10.1109/FOCS RTR.OCCSS......00 2018.00017.
Oded Goldreich and Guy N. Rothblum. Simple doubly-efficient interactive proof systems for locally-characterizable sets. In Anna R. Karlin, editor, 9th Innovations in Theoretical Com- puter Science Conference, ITCS 2018, January 11-14, 2018, Cambridge, MA, USA, volume 94 of LIPIcs, pages 18:1-18:19. Schloss Dagstuhl Leibniz-Zentrum für Informatik, 2018b. doi: 10.4230/LIPICSS TTC. URL httpp: 11t ITCS 2018. 18
Oded Goldreich, Salil P. Vadhan, and Avi Wigderson. On interactive proofs with laconic prover. httts:/s::/ddo
Comput. Complex., 11(1-2):1-55 2002. doi: 10.1007/5000037-00--011 org//10 orgg/0..007//s0e 1101100000//0000700000-----1
Shafi Goldwasser, Silvio Micali, and Charles Rackoff. The knowledge complexity of interactive proof-systems (extended abstract). In Robert Sedgewick, editor, Proceedings of the 17th Annual ACM Symposium on Theory of Computing, May 6-8, 1985, Providence, Rhode Island, USA, pages 291-304. ACM, 1985. doi: 10.1145/22145.22178 URL URLhtttps://dot org/ 10. 221452 22178
Shafi Goldwasser, Dan Gutfreund, Alexander Healy, Tali Kaufman, and Guy N. Rothblum. Ver- ifying and decoding in constant depth. In David S. Johnson and Uriel Feige editors. Pro- ceedings of the 39th Annual ACM Symposium on Theory of Computing, San Diego California, USA, June 11-13, 2007, pages 440 449. ACM, 2007. doi: 10.1145/15079001255555 URL https://doi.. org/ 10. 0045/11500999 1250790.0099 1250855
Shafi Goldwasser, Yael Tauman Kalai, and Guy N. Rothblum. Delegating computation: Interactive proofs for muggles. J. ACM, 62(4):2::1-27:64, 2015. doi: 10.1145/2699436. URL https:
//doi.org/10 10. 1145/2699436
Shafi Goldwasser, Guy N. Rothblum, Jonathan Shafer, and Amir Yehudayoff Interactive proofs for verifying machine learning. In James R. Lee, editor, 12th Innovations in Theoretical Com- puter Science Conference, ITCS 2021, January 6-8, 2021. Virtual Conference, volume 185
11

---

of LIPles, pages 41:1-41:19. Schloss Dagstuhl Leibniz-Zentrum für Informatik, 2021. doi: httpt::t//ooott /tt.:///....../....222.../...... ITCS.2021.44.......
10.4230/LIPICSITCS ITC..
Thomas Gransden, Neil Walkinshaw, and Rajeev Raman. SEPIA: search for proofs using inferred automata. In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction CADE-25 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceed- ings, volume 9195 of Lecture Notes in Computer Science, pages 246-255. Springer, 2015. doi: 10. 10.1007/978-3-331 3-1---33-11--2-1------ 16. URL 16
Lewis Hammond and Sam Adam-Day. Neural interactive proofs. In The Thirteenth International Conference on Learning Representations, ICLR 2025, Singapore, April 24-28, 2025. OpenRe- view.net, 2025. URL httphtt://ppppeeeiiiieeee
www.eewww.eeeeeeeeeeeeeeeeeeeeee wwt. net//oorumiddRR234chaa
Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the MATH dataset. In Joaquin Vanschoren and Sii-Kit Yeung, editors, Proceedings of the Neural Information Process- ing Systems Track on Datasets and Benchmarks I, NeurlPS Datasets and Benchmarks 2021, De- cember 2021, httppp//w//s//e/o///c///////////
heerrreeeeenn....oo...oeeeeeee.e neurips. html
Geoffrey Irving. Paul F. Christiano, and Dario Amodei. Al safety via debate. CoRR, abs/aabssso.// 100.00899,
2018. URL http: hwtp://ogg/ab///aeeeee 00899
Adam Tauman Kalai. Generating random factored numbers, easily. Journal of Cryptology. 16(4):
287-289, 2003.
Ahmed Khaled and Peter Richtárik. Better theory for SGD in the nonconvex world. Trans. Mach. Learn. Res., 2023, 2023. URL /RLiittps://openreiiiee http://.w....eeooooorraaaaaaaaaa
Jan Hendrik Kirchner, Yining Chen, Harri Edwards, Jan Leike, Nat McAleese, and Yuri Burda. Prover-verifice games improve legibility of LLM outputs. CoRR, abs/2407. 13692, 2024. doi: (0.48550/ARXV..40...0 13692. /ttpss//://aai org/10. /0 48550/arXiv 2407 13692
Donald E. Knuth. The Art of Computer Programming, Volume II: Seminumerical Algorithms. org.oolggcco.oooooooooooooo
Addison- Aadison-Wesley, 1969. ISBN 0201038021. URL
310551264
Pawel Ladosz, Lilian Weng, Minwoo Kim, and Hyondong Oh. Exploration in deep reinforcement learning: A survey, Inf. Fusion, 85:1-22, 2022. doi: 1..0166).NNFFUUSS22220000000 URL 2022.03.00 003
https://dol: org/10.1016/6.
Nathan Lambert, Jacob Morrison, Valentina Pyatkin, Shengyi Huang, Hamish Ivison, Faeze Brah- man, Lester James V. Miranda, Alisa Liu, Nouha Dziri, Shane Lyu, Yuling Gu, Saumya Malik, Victoria Graf, Jena D. Hwang, Jianjjang Yang, Ronan Le Bras, Oyvind Tafjord, Chris Wilhelm, Luca Soldaini, Noah A. Smith, Yizhong Wang, Pradeep Dasigi, and Hannanch Hajishirzi. Tülu 3: Pushing frontiers in open language model post-training CoRR, abs/2411..5 2024, doi: 2411. 15124
10.4550/ARXI22411..555
URL httts://///doo http///../.../////
Nayoung Lee, Kartik Sreenivasan, Jason D. Lee, Kangwook Lee, and Dimitris Papailiopoulos. Teaching arithmetic to small transformers. In The Twelfth International Conference on Learn- ing Representations, ICLR 2024, Vienna, Austria, May 6-11, 2024. OpenReview.net, 2024.
Hunter Lightman, Vineet Kosaraju, Yura Burda, Harrison Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe. Let's verify step by step. In The Twelfth International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 6-11, 2024. OpenReview.net, 2024.
Shikhar Murty, Orr Paradise, and Pratyusha Sharma. Pseudointelligeene:: A unifying lens on lan- guage model evaluation. In Houda Bouamor, Juan Pino, and Kalika Bali, editors, Findings of the Association for Computational Linguisties: EMNLP 2023, Singapore, December 6-10, 2023, pages 7284-7290. Association for Computational Linguistics, 2023. doi: 10. 10.18653/V1/2023. FINDINGS- PENIGGS-EMNPPP.... URL. httpps:/dooi ftaap:://doi.or//00/ 18653/v1 102/2222222222 ff findings-enmin
485
12

---

Ashvin Nair, Bob McGrew, Marcin Andrychowicz, Wojciech Zaremba, and Pieter Abbeel. Over- coming exploration in reinforeement learning with demonstrations. In 2018 IEEE International Conference on Robotics and Automation, ICRA 2018, Brishane, Australia, May 21-25, 2018, pages 6292-6299. IEFE, 2018. doi: 10. N0.110//CCAA22118844665
URL https::/tp//oo //rg/ org/
10. 1109/ ICRA.//CR.... 2018. 8463162
Long Ouyang, Jeffrey Wu, Xu Jiang, Diogo Almeida, Carroll L. Wainwright, Pamela Mishkin, Chong Zhang, Sandhini Agarwal, Katarina Slama, Alex Ray, John Schulman, Jacob Hilton, Fraser Kelton, Luke Miller, Maddie Simens, Amanda Askell, Peter Welinder, Paul F. Christiano, Jan Leike, and Ryan Lowe. Training language models to follow instructions with human feedback. In Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh, editors, Advances in Neural Information Processing Systems 35: Annual Conference on Neural Infor- mation Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 De- cember 9, 2022, 2022. URL http://papers mips cttppp/ppreeppppppppppppppppp faaesperrffes/ggeeeeee www.fflllefpeeeeee wwwps//papee//////aaaaaaaaa
html
Orr Paradise. Smooth and strong peps. Comput. Complex. 30(1):1, 2021.
doi: 10.1007/
500037-020-0019993. URL
Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving.
CoRR, 0tts/2009003393, 2020. htw.httpp///rrii.rrr//b/b/////
200///99000003333333 03393
Valentina Pyatkin, Saumya Malik, Victoria Graf, Hamish Ivison, Shengyi Huang, Pradeep Dasigi, Nathan Lambert, and Hannaneh Hajishirzi. Generalizing verifiable instruction following. CoRR, abs/2507.028333 2025. doi: 1044550/ARXIV2550..0055 48550/arXiv. 2507 02833
URL https://doi. http///oo.orr/////////
Omer Reingold, Guy N. Rothblum, and Ron Rothblum. Constant-roumd interactive proofs for delegating computation. In Proceedings of the 48th Annual ACM SIGACT Symposium on Theory of Computing (STOC), pages 49-62, 2016. doi: 10.1145/2897518 28877999.
Bernardino Comera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M Pawan Kumar, Emilien Dupont, Francisco JR Ruiz, Jordan S Ellenberg, Pengming Wang, Omar Fawzi, et al. Mathematical discoveries from program search with large language models. Nature, 625(7995)4468 475, 2024.
Guy N. Rothblum, Salil P. Vadhan, and Avi Wigderson. Interactive proofs of proximity: delegating computation in sublinear time. Dan Boneh, Tim Roughgarden, and Joan Feigenbaum, editors, Symposium on Theory of Computing Conference, STOC" 13, Palo Alto, CA, USA, June 1-4, 2013, pages 793-779--00 ACM, 2013. doi: 10.1145/2488008222 2488779
URL https:://oi. org.
1145/2488608. 2488709
Shai
Shalev-Shward and Shai Ben-David. From Theory to Algorithms.
Understanding
Machine Learning ISBN
Cambridge University Press, 2014.
978-1-10-7057135..
URL. http://www. cambridge org/ /e/ de/academic/
sub att.atts/mmmprrrrrrccaaaaatteeee
Adi Shamir. IP = PSPACE. J. ACM, 39(4):669 877, 1992. doi:
URI.
https://doi. 1145/146558 146609
Zirui Song, Guangxian Ouyang. Mingzhe Li, Yuheng Ji, Chenxi Wang. Zixiang Xu, Zeyu Zhang, Xi- aoqing Zhang, Qian Jiang, Zhenhao Chen, Zhongzhi Li, Rui Yan, and Xiuying Chen. Maniplvm- rl: Reinforcement learning for reasoning in embodied manipulation with large vision-language models. CoRR, abs/2505. 16517, 2025. doi: 10.48550/RXXI.2555.. 16517. URL. https: atfoi.org//0..oo 48550/ arXiv 2505. 16517
Richard Sutton, David A. McAllester, Satinder Singh, and Yishay Mansour. Policy gra- dient methods for reinforcement learning with function approximation. In Sara A. Solla, Todd K. Leen, and Klaus-Robert Müller, editors, Advances in Neural Information Process- ing Systems 12, INIPS Conference, Denver, Colorado, USA, November 29 December 4, 1999], pages 1057-1063. The MIT Press, 1999. URI. http: httt:::/ppapeese nips. cc/paper/ with-withhteet htw.
13

---

Oyvind Tafjord, Bhavana Dalvi, and Peter Clark. Proofwriter: Generating implications, proofs, and abductive statements over natural language. In Chengqing Zong, Fei Xia, Wenjie Li, and Roberto Navigli, editors, Findings of the Association for Computational Linguisties: ACI/LICNLP 2021, Online Event, August 1-6, 2021, volume ACL/IICNIPP 2021 of Findings of ACL., pages 3621-3634. Association for Computational Linguistics, 2021. doi: 10. 10.18653VV//021. SUIDINGS-ACL.111 URL WtRL/ttps:/// /stpp://doi..oom org/10 wtt.a//.....11111111/1 18653/v1/2021 wwndiniinnnaaiaa accpaggs-ccc...... ac1.311 317
Justin Thaler. Time-optimal interactive proofs for circuit evaluation. In Ran Canetti and Juan A. Garay, editors, Advances in Cryptology CRYPTO 2013, pages 71-89, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg.
geometry Trieu H. Trinh, Yuhuai Wu, Quoc Le, He He, and Thang Luong. Solving geomerry with- out human demonstrations. Nut., 625(7995):476-448, 2024, doi: 10. 10.108/541588--0246667711 URL https://doi. org/10 1038/ 0008//415580 44188- 023-06747-355
Miles Turpin, Julian Michael, Ethan Perez, and Samuel R. Bowman. Language models don't always say what they think: Unfaithful explanations in chain-of-thought prompting. In Al- ice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine, editors, Advances in Neural Information Processing Systems 36: Annual Conference on Neu- ral Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 16, 2023, 2023. URL http: htwp:p//ppppp....eeee nips wwtpapprppppiieeeepc faapperrflllseeeeeeeeeeeeeeeeese pwtpppppppp///aaaaeeeppppeeeeeee -bstaa--t-bbttatttt---eeea
html
Jonathan Uesato, Nate Kushman, Ramana Kumar, H. Francis Song, Noah Y. Siegel, Lisa Wang, Antonia Creswell, Geoffrey Irving, and Irina Higgins. Solving math word problems with process- and outcome-based feedback. CoRR, 14225, 2022. doi: (0.4855/ARXXV2221..4777 URL wwtphhttt////..... org/ 48550/ 2211. 14275
Leslic G. Valiant. A theory of the Icarnablc. Commun, ACM, 27(11):134-1142, 1984. doi: 10. 1145/1968. 1972. URL htttp:://dol ort.:ii..rg/1.... 11tg///0.114/9968... 1972
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention all you need. In Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Ro- man Garnett, editors, Advances in Neural Information Prucessing Systems 30: Annual Con- ference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA, pages 5998-6008, 2017. URL //tooceei/// neurips cc/ cc/paper//2017/ Abstract html
hash haaah//56e22444777211100000003.3
Stephan Wäldchen, Kartikey Sharma, Berkant Turan, Max Zimmer, and Sebastian Pokutta. Inter- pretability guarantees with Merlin-Arthur classifiers. In Sanjoy Dasgupta, Stephan Mandt, and Yingzhen Li, editors, Proceedings of The 27th International Conference Artificial Intelligence and Statistics, volume 238 of Proceedings of Machine Learning Research, pages 1963-1971. PMLR, 02-04 May 2024. URL https::/proceediee html
mlr. press/ paress/v338/l v238/ hal////adccee22..m.m www.mmlr...........
Boshi Wang, Xiang Yue, and Huan Sun. Can chatgpt defend its belief in truth? evaluating LLM reasoning via debate. In Houda Bouamor, Juan Pino, and Kalika Bali, editors, Findings of the
Association for Computational Linguisties: EMNLP 2023, Singapore, December 6-10, 2023, pages 11865-11881 Association for Computational Linguistics, 2023. doi: 10. 10.18653/11/0033 FINDINGS BANDINGS-EMNLP775S EMNLP,795. URL https://doi. org/10. 186..011/113332222 findings-emmann
795
Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Brian Ichter, Fei Xia, Ed H. Chi, Quoe V. Le, and Denny Zhou. Chain-of- prompting elicits reasoning in large language models. In Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh, editors, Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NewrIPS 2022, New Orleans, LA, USA, November 28 December 9, 2022, 2022. URL URL http: http::://apppeepeeeeee mipperrs.ipssee wwtpppprrcppppe.eppcppe fil.fiieeeeeee wtape//l/eepepaee/222222 pttpp/aapp//////eeeeee http::ppppppppr.sppp..pppppppppp
0166096113544ecf444155ff0f00f333 htg.a//eeeeaaaaaaaoooooooao-aaar html
14

---

Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi, and Yejin Choi. Natural- prover. Grounded mathematical proof generation with language models. In Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh, editors, Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Pro- cessing Systems 2022, NeurlPS 2022, New Orleans, LA, USA, November 28 Decem- www.ff//ppeeeeeeeee/e /
ber 9, 2022, 2022. URL
Fang Wu, Weihao Xuan, Ximing Lu, Zaid Harchaoui, and Yejin Choi. The invisible leash: Why RLVR may not escape its origin. CoRR, abs/2507.14843, 2025a. doi: 10.48550/AXXI.2500. 14843. URL URLhtttss: battps://dos org/10. 48550/arXix 2507 2507.14843
Jialong Wu, Shaofeng Yin, Ningya Feng, and Mingsheng Long. Rlvr-world: Training world models
with reinforcement learning. CoRR, abs/2505.13934, 2025b. doi: 1044850/ARXXV22505...55
URL https://doi. org//o.//1. 48550/ arxiv. 2505 13934
Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu. Saad Godil, Ryan J. Prenger, and Animashree Anandkumar. Leandojo: Theo- rem proving with retrieval-augmentted language models. In Alice Oh, Tristan Nau- mann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine, editors, Ad- vances in Neural Information Processing Systems 36: Annual Conference formation Processing Systems 2023, NeurlPS 2023, New Orleans, LA, USA, December 10 16. 2023, 2023. URL http:: nips watpapperrlleppppppppppppeeeeeee Seapper22000 2203//2222////// //aah//h//// Datasets waandddeeehaarreeeeeeeeaeeeeeeee html
Neural In-
Mengjiao Yang, Dale Schuurmans, Pieter Abbeel, and Ofir Nachum. Chain of thought imitation with procedure cloning. Sanmi Koyejo. S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh, editors, Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurlPS 2022, New Orleans, LA, USA, November 28- December 9, 2022, 2022. URL http: /ttt:::ppappr..s.ttm nips cc/ wwtpapprp_iilaeeeeeeee files/ www.e//ppppe/////// paper/2022/ /ttp:///bbb0001..6ffff2222222262
www.:eo---bbaaatt--oooooeeeeeeee Confreettt-ooffreeeeee html
Jiaheng Zhang, Tianyi Liu, Weijie Wang, Yinuo Zhang, Dawn Song, Xiang Xie, and Yupeng Zhang. Doubly efficient interactive proofs for general arithmetic circuits with linear prover time. In Yongdae Kim, Jong Kim, Giovanni Vigna, and Elaine Shi, editors, CCS '21: 2021 ACM SIGSAC Conference Computer and Communications Security, Virtual Event, Republic of Korea, November 15 19, 2021, pages 159-177, ACM, 2021. doi: 10. 00.114533460120.44447666 URL https: org//oo./110 10. 1145/ 1145/3460120
3460120. 3484767
Sheng Zhang. Qianchu Liu, Guanghui Qin, Tristan Naumann, and Hoitung Poon. Med-rlvr: Emerg- ing medical reasoning from a 3b base model via reinforcement learning. CoRR, abs/2502. 2025. doi: 10448550/ARXIV.2250.1666 URL htttts://doi...oo org. 10 005.44450///// arxiv 2502. 19655]
Jiecheng Zhou, Qinghao Hu, Yuyang Jin, Zerui Wang, Peng Sun, Yuzhe Gu, Wenwei Zhang, Ming- shu Zhai, Xingcheng Zhang, and Weiming Zhang. RI in the wild: Characterizing rivr training in Ilm deployment. arXiv preprint arXiv:2509.25279, 2025.
NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: Definitions are formally stated in the body of the paper. Claims are stated and proven in the paper.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made in the paper.
15

---

The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings.
fine to include aspirational goals as motivation as long as it clear that these goals are not attained by the paper.
2. Limitations
Question: Does the paper discuss the limitations of the work performed by the authors?
Answer: [Yes]
Justification: Limitations are discussed throughout the body and in Appendix
Guidelines:
The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create separate "LLimitatios" section in their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The au- thors should reflect on how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested few datasets with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect on the factors that influence the performance of the ap- proach. For example, facial recognition algorithm may perform poorly when image resolution is low or images are taken in low lighting. Or a speech-to-text system might not be used reliably provide closed captions for online lectures because fails to handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to ad- dress problems of privacy and faimesss
While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't It acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed not penalize honesty concerning limitations.
3. Theory assumptions and proof's
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
Answer: [Yes]
Justification: Definitions and theorems are formally stated and proved. Formal proofs ap- pear in the appendix, with overview and discussion of the theorems in the body of the paper.
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced in the statement of any theo- rems.
The proofs can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged provide short proof sketch to provide intuition.
16

---

Inversely, any informal proof provided in the core of the paper should be comple- mented by formal proofs provided appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental result reproducibility
Question: Does the paper fully disclose all the information needed to reproduce the main experimental results of the paper to the extent that it affects the main claims and/or conclu- sions of the paper (regardless of whether the code and data are provided or not)?
Answer: [Yes]
Justification: Experiments are presented in Appendix with full details needed for repro- ducibility in Appendix G.2
Guidelines:
The answer NA means that the paper does not include experiments.
If the paper includes experiments, a No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is a novel architecture, describing the architecture fully might suffice, or if the contribution is specific model and empirical evaluation, may be necessary to either make it possible for others to replicate the model with the same dataset, provide access to the model. In general. releasing code and data often one good way to accomplish this, but reproducibility can also be provided via detailed instructions for how replicate the results, access hosted model (e.g., in the case of a large language model), releasing of a model checkpoint, or other means that are appropriate the research performed.
While NeurlPS does not require releasing code, the conference does require all sub- missions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution is primarily new algorithm, the paper should make it clear how reproduce that algorithm.
(b) If the contribution is primarily new model architecture, the paper should describe the architecture clearly and fully.
(c) the contribution is a new model (e.g., a large language model), then there should either be way to access this model for reproducing the results or way to produce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case thors are welcome to describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should be possible for other researchers have some path reproducing verifying the results.
5. Open access to data and code
Question: Does the paper provide open access to the data and code, with sufficient instruc- tions to faithfully reproduce the main experimental results, as described in supplemental material?
Answer: [Yes]
Justification: Model, data and code are released in https:///ithuu. htt.ggtttu.cooooooee com/orrp/ self wwt.--proonng-oeee..
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurIPS code and data submission guidelines
for more details.
17

---

While we encourage the release of code and data, we understand that this might not be possible, so "No" an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurIPS code and data submission guidelines (https: //nips. cc/ h
Sww.eddSSuummssssooooooe.. onPolicy) for more details.
The authors should provide instructions on data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. If only subset of experiments reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information as possible in supplemental material (appended to the paper) recommended, but including URLs to data and code permitted.
6. Experimental setting/details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [Yes]
Justification:
Yes, in Appendix G.2.
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of the paper to level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, or as supplemental material.
7. Experiment statistical significance
Does the paper report error bars suitably and correctly defined or other appropri- ate information about the statistical significance of the experiments?
Question:
Answer: [Yes]
Justification: Standard errors are reported.
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by error bars, confi- dence intervals, statistical significance tests, at least for the experiments that support the main claims of the paper.
The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, overall run with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g., Normally distributed errors).
It should be clear whether the eтror bar is the standard deviation or the standard error of the mean.
is OK to report 1-sigma error bars, but one should state it. The authors should prefer- ably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that are out of range (e.g. negative enror rates).
18

---

If error bars are reported in tables or plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables in the text.
8. Experiments compute resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed reproduce the experiments?
Question:
Answer: [Yes]
Justification: Yes, in Appendix G.2
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs as well estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported the paper (e.g.. preliminary or failed experiments that didn't i make it into the paper).
9. Code of ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurlPS Code of Ethics
Answer: [Yes]
Justification:
The research conforms with the code of ethics.
Guidelines:
The answer NA means that the authors have not reviewed the NeurIPS Code Ethics.
If the authors answer No, they should explain the special circumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g., if there is special consid- eration due to laws or regulations their jurisdiction).
10. Broader impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [Yes]
Justification: The paper discusses societal impacts throughout the body. As this is a theo- retical paper, immediate impact is limited.
Guidelines:
The answer NA means that there no societal impact of the work performed.
If the authors answer NA or No, they should explain why their work has no societal impact or why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact spe- cific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and not tied particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
19

---

The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional unintentional) misuse of the technology.
If there are negative societal impacts, the authors could also discuss possible mitiga- tion strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of MI.).
11. Safeguards
Does the paper describe safeguards that have been put in place for responsible release of data models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification:
The experiments on simple arithmetic capability pose no such risk.
Guidelines:
The answer NA means that the paper poses such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by re- quiring that users adhere usage guidelines or restrictions access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards challenging, and many papers do require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Question:
Answer: [Yes]
Justification: Yes, codebases used in the experiments are cited and used under the appro- priate license.
Guidelines:
The answer NA means that the paper does not existing assets.
The authors should cite the original paper that produced the code package dataset.
The authors should state which version of the asset used and, possible, include URL.
The name of the license (e.g., CC-BY 4.0) should be included for each asset.
For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided.
If assets released, the license, copyright information, and terms of use in the pack- age should be provided. For popular datasets, paapeesssppprssssaaas paperswithcode com/ datasets has curated licenses for some datasets. Their licensing guide help determine the li- cense of a dataset.
For existing datasets that are re- re-packaged, both the original license and the license of the derived asset (if has changed) should be provided.
this information is not available online, the authors are encouraged to reach out to the asset's ss creators.
13. New Assets
Question: Are new assets introduced in the paper well documented and the documenta- tion provided alongside the assets?
Answer: [Yes]
20

---

Justification:
The details of the model and data released as a part of this paper are detailed in /tttps://githue com/ cwnm/orrp/seee selff www.-poooviiioooeeeee models
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details the dataset/code/model as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset used.
At submission time, remember to anonymize your assets (if applicable). You can either create anonymized URL or include an anonymized zip file.
14. Crowdsourcing and Research with Human Subjects Question:
For crowdsourcing experiments and research with human subjects, does the pa- per include the full text instructions given participants and screenshots, applicable, well as details about compensation (if any)?
Answer: [NA]
Justification: No human subjects were used.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information in the supplemental material is fine, but if the main contri- bution of the paper involves human subjects, then much detail as possible should be included the main paper.
According to the NeurIPS Code of Ethics, workers involved in data collection, cura- tion, or other labor should be paid at least the minimum wage the country of the data collector.
15. Institutional review board (IRB) approvals or equivalent for research with human subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based the requirements of your country or institution) were obtained?
Answer: [NA]
Justification: NO IRB approval was required.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Depending on the country in which research conducted, IRB approval (or equiva- lent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere the NeurIPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review.
Declaration LLM usage
Does the paper describe the usage of LLMs if is an important, original, or non-standard component of the core methods in this research? Note that if the LLM is used only for writing, editing, or formatting purposes and does not impact the core methodology, scientific rigorousness, originality of the research, declaration is not required.
Question:
Answer: [NA]
21

---

The method development in this research does not involve LLMs as any important, original, or non-standard components.
Justification:
Guidelines:
The answer NA means that the core method development in this research does not involve LLMs as any important, original, or non-standard components.
Please refer to our LLM policy (https://neurips www.e//ceeonnncee/////aa 2005:/cLcce//22/LLL for what should or should not be described.
A Related Work
We overview related work from machine learning (ML) and interactive proof systems (IPs) literature.
ML and IPs. IPss have found numerous applications in ML towards diverse set of goals. Anil et al. (2021) introduce Prover-Verifier Games (PVGs), a game-theoretic framework for learned provers and learned verifiers. Since our paper initially appeared, PVGs were further investigated in at least two subsequent works: HHammond and Adam-Day [2025] study multi-prover and Zero Knowledge variants of PVGs. Additionally, Kirchner et al. (2024) successfully utilize PVGs to- wards obtaining human-legible outputs from LLMs. Notably, they require a relaxed completeness guarantee of their learned proof system-thir requirement is the same as our Definition 2.4of Self- Proving models.
Beyond PVGs, Wäldchen et al. 2024] cast the problem of model interpretability Prover-Verifier interaction between a learned feature selector and learned feature classifier. Debate systems (Con- don al. [995]. a multiprover variant of IPs, were considered for aligning models with human values Irving et al., 2018 Brrwnn et al. [022]]. In such Debate systems, two competing models are each given an alleged answer y * y and attempt to prove the correctness of their an- swer to (human or learned) judge. Lastly, Murty et al. [2023] define Pseudointelligence: model learner LM and an evaluator learner Lg are each given samples from a ground-truth, Las learns model of the ground-truth, while LE 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 manually-defing verifier. More related in this regard is IP-PAC [Goldwasser et al., 202T]. in which a learner proves that she learned a model that Probably Approximately Correct [Valiant 1984]. 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- Self-Proving models are verified by an algorithm with for- mal completeness and soundness guarantees (see Definition 2..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.
AlphaCieometry (Trnn et al., 2024 is capable of formally proving olympiad-level geometry prob- lems: Others have trained models produce proofs in Gransden et al. [2015), Polu and Sutskever (2020) and others train models to produce proof' in Coq [Gransden et al.) 2015). Metamath [Polu and Sutskever 2020). Lean (Yang et al., 2023], or manually-defined deduction rules [Tafjord al.)
2021]: FunSearch Kooerra-Parede et al.) 2024] evolves LLM- -eneraated programs by systemati- cally evaluating their correctness, Indeed, all of these can 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. 2022) 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 Thouugh (CoT, Wei et al. 2022) 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. 2022 or in the training phase itself
(Yang et al. 2022]. Transcript Learning (TI., Section can viewed as training the model on a Chain-of- Teaf-TThoe Thought induced by the interaction of verifier and an honest prover (Definition 2.2
22

---

To complete the analogy, let us adopt the terminology Uesato et al. [2022], who consider outcome supervision and process supervision. In our case, the outcome is the decision the verifier, and the process is the interaction between the verifier and the model. Thus, Reinforcement Learning from Verifier Feedback (RLVE, Section
3.2) is outeome-supervised while TL. is process supeess-upervised. In [2024] find that pmocess-supervisee transformers outperform outcome-
recent work, Lightman et al. supervised ones on the MATH dataset [Hendrycks et al. 2021].
Subsequent work on RLVE. Following the preprint version of this paper on May 2024, Rein- forcement Learning from Verifier Feedback (RLVF, Section (32) has been implemented and widely adopted. Of particular note is RLVR (Reinforcement Learning from Verifiable Reward. Lambert al. 2024), which implements RIVF by adding KI. regularization to the RI. objective Algo- rithm This implementation provided valuable empirical validation and state-of-
perfor- mance on full-scale LLMs, sparked additional empirical analysis [Wu al. 2025a (Zhou et al.) 2025]. and led to widespread adoption across numerous domains including medical reasoning, com- puter vision, and robotics [Zhang et al., 2025 Wu et al., 2025b] Song et al., 2025). Most recently, Pyatkin et al. [2025] presented IFBench which measures performance in interactive (3-round) proof systems. These empirical contributions complement our theoretical foundations, demonstrating the surprising power and applicability of RLVF as practical post-training method.
B
Limitations
First, our current learning methods, each individual ground-truth truth capability requires training separate Self-Proving model. A natural generalization of this approach is to adapt our definition and methods deal with single generalist Self-Proving model that proves its correctness multiple verifiers of different ground-truths.
Moreover, the second strategy presented in Section 3.1.1 namely, generating accepting transcripts first and then constructing matching inputs-has has an inherent limitation: the resulting training dis- tribution biased by the design of the generator. As consequence, models may end up learning patterns of the construction process, rather than acquiring generalizable reasoning capabilities. This highlights the importance of using sufficiently diverse generators, and of evaluating model perfor- mance on out-of distiiibitttttiinnnnn inputs.
C A Definition for General Loss Functions and One-To-Many Relations
We present variants Self-Proving models (Definition 2.4 generalized to one-to-many relations, and general bounded loss functions. While these generalizations provide a richer framework that may accommodate a wider range of applications, the theorems this paper are based on the forgoing Definition 2.4 which captures the essential properties while remaining mathematically manageable.
General (bounded) loss functions. In Definition 2.1 implicitly use the 0-1 loss when measur- ing the correctness of a model: For any x E X, we measure only whether the model generated the correct output y F* (x:), but not how "far" the generated y was from F* (x:). It is often the in machine learning that we would be satisfied with models that generate a "nearly-correct" output. This is formalized by specifying loss function é: Σ* x E* + [0, 1] and measuring the probability that f(r, y) is smaller than some threshold À E [0, 1). where x is drawn from the input distribution μl, and y is generated by the model when given input æ.
In the context of language modeling, different loss function allow for a more fine-grain grained treatment of the semantics of given task. As example, consider the prime-counting task:
Given an integer æ < 10 output the number of primes less than or equal x.
In the notation of Section 2 the prime-counting task would be captured by the ground-truth function (*)x) = hp E N S x, p is prime}|
Per Definition 2.1 any output other than F* (x) is "just as incorrect" as any other. Yet, we might prefer outputs that closer to the correct answer, say, in L, norm. This preference be captured
Formally, the input and output strings in V representing integers (e.g. in decimal representation).
23

---

by the following bounded loss function
1 F (x)] 10-3
if y S 10
(x.
else.
In particular, if we are interested knowing the answer only up to some additive constant C, we could say that an output y is "correct-enough" if & (ar, I C. 10-9.
More generally, relax Definition 2.1 to capture approximate correctness follows.
Definition C.1 (Approximate conrectness). Let be a distribution over input sequences in l" and let l: D' - + [0, 1] be a loss function. For any a, X E [0, 1], we say that model Fo (a, A)- correct with respect to μ if
Pr gr~Fo(s)
((x S Za.
Ome-to-many-rrlation.. In Section 2 we focused on the setting of models a ground-truth func- tion F* Σ" Σ'. That is, when each input has exactly correct output, namely F (x)). A more general setting would be to consider a ground-truth relation L C Σ' x E". Then, we say that y is correct output for x if (x, y) L. Importantly, this allows single have many possible correct outputs, or none at all.
Note that we must take care to choose a loss function E that captures conrectness with respect to the relation L. i... f(x,3) y)
and only if (z. y) E L. Equivalently, any loss function induces a relaxation approximate-coreedt tion C.T already captures the setting of one-to-many relations, since an input x may have multiple y" such that ((2, v²) O.
relation L = {(x,)) y) (( y) 0}. Therefore,
Defini-
C.1 The General Definition
We first present relaxed definition of Interactive Proof systems for verifying approximate- correctness.
Definition C.2 (Definition 2.2 generalized), Fix a soundness error & E (0, 1), a threshold [0, 1). a finite set of tokens Σ. and loss function E: Σ" E* [0. 1]. A verifier V for é with threshold À is a probabilistic polynomial time algorithm that is given explicit inputs x, y E E' and black-box (oracle) query access prover P. It interacts with P over R rounds (see Figure [ and outputs a decision (V, P) (r,y) E (reject, accept). Verifier V satisfies the following two guarantees:
Completeness: There exists an honest prover P such that, for all x, y E E", if () = then
Pr[(V, (z, y) accepts] = 1,
where the probability is over the randomness V.
Soundness:
For all P and for all x, y E 21, if((z,)) > À then
Pr[(V, P) (z, y) accepts] 8,
where the probability is over the randomness of V and P, and is the soundness error.
Indeed, for given ground-truth function F*; Σ* + Σ*, Definition 2.2 can be recovered by choos- ing the 0-1 loss
a + (*)
(x,
else
and any threshold À E 10.
Remark C.3 (Connection Interactive Proofs of Proximity). Definition C.2 can be seen as slight generalization of (perfect completeness) Interactive Proofs of Proximity Ps, Rothblum et al. 2013). An IPP for relation L S. E" Σ" with proximity parameter is obtained by instantiating Definition C.2 with the loss function Hamming defined by
# Us + b
&Hamming (I, 8) min
(x,y") ) L, 18/1 = 1y
M
24

---

that is, &Hammiugg22 (I.y) 3) is the fraction of tokens in that must be changed to obtain an outpur y" with "..y")= E L. However, the motivation of Rothblum al. [2013] was studying sublinear time verification, whereas ours is to relax the requirements of traditional Interactive Proofs towards meeting common desiderata in machine learning.
With this relaxed notion of Interactive Proofs in hand, we are now ready to define Self-Proving models for general (bounded) loss functions.
Definition C.4 (Definition 2.4 generalized). Fix loss function E: E' x Er - [0, 1). verifier
V for l with threshold X [0. 1) as in Definition C.2 and distribution over inputs L. The
Verifiability of a model Pa == " + "** is defined as
verv, (0)
Pr.
[(V, Pa) (2, accepts].
y~PP(a)
We say that model Pg is 3-Self-Proving with respect to V and p if ver v. (0) 2 B.
observe that Verifiability as per Definition C.4 implies approximate- correctness: Suppose Pa is 3-Self-Proving model with respect to a verifier that has soundness error and threshold parameter for loss function é. Then, by union bound,
Analogously to Remark 2.5
Pr moop
[e v) S Aj 2 3 -.
Pa-P(())
Importantly, as emphasized throughout this paper, soundness of V implies that for all inputs x, any output such that ((2, y) > À is rejected with high probability (1 s).
D Formal proofs
Appendix D.I
formally specifies the setup which our results reside. We then prove Lemma 3.2 in
Appendix D.2
Lemma 3.3 in Appendix D.3 and Theorem 4. in Appendix D.4
D.1
Specification of the Learning Model
In this section, we fully specify the theoretical framework in which our results reside. We define learner as an algorithm A with access to family of autoregressive models {Po and samples from the input distribution x p. our setting of Self Proving models (and in accordance with the Interactive Proofs literature), we give the learner the full specification of the verifier V. More formally,
Definition D.1 (Self-Proving model learner). (Self-Proving model) learner a probabilistic ora- cle Turing Machine A with the following access:
A family of autoregressive models {Po where N is the number of parameters in the family. For each 0 and 2 E Σ', the random variable Po(z) is determined by the logits log Pa(z) E R| For any 2 E E' and a E E, the learner A can compute the gradient of the Th logit, that is, Ve log Pro'>pa(=)]o always differentiable in 0.
o'). In particular, log Pro'=pu(=)lo d')
Sample access to the input distribution μ.. That is, A can sample x ~
The full specification of the verifier V, Le., the ability to emulate the verification algorithm V. More specifically, A is able to compute V's decision after any given interaction; that is, given input x, oulput y, and a sequence of queries and answers (gi, a;) R2 the learner A can compute the decision of V after this interaction.
D.2 Proof of Lemma
We let T denote the transcript generator induced by the model Po when interacting with for each x, (x) is the distribution over transcripts of interactions between and Pa on input x. We stress that x² (a)) and æ ~ (xx) are transcripts produced when interacting with the same verifier queries; we can think of the verifier as simultaneously interacting with the honest prover
25

---

and with the model Po In what follows, we use x² ~ TT(()) and a ~ TØ(x) to denote two transcripts that share the same queries. That is, taking x (y" qi aj.aj..... 9 d'p)) denote an accepting transcript sampled from (r),,, and π (v. qi "1.,,,.......... "i,..., IR. an) to denote a random transcript sampled from TV(2), we say that π and x²' agree if they agree on the prover answers, namely if:
(v. an) = (v",
ap).
This definition implicitly uses the independence of the verifier and model's randomness. We now prove that TL correctly estimates the gradient of A(0) in its update step.
Proof of Lemma 3.2 Throughout this proof, expectations and probabilities will be over the same distributions as the lemma statement. First, we use the law of total probability together with the autoregressive property of Pe (Section 3 to switch from probabilities on transcripts, to products of next-token probabilities. Formally, consider a fixed input z, an honest transcript π = (v", qi, ai..... QR. (R), and denote a random transcript sampled from (x(x) when using the same verifier queries by (y, qi a1...., ......,9R: .IR an). For any [R] denote the random variable To. = (v4taa ... a, 14,)) Then,
Pr [ = n
Pr((y: Uly..., aR) = (y* ai n
Pr y~Po(x)
[ = y7
II
Pr [a aT
rE(M]
Pr
II
Pr
lo = m
(3)
g-Pb(x)
a
(
*ES(r)
a=((),
(4)
rE[R] sES(r)
where, noted above, Equation 2 uses the independence of the verifier and model's random-
ness, Equation (3) uses the autoregressive property of P& (Definition D.I), and Equation is by definition of as and of ag. Next, basic calculus identity gives
Ve Pri (Pr(==x*) = x²)) Pr it ==] Ve log (Pr(==
(5)
This implicitly assumes that Pr. [ = "" is differentiable in 0: indeed, this follows from Defini- tion D.I. where the logits of the model were assumed to by differentiable. Let us focus on the rightmost factor. By Equation 4
V log [r -+m==)))=-- x²1)=
V log
II
(0)
Σ rE(R]U(0) sES(r)
Ve log (0)=
Σ d,(0)
rE(B]U(0)
(E(
sES(r)
sES(r)
(6)
where the last equality is by definition of d0))). Combining Equation (4 and Equation gives
Pr (r(T==
II
(
Σ d,) rE SES(r)
sES(r)
By the law of total probability and the linearity of the gradient,
E 2
0 Pr
p-|x==+1]] Vo
E x.
Pr n [-=
Vo
Pr (r](===)) VoA(O). 2, P
Pr
which concludes the proof.
"The way it is presented the algorithm, first the verifier is called by TP and outputs queries .......q.. and then the model is prompted with the verifier queries one a time. This maintains soundness, since proof system is sound as long the prover does not know the verifier's queries in advance.
26

---

D.3 Proof of Lemma 3.3
Recall the manscript generator of Pe. denoted by TV (see Lemma 3.2). By the definitions of Verifi- ability in Definition 2.4 and (ax y. 91..... aR) in the lemma statement,
ver(O)
Pr Pa(x(
[(V, Po) (2,y) accepts)
E arop y- Pa(a) (Ar.a,) 18
21 an)
E Rou4
Pr <>Tp(a>
[ccov (2, x)]
Now, for every input x; let IT (x) C E" denote the of accepting transcripts:
IT = {+" EE Acov T²) = =1}.
We can assume that (x)) has finite cardinality, since V's running time is bounded and hence the number of different transcripts that can read (and accept) is finite. For any fixed input æ, we can express its acceptance probability by the finite sum:
Pr (ccy
Σ
Pr -- T~(((=)
(T) (m)
We will use Equations through notation, these show that, for any π
6 from the proof of Lemma
Up to change in index
V
Pr
Pr T~
T
V (0).
(x)
(E) sE(T.a]
Combining Equations 7 and (8, by linearity of expectation we have that
(ver(())
E xmp
Σ
Pr T~T (m)
[T=x"|
x*]
(x)
E
Pr T=
(od,
mmp
x'ElI'
(8)
(E(La)
E
E a~7 (x)
AcC
Σ
V vodi (0)
gop
rERU(() .E(T..)
(2
Σ
Vod,(0)
T~T (a)
rERU(O)
eE(La]
E anu you (cr) (.
Accy y, Q1 ......, an) Σ voda(0)
(E sE(La]
)
where in the last equality, the probability is over (gr, a,) sampled in Algorithm 2 and it follows from the definition of the transcript generator (x)).
27

---

D.4 Proof of Theorem 4.1
We first restate Theorem in full formality.
Theorem D.2. Fix verifter V, an input distribution μs, an autoregressive model family {Po)oERs, and a norm || on IR.. Fix an honest transcript generator TV. and assume that the agreement function A(0) == Pr π²) is concave in 9, where the verifier queries are the same in a and n, and the probability is over μb no ~ (T()), and x² ~ (T))). For any >> 0, let BN BLip and be upper-bounds such that the following conditions hold:
There exists E Rd with ||0*1| < Byorm such that A(0*) 21 111-/22 8/2
For all 0, the logits of Pg are -ips-iips That is, suPBeR
I1 log po(())l & BLip-
ZEY.
In the proof system defined by V, the total number of tokens (over all rounds) is at most C.
Denote by 9 the output of TL running for N 2 (2.C2.B% Btsp) /E² iterations and learning
rate = BNtormC B1ap VN. Then the expected Verifiability (over the randomness of the samples collected by TL) of is at least 1 - E. That is, Ey
1-E.
The proof of Theorem D.2 goes by reduction to Stochastic Gradient Descent (SGD). Lemma 3.2 showed that the learner verifier, and differentiating the logits-to optimize the agreement A(0). Since A(0) lower bounds the Verifiability of Pe. the former can be used surrogate for the latter.
its only available tools sampingg honest transcripts. emulating the
For convenience of the reader, we first provide a description of Stochastic Gradient Ascent (equiv. to SGD) and quote theorem its convergence. We adapt the presentation in (Shalev-Shwartz and Ben-David 2014), noting that they present Stochastic Gradient Descent its more general form for non-differentiable unbounded functions. The familiar reader may skip directly to the proof in Appendix D.4.3
D.4.1 Preliminaries on Stochastic Gradient Ascent
Stochastic Gradient Ascent (SGA) is a fundamental technique in concave optimization. Given concave function f: Rd -> [0, 1]. SGA starts at wi = Ô E Rd and tries to maximize f'w) by taking a series of "steps." Than directly differentiating f. SGA instead relies on an estimation V (f()): in each iteration, SGA takes step in direction that estimates V f(w).
Definition D.3 (Gradient estimator). Fix fettreenttaaleefutttti f: Rd - R for some d. A gradient estimator for is randomized mapping Dy: Fdd 12d whose expectation is the gradient of f. That is, for all Rd
Vs(w).
Note that this is equality between d-dimensional vectors.
Algorithm 3: Stochastic Gradient Ascent
Hyperparameters: Learning rate À > 0 and number of iterations E N. Input: A function f: Rd R to maximize and a gradient estimator Dy for Output: A vector 0 IRd
Initialize wy := 0 E Rdd
2 for i N ,....,N
do
Sample 0; (W;-).)
Update W; = W;-1 X- 2c.
Output w == N DiE[M] Wt.
Theorem 14.8 Shalev-Shwarte and Ben-David (0044) implies the following fact.
Fact D.4. Fix a concave f: Rd + [0, 1), norm on Rdd, and upper-bounds B BLip > 0. Let
== E argmax f(w),
wi|l Brorm
28

---

and let to denote the output of Algorithm
run for N iterationn with learning rate
BNorm
Brap N
every iteration it holds that
[us|| Blip then
BNomm BLip
E [f(()) f(w")
VN
D.4.2 Learning with Stochastic Gradient Ascent/Descent
Fact D.4 captures the general case of using SGA for maximization of concave problems. It more common for the literature to discuss the equivalent setting Stochastic Gradient Descent (SGD) for minimization of convex problems. Specifically, common application of SGD is for the task of Risk Minimization: given a loss function and access to an unknown distribution of inputs, the goal to minimize the expected loss with respect to the distribution. Assuming that the loss function differentiable, the gradient of the loss serves as a gradient estimator (see Definition D.3) for the risk function. We refer the reader to Shalev-Shward and Ben- David [2014] Section 14.5.1] for complete overview of SGD for risk minimization.
For the sake of completeness, we formulate Transcript Learning (TL, Algorithm 1 in the frame- work of Risk Minimization
Supervised Learning. This is not strictly needed for the proof of Theorem D.2 but is an illuminating connection. Although multiple loss functions may achieve ultimate goal learning Self-Proving models in what follows we define the loss that corresponds to TL.
Fix verifier V and let Ty denote distribution over accepting transcripts. We define
loss (0, (x,
Pr [Tt * m"), T~ (a)
where n² and share the same verifier messages (as in Lemma 3.2 so the inequality is only the prover's messages, namely (r (T m"] Prx (a) (V; 01 ..,,..,,.00................ aR) *
R
The risk function is the expected value of the loss over the joint distribution of inputs and accepting transcripts μ x (p)::
Risk (0)
E
losss (0, (z, m)]]
which means that the agreement function defined in Theorem D.2
A(0) Pr zm x (x) Tx)
[ot
m"),
satisfies A(0) Risk(f).
Thus, maximizing the agreement is equivalent to minimizing the risk. The hypothesis class over which the optimization is performed is the ball of radius BNorm i.c., {0 H |0||| < BNorm }- The assumption that is concave in implies that the loss function is convex 8, which is the required assumption for using SGD for risk minimization.
D.4.3 Proof of Theorem D.2
Our strategy is to cast TL as Stochastic Gradient Ascent and apply Fact D.4 Let E. BNorm BLip and C' as in the theorem statement be given, Let 6* be such that A(8*) 2 8/2 and |001| S BNorm-
First, notice that
E verv (0) E[A(0)).
'This loss is not to be confused with those discussed in Appendix Here, we are simply explaining how TL can be viewed as supervised risk minimizer for the loss function defined in Equation (9).

---

+ The annotation of the proof consists the first T steps (T....., TT) up to some fixed cutoff T. These are prepended the proof and shown to the model This holds because. for any 2 and model Pg. whenever the transcript generated by (x) agrees with x². then the verifier accepts (because π is honest). Therefore, to prove the theorem it suffices to show that
E[A(O) 2
Following the notation in Algorithm !
in every iteration E
[M]
the norm of the update step is
II a.(0))-
E
(.)
II
a,(O;)
Σ
d.(O:)
rElRuu() xES(r)
rE xES(r)
re(Rjuso) xES(r)
rE(R]u[o) sES(r)
1
Σ
rE(R) *ES(r)
where the inequality is because a, (0t) are probabilities, S 1. Moreover, have
Σ
[ S
E
BLiP S C BLip
rE[R]UÇO) (ES(r)
.E8(r)
The first inequality is by definition of BLiP 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: indexes rounds, and indexes tokens sent in each round.
upper- bound the gradient of Pp's logits. The
To conclude, Lemma 3.2 shows that TL samples from gradient estimator for A(0), while the above equation shows that the gradient is upper-bounded by C BLip- We can therefore apply Fact D.4 to
obtain
[A)) 2 A(0") - s/2 2 (1 - 2/2) E/2 1-
where the inequality is by definition of 0*, This completes the proof of Theorem D.2
E
Learning from annotations
To minimize the length of messages exchanged in 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 "annotated" answer which is then trimmed down to the actual answer a to be sent to the verifier. We adapt Sections and 3 to this setting via Annotated Transcripts. The TL and RLVF algorithms natu- rally extend to annotated transcripts as well. Table 2 shows that annotations significantly improve performance of TL in practice.
[Wei et al., 2022 As concrete example, consider our experiments on computing the GCD. As detailed in Appendix F.2 proof и in this setting is the output of iterative process- the extended Fuclidean algorithm starting from the input
Annotations can be viewed as adding Chain-of-Thoune
Ti r T2
during TL training. At inference time, the model is evaluated only whether it generated the proof π correctly.
We formally capture annotations by introducing a transcript annotator and an answer extractor incorporated into the training and inference stages, respectively. Fix verifier V in an R-round proof system with question length L, and answer length L,, An annotation system with annotation length Ly consists of a transcript annotator A, and an answer extractor E.
In terms of efficiency, think of the annotator as an algorithm the same computational resources as honest prover in the system (see Definition 2.2). and the answer extractor 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:
30

---

Table Self-Proving transformers computing the GCD. We train 6.3M parameter GPT to com- pute the GCD of two integers sampled log uniformly from [10*]. 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; adding Reinforce- ment Learning from Verifier Feedback (+RLVV) increases this 78.3%; training with Annotated Transcript Learning (GPT+ATL) gives the highest Verifiability score of 96%.
LEARNING METHOD
CORRECTNESS
VERIFIABILITY
GPT (BASELINE)
99.8%
GPT+TL GPT+TL+RLVF GPT+ATL
98.8%
60.3%
98.9%
78.3%
98.6%
96.0%
At training time, an input æ and transcript ı is annotated to obtain मे A(2, e.g. before the forwards backwards pass in TL (line 3 in Algorithm
At inference time (i.e., during interaction between V and Po), the prover keeps track of the annotated transcript, but in each round passes the model-generated (annotated) answer through the extractor before is sent the verifier. That is, in each round [R]) the prover samples
a ~ Pa( y, Q1: (i,-..;0y---...... (r)
The prover then extracts answer Or = E(ā,) which is sent to the verifier.
F
Experiments
We describe experimental setup, and present ablation studies that shed additional light on the effect of annotation and representation on Verifiability.
F1
Setup: Training transformers to predict the GCD
Charton
2024 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 uogfounform distribution, and choosing base of representation with many prime factors.
We fix a base of representation = 210 and use x to denote an integer x encoded as a B-ary string For sequences of integers, write (x1x²) to denote the concatenation of x1 with x2, delimited by a special token. The vocabulary size needed for this representation is |>]] Rs 210.
We choose the input distribution to be the log-uniform distribution on [10*], and train the trans- former on sequences of the form (x1x2y), where I1, 42 ~ 14 and y = GCD(z1, This is a scaling-down of Charton [2024], to allow single GPU training of Self-Proving transformers. In all of our experiments, we use a GPT model (Vaswani al. 2017 with 6.3M parameters trained on dataset of 1024K samples in batches of 1024. Full details are deferred to Appendix G.2
Proving correctness of GCD. Following Charton 2024 as a baseline, we find that transformers can correctly compute the GCD with over 99% probability over (#1, μ. To what extent can they prove their answer? To answer this question, we first devise natural proof system based on Bézout's 's theorem. Its specification and formal guarantees are deferred to Appendix [G.] 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 from the prover.
Completeness: For any Tı, T2, y E [10*] such that y GCD(z x2), there exists a proof т such that (x1x2yy) accepts. As detailed in Appendix G. the proof π consists of pair of integers who are Bézout coefficients for 2ı, æ2.
B 210 is chosen following Charton 2024 to be integer with many prime factors.
31

---

Soundness: y + GCD((1,.2). then ((x1X2yT) rejects for any alleged proof π E E"
To measure Verifiability, we train a Self-Proving transformer using Transcript Learning on sequences (X1X2уz) and estimate for how many inputs 41,42 μ does the model generate both the correct GCD y and a valid proof x. We test on 1000 pairs of integers zi,4z3 ~ ii held-out of the training set, prompting the model with (x/x2) to obtain (y'x') and testing whether ((x x2y'm') accepts.
Table 2 shows our main experimental result, which has the following key takeaways:
1. Transcript Learning (TL.) for 100K iterations (=100M samples) results in Self-Proving transformer that correctly proves 60.3% its answers.
2. A base Self-Proving Model with fairly low Verifiability of 40% can be improved to 79.3% via Reinforcement Learning from Verifier Feedback (RLVF). Although it does not rely on honest transcripts, RLVF trains slowly: this nearly-twofold improvement took four million iterations.
3. Most efficient is Annotated Transcript Learning, which yielded a model with 96% Verifia- bility in 100K iterations. We further investigate their effect next.
F.2 Models generalize beyond annotations
(Zoomed-in)
Euclidean depth 8
Euclidean depth
Euclidean depth
T=3
T=5
T=6
T=7
82.0%
84.0%
86.0%
88.0%
90.0%
92.0%
94.0%
96.0%
Euclidean deptn 0
Euclidean degen
Euclidiçnn depth 4
Dichidean depth
20%
30%
40%
50%
60%
70%
80%
90%
100%
Verifiability
Figure 3: 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 + standard error depicted. The upper graph provides zoomed-in view of the 82% to 98% range from the lower graph, which spans broader scale from 20% to 100%.
The proof π is annotated by including intermediate steps in its computation. Details are deferred to Appendix G.I roughly speaking, we observe that the proof for input (a, b) is obtained as the last element in sequence a, b, TT, . computed by the Euclidean algorithm. We annotate the proof by prepending to the sequence of Euclidean steps (II...., ... RT) up some fixed cutoff T.
Figure shows how affects the Verifiability of the learned model. As suggested by Lee et al. training the model more intermediate steps results in better performance; in case, increasing the number of intermediate steps 7 yields better Self-Proving models. One might suspect
2024
With probability ie.. in Definition 2.2
32

---

Verifiability
0.8
0.6
0.4
0.2
Iteration
20k
80K
1001
Figure 4: Annotated TL Verifiability as function of the number samples N. Each iteration (X axis) is batch of 1024 samples from dataset of x= =0M sequences. Every 10k iterations, Verifiability was evaluated on a held-out dataset of 1 inputs. T is the number steps in Annotated Transcript Learning (Figure B), and T is non-annotated Transcript Learning. Each T was with three seeds, with mean depicted by the curve and standard error by the shaded area.
that models only learn to execute the Euclidean algorithm in-context. To rule out this hypothesis, we derive upper bound on the possible efficacy of such limited models. This bound is based on the Euclidean depth of integers (x1, 22), which we define as the number of intermediate steps that the Euclidean algorithm makes before terminating to compute (in-context) the arithmetic of the Euclidean algorithm would only be able to prove the correctness of inputs (2), whose depth does not exceed the annotation cutoff T'.
input (æ1, (2), Indeed, model that only learns
Figure tells a different story: For each cutoff T, we estimate the probability that integers .7, 422 have Euclidean depth at most T on 10" sampled pairs. Larger annotation cutoff T increases Verifiability, but all models exceed their corresponding Euclidean depth bound.
F.3 Base representation
concludes that, for a given base of representation B, transformers correctly compute the GCD of integers I1, H2 that are products of primes dividing B. Simply put, choosing base B with many different prime factors yields models with better correctness (accuracy), which suggests why base 210 2- 5 yielded the best results. To test B's factorization has a similar effect Verifiability, we train transformers on 68 bases varying number of prime divisors from wB) = (i.e., is a prime power) w(B) shows that (B)) correlates not just with correctness [Charton 2024 but also with Verifiability.
As mentioned previously, Charton 2024
Figure
33

---

w
((B) =
w(B) =
w(B)
4
43.0%
44.0%
45.0% Verifiability
46.0%
47.0%
48.0%
Figure 5: The number of prime divisors of base w(B) determines Verifiability. For each E [4], we sampled 17 bases B E (2...., 1386} such that w(B) A Self-Proving transformer was trained via Transcript Learning for twenty epochs on identical dataset of 1024K samples encoded in base B. For each w ()) we depict the mean + standard error.
Although the finding statistically significant (no overlapping error margins), the difference is by few percentages; we attribute this to the smaller (10%) number of samples on which models were trained, relative to other experiments.
Verifiability
0.75
0.65
0.6
0.55
Iteration
4M
Figure 6: RLVF Verifiability as a function of number of samples N. Starting from a base model with Verifiability 48% (obtained via Transcript Learning), in each iteration batch of 2048 inputs are sampled; the model generates proof for each; the Verifier is used to check which proofs accepted; then, the model parameters updated accordingly (see Algorithm 2 Verifiability was evaluated on a held-out dataset of 1k inputs.
34

---

Algorithm 4: Extended Euclidean algorithm
Input: Nonzero integers 20, 41 E N.
Output: Integers (y, 20, 21), such that GCD (10. and (zo, 21) are Bézout coefficients for (2o, x1).
Initialize To = 20. 71 = I1, = 1, 81 0, and q = 0.
while ri + do
3
Update y = (ro/ri]
Update (To. 11) = [1,, Po 11).
Update (Sp. $1 = ($1, - $1).
6
Output GCD ro and Bézout coefficients 20 = and 21 == (ro -80 20)) 21.
G Full details of the experimental setup
G.1
The Bézout proof system for GCD
The Euclidean algorithm for computing the Greatest Common Divisor (GCD) of two integers is possibly the oldest algorithm still use today [Knuth 1969.. Its extended variant gives a simple proof system.
Before we dive in, us clarify what we mean by a system for the GCD. Prover Paul has two integers 212 and 159; he claims that GCD(212, 159) = 53. An inefficient way for Verifier Veronica to check Paul's answer is by executing the Fuclidean algorithm on (212, 159) and confirm that the output is 53. In an efficient proof system, Veronica asks Paul for short string x² (describing two integers) with which she can casily compute the answer- without having to repeat Paul's work all over. On the other hand, if Paul were claim that "GCD(212, 159) 51" (it does not), then for any alleged proof h, Veronica would detect an error and reject Paul's claim.
The verifier in the proof system relies on the following fact.
Fact G.1 (Bézout's 's identity [Bezout 1779 ). Let Zg. 21 E N and 2o, 21 E Z. If 20 2o + 21 divides both 2o and 2 then 20 20 21 21 = GCD
Any coefficients 20, 21 satisfying the assumption of Fact G.1 are known as Bézout coefficients for (Io, ). Fact G. immediately gives our simple proof system: For input x = (f0, and alleged GCD y. the honest prover sends (alleged) Bézout coefficients. (#o, #1). The Verifier accepts if and only yf 20 + I1 and y divides both and æ1.
In this proof system the Verifier does not need to make any query; to fit within Definition 2.2 can have the verifier issue a dummy query. Furthermore, by Fact G.1 it is complete and has soundness error 0. Lastly, we note that the Verifier only needs perform two multiplications, and two modulus operations; that sense, verification is more efficient than computing the GCD in the Euclidean algorithm required by Remark 2.3
addition,
Annotations. To describe how proof (20, 21) is annotated, let first note how it can be computed. The Bézout coefficients can be found by an extension of the Euclidean algorithm. is described in Algorithm 4
Referring to Algorithm the annotation of a proof z (=o, 21) will consist of intermediate steps in its computation. Suppose that in each iteration of the While-loop, the algorithm stores each of ro- 8o and in an arrays rō. 66 and q. The annotation of is obtained by concatenating each of these arrays. In practice, to avoid the transformer block (context) size from growing too large, we fix cutoff T and first trim each array to its first elements.
We formalize this in the terminology of Appendix E by defining a Transcript Annotator and Answer Extractor. Note that, since our proof system consists only of one "answer" send from the prover to the verifier, the entire transcript is simply z = (Zo. 21). Since the verification is deterministic, this means that the proof system is of an NP type (however, note that the search problem of finding the "NP-witee witness" = (zo, #1) is in fact in P).
Our description follows https: /thps://Aee httper///e..vkiiiiiiiieee wikipedia http:///rwwwaaaetteeeeeettaieee algorithh
35

---

Transcript Annotator A: For a fixed cutoff T' and given input = (Io, X1) and transcript 2 (zn, 21). ) A executes Algorithm on input x (zg. (1): During the execution. A stores the first T intermediate values of ro. and y in arrays rö. so and qj It outputs
A(r, 2) (To, 50. q, 2).
Answer Extractor E: Given an annotated transcript 2 = (77, so, q, z), outputs E( = 2.
We note that the computational complexity of A is roughly that of the honest prover, i.e. Algorithm 4 (up additional space due to storing intermediate values). As for E, it can be implemented in
logarithmic space and linear running time in [ i.e. the length of the description 12
G.2 Implementation details
Code, data and models are available
Model architecture. We use Karpathy's nanoGP7 implementation of GPT. Note that we train the model "from scratch" only sequences related to the GCD problem, rather than starting from a pretrained checkpoint. We use 6.3M parameter architecture 256 embedding dimensions. We optimized hyperparameters via random hyperparameter search, arriving at learning rate 0.0007, AdamW 31 = 0.733 and 82 = 0.95, 10% learning rate decay factor, no dropout, gradient clipping at 2.0, no warmup iterations, and 10% weight decay.
layers, attention heads, and
Data. We sample integers from the logio-uniform distribution over (1...., 10*). Models in Ta- ble lnd Fig. 33 are trained for 100K iterations on a dataset of ss10M samples. For Figure (base ablation) we train for 20K iterations a dataset of IM samples; this is because this setting re- quired 68 many runs in total, whereas the annotation-cutoff ablation required 18 longer runs.
Compute. All experiments were run on machine with an NVIDIA A1OG GPU, 64GB of RAM, and 32 CPU cores. The longest experiment was the single RLVF run, which took one month and four days. The innoationn-cutff ablation runs took about 75 minutes each. Base of representation ablation runs were shorter at about 15 minutes each. The total running time of the Transcript Learn- ing experiments was approximately 40 hours (excluding time dedicated random hyperparameter search), and the RLVF experiment took another month and four days. The overall disk space needed for our models and data is 4GB.
Representing integers. We fully describe how integer sequences are encoded. As running ex- ample, 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 appended, with unique delimiter identifying each component of the sequence. For example, consider the input integers Jn 159. Their GCD is y 53, with Bézout coefficients 2g 1 and 21 = 1. Therefore, the sequence (212, 159, 53, 1, -1) is encoded as
212 (which is 12 in base 210) and
+, 9,1,2,x0,
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 mi delimited by unique token. Since different integer pairs may require different number of inter- mediate steps to compute the Bézout coefficients, we chose to pad all annotations to the same length T by the last step Tr 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 to batch model testing (generation and evaluation) resulting in a 1000x speed-up over sequential testing.
12 That is, if integers are represented by n-bits, then has space complexity O(log n + log and running time O(n -T).
36

---

As an example, consider the inputs = 46 and 21 Algorithm 4 we have
39.
Tracing through the execution of
21
46
46
0
39
5
-5
4
-11 13
To encode this as an annotated transcript for the transformer, we must specify a base of represen- tation and an annotation cutoff. Suppose that we wish to encode this instance base 10 and cutoff T = 3. Then the input with the annotated transcript is encoded as
+ ,,,,
,,,,q', +, ",0,,,0*,,,,,,,,,,, ,,,,4''', +,1,20" ,,,,211", ,,,,"""" ,,,,,"" 2,,,,,,,,,,1,,,,2,
+
where commas used to separate between tokens, and linebreaks added only for clarity. No- tice the three types of tokens: signs, digits, and delimiters. Notice also that the output 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 output and only then proves it.
37


Reviews:
[{"review_id": "NK7BMt5Ci0", "reviewer": "Reviewer_FMTQ", "summary": "This paper introduces the concept of self-proving models, a class of sequence-to-sequence models designed to interact with a specified verifier via an interactive proof protocol. Two learning algorithms are proposed for training such models:\n- Transcript Learning Algorithm: This method trains the model using a ground-truth dataset of interactive proofs generated by an honest prover interacting with the verifier.\n- RLVF Algorithm: This approach employs reinforcement learning, where the training data is generated by the model itself and validated by the verifier.\n\nUnder certain assumptions, the authors prove the convergence of both algorithms.", "questions": "N/A", "limitations": "- The high level of abstraction in the problem formulation restricts both the theoretical implications and the potential for real-world applications.", "rating": 2, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 3, "significance": 1, "originality": 1, "strengths_and_weaknesses": "Strengths:\n+ The paper addressed an interesting challenge of the worst-case guarantee of probabilistic models.\n\nWeaknesses:\n- The setting proposed is overly abstract. The self-proving model is defined in terms of an unspecified probabilistic model and an abstract verifier, without any structural constraints. Given that the general interactive proof setting includes problems as hard as IP or PSPACE-complete, the current abstraction leaves little room for meaningful theoretical insight or practical application.\n- The proposed learning algorithms are relatively straightforward, and the lack of empirical evaluation significantly reduces their practical interest.\n- The convergence guarantee in Theorem 4.1 relies on strong and arguably unrealistic assumptions, including parameter convexity and Lipschitzness, which limits the practical relevance of the result.\n- The technical novelty is limited. Key aspects of the convergence proof rely heavily on prior results by Shalev-Shwartz and Ben-David [2014], with little original contribution.", "was_revised": true, "final_justification": "The authors present an empirical study on generating proofs for GCD. While the work is interesting, I see a fundamental limitation in the proposed architecture: the model is trained to produce the final answer before generating the proof. Although this ordering resembles the definition of an interactive proof system, it effectively removes the chain-of-thought reasoning process from answer generation. As a result, the model’s reasoning capacity is constrained to AC0 [a], i.e., problems solvable by constant-depth circuits.\n\nGiven that reversing the generation order can significantly enhance the model’s problem-solving ability, I believe the formulation in the paper should be substantially revised to address this architectural limitation. I will therefore keep my score unchanged.\n\n[a] Li, Zhiyuan, et al. \"Chain of thought empowers transformers to solve inherently serial problems.\" arXiv preprint arXiv:2402.12875 (2024).", "rebuttal": "Thank you for your review and for acknowledging that our paper addresses an interesting challenge regarding worst-case guarantees of probabilistic models. We appreciate your detailed feedback and address each of your concerns below.\n\n**Regarding abstraction and PSPACE-completeness:**\nAs the reviewer notes, IPs can be used to prove PSPACE-complete problems. However, this *does not* preclude designing very efficient IPs for tractable computational problems or classes of computations. Moreover, even if a problem is intractable *in the worst case*, this does not preclude constructing efficient honest provers that perform well on real-world inputs  (i.e. convince the verifier on average-case inputs). In terms of theoretical insights, the literature on IPs has produced a treasure trove of such insights (e.g. the literature on ZK proofs and doubly-efficient proof systems), even though the same objection (that IPs include PSPACE complete problems) could be raised there. This is the case even though the focus there is on *worst-case* guarantees (for the honest prover), let alone in the ML setting where we focus on *average-case* guarantees (for the honest prover).\n\n**Regarding empirical evaluation:**\nWe have conducted comprehensive experiments demonstrating practical instantiation. We trained 6.3M parameter transformers to compute *and prove* GCD correctness using Bézout certificates. Results: Transcript Learning achieved 60.3% verifiability, RLVF improved models from 40% to 79.3%, and Annotated TL reached 96% verifiability. Crucially, models generalize beyond their training—proving GCDs that require more steps than seen during training. These experiments validate that our algorithms produce non-trivial learning behavior in practice. We provide additional experimental details following the rebuttal.\n\n> Theorem 4.1 relies on strong and arguably unrealistic assumptions.\n\nWhile autoregressive neural networks have non-convex loss landscapes, analyzing convex settings remains valuable in ML theory. Convex analysis provides clean mathematical tools for building intuition and establishing foundational results—a standard approach in theoretical ML. Proving convergence without convexity is the subject of cutting-edge research. Following common practice, we prove results under simplifying assumptions and complement them with experiments showing convergence even when these assumptions don't hold. We note that the same algorithm for transcript learning  is used in the experiments as in the theorem. Our experiments confirm practical convergence of transcript learning on non-convex transformer architectures.\n\n> The technical novelty is limited. Key aspects of the convergence proof rely heavily on prior results by Shalev-Shwartz and Ben-David [2014], with little original contribution.\n\nThe technical novelty of this paper is in contributing a formal model for verifying correctness on every instance  connecting a rich body of literature on interactive proofs to the area of generative models (as well as in the proofs of the convergence theorems on the use of transcript learning). Many impactful theoretical works have been first introduced in “definitional” papers; with a robust definition at hand, follow up works can yield general theorems. A case in point is the original work on “Zero Knowledge Interactive Proofs” where the first paper introduced the model and one example of zero-knowledge proof for one specific problem (distinguishing quadratic residues from non-residues) and shortly after  in follow up work it was shown how to get zero-knowledge proofs for all of NP. Furthermore, using theoretical notions such as debate systems has improved the accuracy of generative models significantly; similarly, our self proving models could potentially lead to improved accuracy guarantees as well.  \n\n---\n**Experiment details**\nWe have conducted experiments demonstrating that our framework can be practically instantiated. We trained 6.3M parameter transformers to compute and prove the correctness of GCD computations on pairs of integers up to 10^4, following Charton's [1] setup.\n\nKey results:\n- Transcript Learning (TL): Achieved 60.3% verifiability (correctly proving answers) after training for 100k steps.\n- RLVF: Improved a base model with 40% verifiability to 79.3%, albeit in significantly more (4M) iterations; while this is not an experimental paper, we will continue to explore a practical speedup by searching the hyperparameter space.\n- TL + Annotations: Reached 96% verifiability by training on proofs annotated with intermediate Euclidean algorithm steps (similar to chain-of-thought); importantly, evaluation uses only the final proof.\n\nOur proof system uses Bézout's theorem: the model must output coefficients a,b such that $a x_1 + b x_2 = GCD(x_1, x_2)$, which the verifier can use to easily check (with certainty) that the model's output is indeed the GCD.\n\nMore nuanced results show (1) more annotation steps improve verifiability monotonically, (2) even when trained with annotations, the model generalizes beyond the amount of annotations (i.e., it is not just memorizing the chain-of-thought, but exhibits length generalization), and (3) bases with more prime factors improve both correctness and verifiability—in line with Charton's findings.\n\nWhile GCD is simpler than general theorem proving, it provides a concrete proof-of-concept that self-proving models can be trained in practice. We are happy to provide full experimental details and will include them in the camera-ready version.\n\n[1] Francois Charton. Learning the greatest common divisor: explaining transformer predictions. ICLR 2024."}, {"review_id": "9SiaER4gtY", "reviewer": "Reviewer_KBcF", "summary": "This work focuses on the correctness of LLMs according to certain inputs. To do so, it proposes an approach via interactive proofs named self-proving models. In this model, LLMs can generate the answer with proofs, and users are able to verify and be convinced that answer and proofs. It also proposes transcript learning and reinforcement learning from verifier feedback to learn SPMs.", "questions": "1. Have you considered to extend this work to support ZKPs? ZKPs provide properties in IPs as well as zero-knowledge property to make the system secure if the prover with LLMs is untrusted.\n2. What is the convergence guarantee for RLVF? I know you mentioned this in Remark 4.2. Can you provide more explanation (You may provide this in appendix if space is tight)?", "limitations": "N/A", "rating": 5, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 4, "clarity": 4, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Strength:\n\n1. This work carefully defines notions of correctness and soundness in LLMs with interactive proofs as well as the verifiability.\n2. Other than worst-case scenario, this work also discusses the average-case scenario.\n3. This work provides algorithms to learn SPMs with convergence of transcript learning.\n\nWeakness:\n\n1. This work lacks of empirical results, even though this work focuses mainly on theory. However, experimental results are more convincing even with a simple ones.\n2. This work hides too many details in the appendix like related works and proofs of lemmas.", "was_revised": true, "final_justification": "Since the authors will add empirical results for the work, I will keep my score.", "rebuttal": "We sincerely thank you for your positive and constructive review. We appreciate your recognition of our careful definitions of correctness and soundness, our treatment of both worst-case and average-case scenarios, and our convergence analysis for transcript learning. Your feedback has helped us significantly improve the paper.\n\n### Regarding concerns\n**Empirical results:** We will add experiments demonstrating the practical viability of our framework. We trained 6.3M parameter transformers to compute and prove the correctness of GCD computations. Key results include: Transcript Learning achieving 60.3% verifiability, RLVF improving a model from 40% to 79.3% verifiability, and Annotated TL reaching 96% verifiability. Our ablation studies reveal that models generalize beyond their training annotations and that representation choices significantly impact performance. Appended to this rebuttal are additional details. We will include analysis (with figures) in the camera-ready version and release the model and code publicly.\n\n**Paper organization:**\nWe will move the related works into the body of the paper. We follow the conventions of theory papers wherein theorems are formally stated in the body; proof overviews are given in the body, and the full details are deferred to the appendix.\n\n### Regarding questions\n**ZKP extension:**\nThat is an extremely interesting direction for future research. We note that already the current setup (IPs) has a secure system even when the LLM-prover is untrusted (this is the soundness property). ZK would guarantee that, an LLM-prover would not leak anything (e.g. sensitive training data) to the verifier. Thank you for encouraging this direction.\n\n**RLVF convergence:**\nUnlike supervised learning, there is no \"standard\" set of assumptions for RL convergence theorems. Rather than arbitrarily choosing specific assumptions, we prove a Gradient Approximation Lemma from which convergence guarantees can be derived in particular settings. This mirrors the approach for, e.g., Policy Gradient methods, where the Policy Gradient Theorem (which is a gradient estimation lemma) provides the foundation from which specific algorithms derive their guarantees. See, for example, Chapter 3 of Reinforcement Learning: Theory and Algorithms by Agarwal, Jiang, Kakade and Sun (2022).\n\n---\n**Experiment details:**\nWe have conducted experiments demonstrating that our framework can be practically instantiated. We trained 6.3M parameter transformers to compute and prove the correctness of GCD computations on pairs of integers up to 10^4, following Charton's [1] setup.\n\nKey results:\n- Transcript Learning (TL): Achieved 60.3% verifiability (correctly proving answers) after training for 100k steps.\n- RLVF: Improved a base model with 40% verifiability to 79.3%, albeit in significantly more (4M) iterations; while this is not an experimental paper, we will continue to explore a practical speedup by searching the hyperparameter space.\n- TL + Annotations: Reached 96% verifiability by training on proofs annotated with intermediate Euclidean algorithm steps (similar to chain-of-thought); importantly, evaluation uses only the final proof.\n\nOur proof system uses Bézout's theorem: the model must output coefficients a,b such that $a x_1 + b x_2 = GCD(x_1, x_2)$, which the verifier can use to easily check (with certainty) that the model's output is indeed the GCD.\n\nMore nuanced results show (1) more annotation steps improve verifiability monotonically, (2) even when trained with annotations, the model generalizes beyond the amount of annotations (i.e., it is not just memorizing the chain-of-thought, but exhibits length generalization), and (3) bases with more prime factors improve both correctness and verifiability—in line with Charton's findings.\n\nWhile GCD is simpler than general theorem proving, it provides a concrete proof-of-concept that self-proving models can be trained in practice. We are happy to provide full experimental details and will include them in the camera-ready version.\n\n[1] Francois Charton. Learning the greatest common divisor: explaining transformer predictions. ICLR 2024."}, {"review_id": "YAdwQphhoz", "reviewer": "Reviewer_AHTf", "summary": "The paper proposes the idea of Self-Proving models - which prove interactively the correctness of their output with a verifier. This gives guarantees for a given input c.f. the typical average over a distribution of accuracy guarantees. Two methods are proposed for learning such models - one via access to transcripts of verifications and the other via RL through emulation of interaction with a verifier.", "questions": "1. Perhaps a naive question, but how does this work sit with Godel, e.g. the existence of true statements which are not probable would seem to present an issue for the claims of completeness in practise.\n\n2. In definition 2.2, is the word \"honest\" redundant? ie there exists a P* s.t. ....is surely sufficient", "limitations": "Yes", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 2, "originality": 3, "strengths_and_weaknesses": "The paper introduces a new concept of Self-Proving models, proposed two methods for learning such models, and considers convergence bounds. \n\nOne concern might be the level of significance/applicability of the work. Whilst theoretically solid, the practical implications of this work I feel would be limited. For example, considering the related area of models that prove general formal theorems. This is notoriously hard, and it seems unlikely that one could train a model with practical confidence parameters in any non-trivially applicable scenario. (The paper seems to push this question out of scope: \"the rich and well studied question of which settings are verifiable within an interactive proof system is beyond our scope)\n\nIn summary, I think this is an interesting framework that has been created, but I am left wondering if it can be instantiated in any meaningful way.\n\nStrengths:\n- well-written with sound and well-presented theorems/lemmas\n- thorough and illumination discussion of the motivation and concepts\n- the ideas re backward data generation and the idea of bootstrapping RLVF with TL are good\n\nWeaknesses:\n- concerns re practicality/applicability of framework (per above)", "was_revised": true, "final_justification": "Though the proposed additional experiment is appreciated, I think my underlying feeling still stands that the scope of relevance of this framework is typically quite limited. I will keep my score.", "rebuttal": "Thank you for your thoughtful review and for recognizing our framework as interesting and theoretically sound. We appreciate your acknowledgment of our well-presented theorems, thorough motivation, and novel ideas. Your questions about practical applicability and foundational limits are insightful and help clarify important aspects of our work.\n\n### Regarding concerns\n\n> Whilst theoretically solid, the practical implications of this work I feel would be limited. For example, considering the related area of models that prove general formal theorems. This is notoriously hard, and it seems unlikely that one could train a model with practical confidence parameters in any non-trivially applicable scenario.”\n\nWe share your view that general theorem proving is notoriously difficult. However, our framework applies to a much broader class of problems than just \"trivial\" mathematics. Many computational tasks admit efficient interactive proofs while remaining tractable—from arithmetic operations to graph properties to optimization problems.\nTo demonstrate practical instantiation, we have conducted experiments on GCD computation with Bézout coefficient proofs. Our 6.3M parameter transformers achieved 60.3% verifiability with basic Transcript Learning, 79.3% with RLVF, and 96% with annotated training. While GCD is admittedly simpler than general theorem proving, it demonstrates that self-proving models can be trained effectively for non-trivial mathematical tasks. This provides a foundation for exploring more complex applications in future work. We will include analysis (with figures) in the camera-ready version and release the model and code publicly. We note that the code is generic, so that larger transformers can be trained for more involved proof systems by those who have the computational resources.\n\n### Regarding questions\n**Gödel's incompleteness:**\nNot at all naive, this question is an important one to ask in the context of any Proof system! Informally speaking, you are right to say that there is no single Interactive Proof system that is complete with respect to “all True statements.” Instead, one should think about specific problems (i.e., specific notions of True statements) for which there is an IP system. Then, our theory studies whether it is possible to learn an approximately-honest Prover. Indeed, there are problems for which an IP system _cannot exist_; but on the other hand, there is an extremely rich family of problems (anything solvable in polynomial space) for which an IP system _does exist_ (as shown by Shamir 1992).\n\n**\"Honest\" terminology:**\nThank you for pointing out this potential confusion. We've clarified the definition to make it clearer that we're defining what \"honest\" means. We now write: \"If there exists a prover P* such that [conditions]... Such a prover is called an honest prover.\" This should make it evident that \"honest\" is the term being defined, not a redundant qualifier.\n\n---\n**Experiment details:**\nWe have conducted experiments demonstrating that our framework can be practically instantiated. We trained 6.3M parameter transformers to compute and prove the correctness of GCD computations on pairs of integers up to 10^4, following Charton's [1] setup.\n\nKey results:\n- Transcript Learning (TL): Achieved 60.3% verifiability (correctly proving answers) after training for 100k steps.\n- RLVF: Improved a base model with 40% verifiability to 79.3%, albeit in significantly more (4M) iterations; while this is not an experimental paper, we will continue to explore a practical speedup by searching the hyperparameter space.\n- TL + Annotations: Reached 96% verifiability by training on proofs annotated with intermediate Euclidean algorithm steps (similar to chain-of-thought); importantly, evaluation uses only the final proof.\n\nOur proof system uses Bézout's theorem: the model must output coefficients a,b such that $a x_1 + b x_2 = GCD(x_1, x_2)$, which the verifier can use to easily check (with certainty) that the model's output is indeed the GCD.\n\nMore nuanced results show (1) more annotation steps improve verifiability monotonically, (2) even when trained with annotations, the model generalizes beyond the amount of annotations (i.e., it is not just memorizing the chain-of-thought, but exhibits length generalization), and (3) bases with more prime factors improve both correctness and verifiability—in line with Charton's findings.\n\nWhile GCD is simpler than general theorem proving, it provides a concrete proof-of-concept that self-proving models can be trained in practice. We are happy to provide full experimental details and will include them in the camera-ready version.\n\n[1] Francois Charton. Learning the greatest common divisor: explaining transformer predictions. ICLR 2024."}, {"review_id": "Sui6EK3INU", "reviewer": "Reviewer_p6mv", "summary": "This paper investigates the usage of interactive proofs for learned models. They provide a generalized theory, and show that incorporating rounds of verification helps to produce guarantees on soundness (i.e. rejecting wrong answers with high probability). This lays the conceptual groundwork for applying learned models to decision problems solvable in PSPACE. The authors propose two training algorithms and prove convergence results under certain assumptions.", "questions": "Could you provide more guidance or examples on how a verifier might be instantiated in practice, even in a simplified setting? This would help clarify the practical applicability of the framework.\n\nHave you considered demonstrating this approach on a constrained problem space where verifier construction is tractable, such as arithmetic or logic puzzles?", "limitations": "While a few illustrative examples are mentioned (e.g., lines 134 and 238–244), the paper lacks any empirical results or concrete instantiation of the proposed framework, making it hard to assess its practical feasibility.\n\nAs noted above, the strongest limitation is the absence of a method for producing a suitable verifier — which is essential to the framework’s claims. Even a toy example or partial empirical demonstration would significantly strengthen the paper.\n\nThese limitations are not sufficienlty acknowledged in the paper.", "rating": 4, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 2, "originality": 3, "strengths_and_weaknesses": "Strengths:\nThe background and introduction are strong and clear, providing a clear example of the benefits of self-proving models. The intuition and informal explanations provided about the verifier were helpful in lines 67-68 and in lines 134-142.\n\nWeaknesses:\nRemark 2.5 cites the union bound in line 128, but it is more accurate to just say that the events of a true positive (correct output) and false positive (soundness error) are disjoint.\nMany of the core claims rely on the existence of a verifier with strong properties (e.g., sufficiently low soundness error), but the paper does not explain how such a verifier would be constructed or learned. This weakens the practical relevance of the theoretical results.", "was_revised": true, "final_justification": "The paper remains somewhat abstract and speculative but might be considered promising.", "rebuttal": ""}]

Author rebuttal:

Meta-review: This paper proposes a framework of designing (LLM) models that can argue about the correctness of their decision to convince a (weak) verifier. The paper proposes a definitional framework a la interactive proofs. It then proposes two methods for training such models: one is based on “transcript learning” and the other based on “reinforcement learning” (designed for interactive proofs).

The paper does not have empirical experiments, which was brought up by the majority of the reviewers and was considered a major weakness. During the rebuttal, the authors report that they can implement and get initial results for the (simple problem of) GCD. Different reviewers valued this (potential) contribution differently; some considered it enough to make the paper acceptable and some still saw it as a toy example. The paper’s methods also build upon previous works and hence its main contributions are definitional.

At the end, the problem tackled by the paper is very timely and relevant to how LLM’s reasoning is playing out in practice. However, the practical side was questioned by the reviewers and hence the paper would definitely get a boost from adding such experimental results. At the end, the paper is borderline, but due to its theoretical merit can be a nice addition to the program if there is room.
Decision: Accept (poster)