On Learning Verifiers and Implications to Chain-of-Thought Reasoning
Authors: Maria Florina Balcan
Avrim Blum
Zhiyuan Li
Dravyansh Sharma
Venue: NeurIPS 2025 poster ()
Keywords: Learning theory
LLM reasoning
Chain-of-Thought
Primary area: theory

Abstract: Chain-of-Thought reasoning has emerged as a powerful approach for solving complex mathematical and logical problems. However, it can often veer off track through incorrect or unsubstantiated inferences. Formal mathematical reasoning, which can be checked with a formal verifier, is one approach to addressing this issue. However, currently LLMs are simply not good enough to solve complex problems in a formal way, and even just formalizing an informal problem statement can be challenging. Motivated by this fact, in this work we consider the problem of learning reliable verifiers for sequential reasoning, including natural language Chain-of-Thought reasoning. That is, given a problem statement and step-by-step solution in natural language, the aim of the verifier is to output [Yes] if the reasoning steps in the solution are all valid, and [No] otherwise. In this work we give a formal PAC-learning framework for studying this problem. We propose and analyze several natural verification goals, at different levels of strength, in this framework. We provide sample complexity upper-bounds for learning verifiers satisfying these goals, as well as lower-bound and impossibility results for learning other natural verification objectives without additional assumptions.

On Learning Verifiers and Implications to Chain-of-Thought Reasoning
Maria-Florina Balcan Carnegie Mellon University ninamf cmu. edu
Avrim Blum TTIC avrimêttic
Zhiyuan Li TTIC
zhiyuanl1@ttic.ddi
Dravyansh Sharma TTIC, Northwestern University dravySttic.
Abstract
Chain-of-Thougee reasoning has emerged as a powerful approach for solving complex mathematical and logical problems. However, it can often off track through incorrect or unsubstantiated inferences. Formal mathematical reasoning, which can be checked with formal verifier, is approach to addressing this issue. However, currently LLMs are simply not good enough to solve complex problems formal way, and even just formalizing informal problem statement can be challenging. Motivated by this fact, in this work we consider the problem learning reliable verifiers for sequential reasoning, including natural language Chain-of of Thought reasoning. That is, given a problem statement and step-by by- step solution in natural language, the aim of the verifier is output [Yes]] if the reasoning steps in the solution are all valid, and [No] otherwise. In this work we give a formal PAC-learning framework for studying this problem. We propose and analyze several natural verification goals, at different levels of strength, in this framework. We provide sample complexity upper-bounds for learning verifiers satisfying these goals, as well lower-bound and impossibility results for learning other natural verification objectives without additional assumptions.
Introduction
With increasing of LLMs solve complex mathematical and logical problems through chain-of- thought reasoning, it has become crucial to develop verifiers that can check the correctness of these generated solutions. particular, even with recent advances, Chain-of-Thoueee (CoT) reasoning still widely believed to suffer from catastrophic failures resulting from accumulated errors except for highly limited scenarios [LFL 23 SVK24]. It can be particularly challenging to detect subtle errors in long sequences of reasoning, especially when presented via informal natural expressions. This motivates the need for designing effective verifiers for CoT reasoning in natural language.
To study this problem, in this work we introduce a PAC-Iearning framework for learning verifiers for sequential reasoners. Our learning algorithms are given sample of some problem statements and labeled reasoning sequences for the problems, and are required to check the correctness of unseen reasoning sequences for unseen problems. We consider several related but different verification goals and analyze the sample complexity for learning verifiers satisfying these criteria, giving both upper bounds and impossibility results.
For example, the simplest (weakest) verification goal we consider is that given a random reasoning trace from underlying distribution D, the verifier should output whether the reasoning is correct
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

or faulty (and if faulty, where the first error occurred). and it should have error rate at most some given e >> O. The aim is then, with probability 2 1 6, to learn such a verifier from labeled data of correct and faulty reasoning traces from the same distribution. One drawback of this simple verification goal that it is not secure against adaptive use. For example, if an L.LM reasoner is told by the verifier that a reasoning trace To, I,,,.., ..... Ft is incorrect at the ith step, then a natural reaction is to back up and replace 2; with some other step z and try again, and to keep trying until a new reasoning trace is found that succeeds. But there is now no guarantee the final trace produced is correct, both due to the multiple rounds of querying and because the new traces queried may now be out-of-distribution.
To address the above challenge, we also introduce stronger. more trustworthy verification goal. in which given some distribution over problem instances zo, for most To D the verifier should not accept any faulty reasoning trace from Zg. Of course, such a verifier should also accept at least some correct reasoning traces from Ti, and we give upper and lower bounds depending on whether we allow the verifier to just accept designated gold standard reasoning trace g(vo) or whether we require it accept a large fraction of all correct reasoning traces from To without any additional assumptions. These verifiers are more robust any distribution shift in the reasoning traces compared to what was available in the training set.
Overall, our work introduces a principled framework for designing verifiers for CoT reasoning using machine learning. Our learnability results highlight the usefulness of our framework for designing verifiers with desirable properties with bounded sample complexity and some fundamental requirements for learning CoT verifiers.
1.1 Contributions
We introduce formal framework for studying verifiers for Chain-of-Thoupe reasoning. Given any problem statement and sequence of reasoning steps for the problem, we propose the problem of learning verifiers that examine the steps for correctness, and for an incorrect reasoning trace return the first faulty step in the reasoning.
We formally define simple verifiers that have access to random Chain-of-Thought reasoning sequences labeled "correct" or "incorrect" along with the first faulty step. We establish sample complexity bounds for learning good simple verifiers in a PAC (probably approximately correct) sense for verifier classes that are finite or have a finite VC dimension.
We next introduce the more powerful trustable verifiers, which only have access to random problems, and a gold standard reasoner, which provides a small number of guaranteed correct reasoning traces for each sampled problem. We establish PAC learnability of designing verifiers that accept all the gold standard reasoning traces on most problems and never accept faulty reasoning traces, provided that the space of reasoning steps is finite.
We extend our trustable verification goal to the case where there may be a large number of gold standard reasoning traces, but only a random correct trace is available to the learner. We establish upper and lower bounds on the sample complexity of learning a verifier that is always sound (i.e., never accepts an incorrect trace) and accepts most of the gold standard traces on most problems.
1.2 Related work
Chain-of-Thought generation. Chain-of-Thought and its variants WWSS+ 22 ZZLS23 WWS+
YY are gaining popularity as paradigms for studying LLM reasoning. CoT reasoning has known connections with planning for complex tasks (HGM+23), and in fact, our theoretical ab- straction applies to generating plans as well. [JVB+25) study the learnability of a time-invariant autoregressive generator for CoT for a fixed generation length T, and obtain sample complexity logarithmic in T', improving over the linear dependence for time-variant generation in [Ma124]. Their work focuses only on in-distribution generalization. In contrast, our trustable verification model is able to provide strong verification guarantees even for distriibubtonno reasoning, which is crucial in the context of typical CoT generation where the generator may adapt to prompts or feedback. Fur- thermore, we show concrete computational gaps between generation and verification, the functions in the generator class may not be efficiently evaluatable for class of problems for which the verification functions are. We also note an equivalence between special case of our verification model and their generation model, in the sense that an algorithm for one can be used to achieve the other (Remark 4.6). Empirically, LLM-bbsed verifiers have been used to solve specific tasks, even outperforming

---

finetuning-bast based approaches 21) trustable verifiers involve checking proofs with respect to some gold standard reasoners, which may be reminiscent of imitation learning INHB-11
especially with step-by-step verification [LKB Our
YSAN22]
Learning with one-sided error. Our strongest verification model requires the verifier not accept any incorrect proof but possibly miss some legitimate proofs. The formulation bears resemblance to prior work on learnability under one-sided error [Nt877 Kiv95 BB05]. In particular, our learning algorithm is similar to the closure algorithm proposed in this literature, Other related lines of work that offer similar reliability guarantees using blssuee-based algorithms include selective classification [RS88] EYWIO], robustly-reliable learning BBHS22 BHPS23 BS24 BS25] and learning in the presence of strategic improvements (ABN 25 SS22 In addition, we consider learning from only positively
labeled traces (Section 4.2.. A related direction studies learning from positive and unlabeled data for
binary classification [Dn98 DGL055.
Formal methods and learning. Formal verification [CW96 is a sound approach used to verify the correctness of software or mathematical proofs written according to precise formal specifications. Although LLMs have helped improve some formal verification systems [CP24], it is not clear if formal verification can be used to verify the natural language reasoning of modern LLMs [ZSL* 24). A related approach is to use proofs in a functional programming language (say Lean) to build datasets for training machine learning models capable of writing proofs in that formal language (while they also generate natural language descriptions of their proof steps. the evaluation is through correctness of the lean proof). Note that the "verifier" in this interaction is the Lean proof system, which only accepts formal language, while our work studies the learnability of verifiers that may evaluate natural language reasoning directly.
Interactive provers. Our work is related to recent line of work related to interactive provers. Here, the goal is to generate a good prover that not only produces good solution, but is also able to convince a given verifier V about the correctness of its proof. This is complementary to our work in the sense that we show how to actually learn good verifiers from data, which can, in turn, provide good automated benchmarks with respect to which the prover establishes verifiability guarantees. [GRSY21] define a PAC model where the prover is able to convince the verifier on most typical inputs, analogous to our SVPAC model. [AGPR24] develop more powerful interactive provers that provide per-instance guarantees, similar to our TVPAC models. In this context, our work opens up concrete questions for interactive verification Seetfcattonnwwhhherrihh it is possible to achieve better sample complexity of learning verifiers, either assuming provers with certain guarantees or with techniques from active learning [BBL06). [BLM*25 RSS show theoretical as well as practical advantages of verifier-assisted constrained language generation.
2 Setup and Definitions
Let X denote a domain of possible problem statements. For example, an To E X could be a mathematical conjecture, or Satisfiability problem instance, or the description of an initial state in Sudoku game or Einstein puzzle. Let E denote a set of possible reasoning steps; we will think of a "step" as a few tokens, such as [Suppose, for contradiction, that /2 = & for integers a, b] or [Clauses (A V B) and (A V BB imply (A)]. A verifier is function h X E' + {YES, NOJ. where given input (Io, T = (I1, I2, ..., .2.. 2;)) where xo E X and each F; E Σ for 2 1, the verifier should and should output NO if 2, is not a legitimate inference from (Ip, (I1,..., .... 12)1)). Formally, we can allow h to output arbitrarily if (zo, (I1, 1)) itself contains faulty step: that is, "correct" h only needs to output correctly on (Io, (11, F2, ..., rr if (Zo, (I1,..., x1-1)) is itself correct.
output YES if T, is legitimate inference from (Io. (I-1)) ))
xI-1))
Given full reasoning trace proof (zr, (o,,),,,))), verifier h is "run" on the trace by running h on each prefix, that is, M(zo, (x1)). 1( (21, (22), ..., l1(20. (æ1, ...: )). If all of those runs output YES then we define h as saying the reasoning is legitimate, and if any output NO then we define h as saying the reasoning is faulty (and we output the first NO as the location of the first faulty step). We will use H to denote family of verifiers.
Remark 2. We will typically want to emulate the behavior of (or, agnostic verification, at least be competitive with) the best verifier h² E H. In particular, note that our formulation does not involve an explicit notion of verifying whether the reasoning trace "completes" the proof. good verifier may "accept" a reasoning trace if h² accepts it. This is analogous to the notion of CoT generation
3

---

Verifier
SVPAC (Sec.
TVPAC (Sec. 4.1
7-TVPAC (Sec. 4.2
Data format
random tuples
(random problem.
random pairs
(problem, reasoning,
< k gold-standard solutions)
(problem, correct reasoning)
first incorrect step)
Learning Algorithm
ERM on training set
ERM using
Intersection of all consistent
trees [z)
verifiers (Algorithm)
Sample complexity
O(log [H]
Ó(log [H])
{(H))
(finite H)
Sample complexity
O(VCdim(H))
O(VCdim(H))
O(VCdim(H)) (if
(bounded VCdim(H)) (F)
intersection-closed)
Table I:
Different verification goals, training data, learning algorithms and sample complexities. The soft-O and soft-Q notation suppresses dependence on quantities apart from |H] and VCdim(H),
studied by JVB 25
where one hopes to emulate the "correct" generator, although they do not consider the extension to agnostic learning (see Appendix F)).
Remark 2.2. Our use of Chain-of of-Though different from that the original paper WWS 22 where it is used primarily as prompting technique. We use CoT to refer to the standard generation pattern of reasoning models such as o3, Deepseek RI, that is, the model generates the ordered list of intermediate reasoning steps (.1,...; (5T) before its final answer. Our use of the terminology Chain-of-Thooee Chain-of-Thought generation (in contrast, models). Suppose that the language model is given an input question and it produces an output consisting of intermediate steps before arriving at the final answer. This behavior may be due to the nature the training data with such Mmain-of-Thougee sequences as studied the prior works mentioned above, because the language model was prompted to "think step by step".
consistent with prior theoretical work, e.g. [JVB+2] 25 Mal24] which studies study verification of the reasoning produced by such
3 Simple Verification
Let D be a distribution over problems and reasoning traces (ro. (I1,..., v²)) of length S T, including both legitimate reasoning traces and faulty reasoning traces. Assume that have an i.i.d. training sample S of problems and reasoning traces drawn from D, and the traces are labeled according to a perfect verifier h* E H C (YE NO) That is, a trace is labeled YES if every step in is legitimate, and is labeled NO otherwise. Assume that for the faulty traces, the first faulty step in it. We aim to learn a verifier h from such a sample that has a small error over unseen samples from D. Note that make assumptions the size of Σ (the set of all possible reasoning steps) for this result.
are also told which is
Goal: Given the training set S of reasoning traces drawn i...d. from D, our goal is to learn simple verifier h with error at most e over D. Specifically, given a new trace (Io, (#1...., 21)) ~ D, we will run h(2o, (xr)), (aro (21, =22)) ... h( (x1,,..,,<t)) and if all of them output YES then say the reasoning trace is "legitimate" and if any output NO then we say the reasoning is "faulty", and we output the first NO the location of the first faulty step. We say that the learned verifier h is correct on trace (Io,
xx)) if either
(a) the entire trace consists of correct reasoning steps (i.e., h² (1tos (11,
YES for all xT)) ......,,)))))
...,....2...
1 S j I t) and all of h0o, (I1)), h(2o, (I1, M( (Ii,..., xz)) output YES, or
(b) the trace is faulty reasoning and h correctly outputs NO on the first faulty step (and outputs YES up until the first faulty step).
Any other behavior is viewed h making an
the given reasoning trace.
We will use f(h, (ro, т = (I1, x2, ..., 22))) to denote the smallest index j such that the verifier rejects the reasoning sub-trace (zı,..., Mz). that is h(so, (æ1,.... :z))) NO, and set to / otherwise (if no such index exists). That is, f(h, (ro; r)) is the index of the reasoning trace where terminates
its evaluation of (zo,7 7), either by finding faulty step at some index j E [t] or accepting the reasoning

---

as legitimate by evaluating to YES all the way through the last index t. We use this to define the following loss function which gives the 0-1 loss of the verifier h on the input (zo. T)
En (20: T) = l,- (Fo, r)) == I[h(Tr: Ty) + h² (20, Ty) for some j S f(hh, (xo, T))l-
Here 7, = (z1,...., 2y) denotes sub-trace of = (x1 (.1...., 24). Formally, we have the following definition for
learning a verifier from class of verifiers H.
Definition 3.1 (SVPAC-leamable). Let X denote the problem space and let H C (YES, NEES,OO.*x NOJXXX denote the class of verifiers. Then learner is said to simply-verrffably-PP
learn H with sample size m (c, 5) (sample complexity is the smallest such m) if for any h" H. for any e, E (0. 1). for any distribution D over X x Σ" realizable by h" (i.e.. legitimate inference is always given by h,", given a sample S ~ D the learner outputs verifier h such that with probability at least 1 -8 over the draw of S,
(fx- (h, (Zo.7) = 1] S
The learner is said to be proper if E H. Note that our definition above requires the learned verifier h to match the behavior of the correct verifier h- (with high probability) on any reasoning trace drawn from D up to the first faulty step (if one exists) pointed out by h" We will now show that it is possible to learn such a verifier with small sample complexity. First, for the case of finite class of verifiers H. we observe that a simple union-bound based argument implies that we can learn a good verifier with (log [ trace samples. See Appendix B for proof.
Theorem 3.2. Any finite class of verifiers H is SVPAC-learnable with sample complexity (log H + log 3).
We further show that a finite VC dimension of the verifier class is a sufficient condition SVPAC- learn with respect to H. Our sample complexity bounds in this case are O(VCDim H) log T), scaling only logarithmically with the maximum length T of a reasoning trace. We will select h E H by ERM (Empirical Risk Minimization) over the training sample. Note that we will run a verifier h up to T times on any sample trace to determine whether runs correctly on it. Our argument adapts the analogous proof in [JVB
A complete proof is in Appendix B
Theorem 3.3. Any class of verifiers И with fimite VC-dimension VCDim(H) is SVPAC-lcarnable with sample complexity O (1 (VCCCim H) log + log 4)).
Our model for the simple verifiers above allows for learning a verifier from an arbitrary unknown fixed distribution D over the reasoning traces. However, major limitation of this model is that the guarantees only apply to traces drawn according to D. If reasoning model is told that there is faulty step in its reasoning chain (z1,..., then it might modify its reasoning slightly to (..,,..,, xx)) But the new trace no longer from 1) and a verifier trained over samples from Î is not guaranteed to work well on this modified reasoning trace. In other words, the feedback from the verifier may be the very reason why there is a distribution shift. In the following sections, we introduce a more powerful model for learning verifiers that are robust to distribution shifts that may be induced as a natural consequence of receiving feedback from the verifier.
4 Trustable Verification
As discussed above, designing a verifier that only works well for in-distribution reasoning traces may not be desirable in typical scenarios. Motivated by this, introduce model for learning more powerful verifiers which provide strong guarantees for any reasoning trace, as long as the problem statements come from distribution. In particular, we require that for most problem statements, the learned verifiers do not accept any false traces; that is, the learner should be sound. However, we potentially relax the requirement that the learner must accept all correct traces. It turns out that observe two distinct regimes for learnability depending on whether the number of correct reasoning traces is small (and are all available for training) or large (and only a random trace per problem given in the training set).
We will make two additional assumptions in order to achieve the above stronger verification guarantee. First, we assume that correct proofs any problem are given to the learner
Assumptions.
5

---

by a gold standard reasoner X + 2= That is, g(z) denotes set of correct reasoning traces for problem z, and we will have access to some reasoning traces (made more precise below) generated by in our training set. For example, [g(())| = 1 corresponds to there being single correct gold standard reasoning trace for the problem z; which will be available if the problem a is sampled in the training set. A caveat is that we would not be able to verify reasoning traces that are not generated by the gold standard reasoner available to us, even if they may be legitimate. Second, we will assume that the set of legal reasoning steps |X]] is finite.
Our training set S will consist of m problems drawn i.i.d. from some distribution D. For each problem x in the training set, we will run g to create the gold-standard traces, which will be our positive examples. If the number of correct traces is small, we can create negative examples for each way of deviating from the tree of gold-standard proofs (see Section 4.1] Given these examples, our goal is to learn a trustable verifier h that, given a new problem x D and a proposed reasoning trace T for it, is able to verify (with high probability) if the reasoning trace is correct according to g- That is, h is correct on if it will reject all faulty traces x, and will correctly accept most (or even all) traces that match the gold standard g.
Goal:
Using terminology familiar from formal logic, we define the goal for our learned verifiers in terms of sound and complete verification as stated below.
Definition 4.1 (7-completeness w.r.t. and Di stepwise and overall soundness). Given a problem X, set of correct reasoning traces (xx) C ΣT for the problem, and a distribution D/D over traces in g(x). a verifier h X x Σ - NO) is said to y-completely verify x w.r.t g and 1/2 Cx = (r E ET h,,,,,) = YES V prefixes T, r} satisfies E.,, (C((x) n g()x)] 2 y- Furthermore, we say that h 1-completely verifies æ w.r.t. 9 if g(x) S (t))
is said to stepwise soundly verify if whenever h(æ, TT) YES for Tj E EST then T, is prefix of some E g(z) (in particular, this implies (z) S g(z)), and is said to overall soundly verify (1) C ((r).
1 1-completeness corresponds to the learner essentially accepting all the traces that the gold reasoner g deems as correct. In other words, 1-completeness w.r.t. g (omitting the conditional distribution I(,)) means that y-copleteeeess holds in the above definition for y = 1 for all conditional distributions. 17 completeness for small 17 in some more challenging
Later, will relax 1-completeness to y learning settings. We study two types of soundness guarantees- a stronger "stepwise" soundness which guarantees that we reject a proof at the first incorrect step (deviation from gold-standard step) and "overall" soundness that only guarantees that incorrect proofs of length T are rejected. Note that stepwise sound verification implies overall sound verification, but the converse may not necessarily hold.
Remark 4.2. We note that soundness and completeness of proof systems is a terminology also used in formal verification and logic, and caution the reader against conflating them with our notions. A soundness guarantee for deductive system expresses that all provable sentences true. Completeness states that all true sentences are provable. While there is an analogy, we remind the reader that our study applies to natural language reasoning while formal logic involves proofs expressed in a very precise formal language and their verification.
4.1 Sample complexity when the number of correct proofs is small
In this section, we will assume that the number of gold standard reasoning traces for any problem of interest in X is small. That is, [g(z) is bounded by small constant & for any E x In this case, it is reasonable to expect that we have access to all the gold standard proofs for any problem x in the training sample. We show how to create training samples for learning verifier using g and establish sample complexity bounds for learning verifier classes that are finite or have finite VC dimension.
Formally, for each problem æ in the training sample S ~ Dm, we will run g to generate all the gold standard proofs. These will be our positive examples. To generate negative examples, we consider the first step of deviation from any correct trace for and add negative example corresponding to it. Let
A natural example for the case k = 1 could be SoT-solver or an Mixed Integer Program solver where the gold-standard solver g deterministic branching rule that we know works pretty well.

---

Tx(2) denote the tree of positive traces on the problem instance x. The root of the tree is the problem statement z, and each node represents a valid reasoning step according to one of the positive traces in has at most k leaf nodes. Now we create negative examples for g(z). By assumption on [ Ty(2)
each internal node 24 of Ty (z) as follows. Let (ão = z; T1..... 3. = x;) denote the path from the root to z; on T (a)), and X; C Σ denote its set of child nodes. Then for every x' E Σ X we create a faulty trace (To, $1,,.. 1;- z") and add it as a negatively labeled example for the problem x.
Finally, we formally state the definition of trustable verification. Notably, we require the learned verifier to be both complete (w..t. the gold standard g) and sound on problems drawn from D. In contrast to simple verifiers, the traces that we expect trustable verifier to verify can be arbitrary.
Definition 4.3 (stepwise and overall TVPAC-ccamable) Let X denote the problem space and let H S {YES, ]
[YJS,NO).M X x denote the class of verifiers. Let g(x) C E" denote the set of correct reasoning traces for any E X. Then a learner is said to stepwise (resp. overall) mustably-verrfiaallyPP H with sample size m = M(,, 5) (sample complexity is the smallest such m) if for any h- E H, for any e. 6. (0. 1), for any distribution D over X realizable by h" (i.e. for all z, g(z) Ca- (2)
learn
{T ET h- (z. T2) = YES A prefixes T, of T.), given a sample S ~ D and for each x E S given
access the set g(x), the learner outputs a verifier h such that with probability at least - 5 over the
draw of S, Prz-Dll [h is 1-complete w.r.t. 9 and stepwise (resp. overall) sound for æ] 2 1 - c. The learner is said to be proper if h E H.
For the case of a finite verifier class H, we can still show a O(log H| upper bound on the sample complexity of learning good verifier. A proof is located in Appendix
Theorem 4.4. Any finite class of verifiers H is stepwise TVPAC-leamable with sample complexity [log([||]) + log 2)).
We further show that it is possible to stepwise TVPAC-leam any verifier class with finite VC- dimension (complete proof in Appendix[[]
Theorem 4.5. Any class of verifiers H with finite VC-dimension VCDim (H) is stepwise TVPAC- learnable with sample complexity O ( (VCCDmm(H) log(kT El) + log f)). where ks is bound on the number of correct proofs generated by
Some remarks are in order. Our stepwise trustable verification model has an interesting property that good verifiers in our models for any problem x not only guarantee correctness of the reasoning steps so far, but also prompt the reasoner away from possibly legitimate reasoning steps which may not however result in a solution for the problem x. This additional stronger property is not achieved by overall TVPAC verifiers. In fact, for the special case [g(x)] equivalent to the Chain-of- Chain-of-Thought autoregressive generation model of [JVB+25) This is surprising as verifying a proof is usually believed to be easier than generating it (although formally an open question, for instance determining whether P * NP), but the strong "guiding" abilities of our verifiers can be used for generation.
1. our verification model is
Remark 4.6. For A = 1, our stepwise trustable verification model is equivalent to the generation model of [JVB+25) provided |Σ| is small, in the sense that an efficient algorithm for verification implies efficient algorithm for generation, and vice versa. To see this, given stepwise sound verifier that is guaranteed to accept only the single gold standard trace g(x), we can generate the correct proof using h as follows. Run hi2,, To) for each T) E Σ until one of them, say 31, yields YES. Now run h(z, (II, Ti) T) for each Ti until acceptance, and so on. Doing this T times generates a proof for x that matches (x)) Conversely, to verify if generator is correct on a problem x, we can simply match its reasoning trace against g(x). An interesting consequence of this is that we can hope to use a good verifier to train a good reasoner.
Thus, there is an equivalence between stepwise TVPAC verifiers and CoT generators (provided the size of the reasoning space [X] is small). However, the equivalence breaks down for large |E], and does not hold for overall TVPAC verifiers. In the following remark, we show a computational gap between proving and verification. Namely, for the same problem space, the proof generation functions may not be efficiently evaluatable even though the verifier functions can be evaluated in polynomial time.
Remark 4.7. Computationall gap between CoT provers and TVPAC verifters. We first provide a concrete example showing computational separation between CoT generators and overall TVPAC
7

---

Algorithm 1 Intersection of Consistent Verifiers
Require: Set of positive problem-trace examples S {(x0), )(1),,... ..., (a(m), {(m))} where
2111) hid D2y(1) lid. Diz00, verifier class H. 1: Hs < {h E H h(x,T) = 1 for all (2, S}.
(Set of verifiers consistent with S) 2: return h': (I, H h(,,T [predict YES only when every consistent h predicts Y
verifiers. Let X be the set of all satisfiable USAT (Unique-SAT problems in variables and consisting of m clauses. Suppose each reasoning step consists of single variable assignment, i.e., {0, 1}. Then it is easy to construct verifier function h that is efficiently computable and is [n]] E=
both complete and overall sound. Given a problem-prood pair (z) the verifier simply checks that no variable is given multiple inconsistent assignments, each variable appearing in æ: has an assignment, and each clause æ satisfied. On the other hand, by the Valiant- Vazirat theorem [VV85], USAT has no polynomial-time randomized algorithm (assuming RP & NP). Therefore, there is no efficiently computable proof generator for all problems in X. The above argument can also be extended to stepwise TVPAC verifiers by using an exponential-sine
7).
D. In the USAT example above, could consider one-step proofs (E {0, 1) (*)) which set all the variables in single step. In this case, the reduction Remark 4.6 is no longer polynomial time since |ا| 2".
4.2 Linear sample complexity for any number of correct proofs
We will now consider an extension to our trustable model where we no longer assume a small bound on the number of gold standard traces for every problem X. This would make it unreasonable to expect the gold standard reasoner g to generate all proofs for a given problem instance r. Instead, we would only require it to generate a random correct proof. For an example, one could think of randomized solvers for constraint satisfaction problems. We will relax the goal of being perfectly complete w.r.t. g (Definition 4.1) to being almost perfectly complete, while still requiring the verifier to be (overall) sound. In this subsection, we assume soundness refers to overall soundness throughout.
Our training set S will consist of problem-trace pairs (Ir,7) r) where is a random correct trace from g(x). We learn from only positively labeled examples. Formally, we have the following definition.
Definition 4.8 (G-TVPACCleamabbll) Let X denote the problem space and let H S [[EES,NO) XxX" denote the class of verifiers. Let gxx) C ΣT denote the set of correct reasoning traces for any x E X. Then a learner said to p--rrusaably-verrfibblyy
learn H with sample size m M(e, 6) (sample complexity is the smallest such m) if for any ho E H, for any e, E (0, 1), for any distribution D over X realizable by h", given a sample S ~ 1mmh and for each xx(() S given access to random frace Tz00 E D sampled according to D over g(x((), the learner outputs a verifier h such that with probability at least - ó over the draw of S and the traces, Pr is --complete w.r.t. and Dr and a sound verifier for æ] 2 1
An interesting special case is where D/2 is the uniform distribution over g(x) for all x. Here, would uniformly select one of its correct proofs when queried for generating the training set, and y-completeness corresponds to accepting at least a y fraction of the correct proofs of g. For this more challenging setting, we first show the existence of improper learner that achieves learnability in the case where the verifier class H is finite. Our algorithm (Algorithm I outputs the intersection (agreement region) of all consistent verifiers with the training set. We show bound on the sample complexity of Algorithm [ which is linear in [/]-
Theorem 4.9. Let 10. For any finite class of verifiers H, Algorithm (1-1) - TVPAC-leams
H with sample complexity O L (IH + log 5)). Moreover, Algorithm never accepts a faulty trace for any problem x E X.
zye
Unique-SAa SAT is a promise problem, the decision version of which asks whether given Boolean formula, which is promised have either zero or exactly one satisfying assignment, has exactly one satisfying truth assignment. The search version of the problem further asks to determine the unique assignment.
8

---

Proof. Overview. Let D* denote the joint distribution over problem-trace pairs (z, r) induced by the marginal distribution D and the conditional distribution D used to sample positive traces from g(x). We will show that the expected error of the verifier learned using Algorithm| | on a test pair
(2, D+ is at most O | + with probability at least 1- 6. We will further show that the errors are one-sided, i.e. we never accept faulty trace for any problem Finally, using the law of total expectation, we show that this implies the stated bound on the sample complexity.
m
Bound on generalization ervor. We define the population error of h E (YES, NO) (any verifier, not necessarily in H) on positive examples as Lp+ (h) = PT(a,))---Ihb r) = NOJ. For each
verifier h4 E H, let ph. = (I(a,.)>>++ [2, 7) = NO and h (2, = YES] be the probability that h; incorrectly rejects valid reasoning trace.
By the realizability assumption, h* E Hs for any sample (recall that Hy the set of verifiers consistent with S. Algorithm I. Since h' (x, r) = M h(x, r), the error of h' occurs only when least one h E Hg incorrectly rejects valid trace. Thus,
L.D- (hh) = Pr [N((x,))= NO and h² (x; (I, = YES)
(2,r)=D
Pr [3h Hs s.t. h(,, r) NO and h" (a, YES] (a.t)nn
Σ
Ph
he
For any subset T [ H, define
L (T) == Pr (2,5)/Dt
3h E s.t. h(x,7) = NO and h" (x, YES].
Note that since h TT( = NEE h(,, T), we have the exact identity L. (h²) I (Hs).
Fix > and let Tg = {T C H: L (T) 2 t}. If L- (h) 2 E, then Hg E Tg. Therefore, by union bound,
Pr[LDt (h') c| = -PiHHs E Tel
Σ Pr|Hs S
- S
Pr[T S Hsl. S
TET.
TET.
For fixed T, the event T S Hs means that every h T outputs YES on all samples. Equivalently, none of the m samples falls into the event defining Lp+ (T). Since the m samples are i.i.d., we get
Pr(T C Hs] = (1 - I.p+ (T)) Th S (1 - e)m
Thus,
Pr( (h') 2 e) < [Tl (1 < 2 (1 2)T S < - g
Setting the RHS to be at most å gives = | 24))( Therefore, with probability at least 1 8,
H 2n + In(1/5)
LD (h')
m
We never accept a faulty trace. By construction, N [z(x, Ane M,,,), This means h (.,,7) 7) YES only if all h E Hs output YES for (z, T). Since Hs is set to be the set of all verifiers consistent with the training data S, and we assume by the realizability assumption that h" E H, we have ht E Hs. Therefore, if fz(xz, T) = YES, then h (xx r)= YES as well. This guarantees that h' never accepts an invalid reasoning trace, i.e., h has zero false positive rate.
Sample complexity bound. We say that x E X is a bad problem if h/' not (1 17) completee w.r.t. on (i.e., h accepts fewer than (1 7) fraction of correct traces in g(z) in expectation according to 1Iz)). We say that is a bad trace for a problem x, 7 is valid according to g but not according is not bad but is bad for
to h'_ If Nt' makes error on (). then either x: is bad problem,
x. Let c = Prp (2: is bad]. The total error of h', L (h') 2 c Pr Dj. [r is bad x is bad] 2 on. Using
the above bound on T.D+ (h'), we get with probability 8, en S T.px (h²) S implies the claimed sample complexity bound.
|F In 24 which
m
D

---

Note that our upper bound above makes no assumption on H. other than it is finite. If H is intersection-cloeed (that is, intersection of verifiers in H is also in H). Algorithm| corressoonds the closure algorithm and h'' E H. In this case, we have much nicer bounds on the sample complexity Óllo ) for finite H and O(VCDim H)) for H with finite VC dimension (see Appendix D). As a simple example, suppose the set of reasoning steps Σ consists of n axioms. The verifier class H consists of 2" cenfffers-correspponie
to each subset C E, there is ha E H such that ho only accepts traces that consist of reasoning steps from o. In this case, the sample complexity of Algorithm iis ((n) instead of (22)). See Appendix E for additional examples.
Lower Bounds. We further show that the linear dependence on H in our upper bounds on the sample complexity of trustable verification (given random access to positive proofs in the sense of Definition 4.8) is unavoidable without further assumptions on H. Roughly, if we do not have a bound on the number of correct reasoning traces from any given zo. and if we want to learn verifier h E H such that for most zi. we have both (a) h accepts al least half of the correct reasoning traces from To and (b) h rejects all faulty reasoning traces from To. then without further assumptions on which traces are correct, in the worst case we will need a training set with Q(HH) reasoning traces, for any [H] < E This is in contrast to the (log H)) bound in Section 4.1 when we had only a single correct trace (or a few correct traces) per Zo-
Our first result states that if we want to output a sound proper verifier, i.e. h E H and we only require condition (b) above, then we already need least ((H)) samples achieve TVPAC learnability for any learning algorithm. A proof is in Appendix [
Theorem 4.10. Let ]- 2 2. For each size 3 S H S |>]" there exists a finite class H with |M] = H such that any proper learner that T-TVACC learns H (for any E 2 0, i.c. the learned verifier is only required to be sound) has sample complexity at least ((Hl)).
We next show that if we further require the learner to even accept at least a constant fraction of the correct traces (say & -completeness), in addition to soundness, then the linear lower bound on sample complexity holds even for representation independent learning, i.e. even if we allow the learner to output verifiers that are not in the verifier class H (proof in Appendix C.)
Theorem 4.11. Let [ 2 2. For each size H < EΣ|T there exists finite class H with |H| = H such that any (proper or improper) learner that TVPACC learns H has sample complexity at least ()
5 Discussion
Verification that can be trusted is strong candidate approach towards powerful automated benchmarks for Chain-of-Thooulee reasoning. While verification using formal methods has been successfully deployed for testing software and proofs in formal systems, the task of verifying natural language rea- soning seems more challenging. We propose a learning- based approach to designing such verifiers and introduce various verification models with different strengths of guarantees. Our simplest framework consists of verifiers that learn from random proofs from some fixed unknown distribution D annotated with their first faulty step (or correct, if the entire proof is good). Such a verifier would be able to cor- rectly annotate new reasoning sequences from the same distribution, but is not robust to distribution shifts (for example, due adaptive editing of proofs by incorporating the feedback from the verifier). We next address a stronger type of verifiers that guarantee to reject any faulty reasoning (possibly very different from the incorrect proofs seen in the training set), by accepting only proofs that adhere to certain gold standard. We call these verifiers trustable and show two distinct regimes for their learnability- small sample complexity when there a small number of gold standard proofs for any problem, and an unavoidable larger sample complexity linear in the size of the verifier class without this assumption. This raises an interesting question-ant are there alternative assumptions or models for interactive verification where our linear lower bound on the sample complexity may be circumvented?
Acknowledgments
We thank Feras Saad for pointing out an issue in the original proof of Theorem 4.9 which we subsequently fixed. This work was supported in part by the Simons Investigator Award MPS-SICS- 00826333, a Microsoft Research Faculty Fellowship, and the National Science Foundation under grants CCF-2212968. ECCS-2216899, and 2CC9-2216970.
10

---

References
[AB99] Martin Anthony and Peter Bartlett. Neural network learning: Thcoretical foundations. 1999.
[ABN+25] Idan Attias, Ayrim Blum, Keziah Naggita, Donya Saless, Dravyansh Sharma, and Matthew Walter. PAC learning with improvements. In Forty-second International Conference on Machine Learning. 2025.
[ACB98] Peter Auer and Nicolo Cesa-Bianchi. On-line learning with malicious noise and the closure algorithm. Annals of Mathematics and Artificial Intelligence, 23:83 --99, 1998.
[AGPR24] Noga Amit, Shafi Goldwasser, Or Paradise, and Guy N Rothblum. Models that prove their own correctness, In ICML 2024 Workshop Theoretical Foundations of Foundation Models, 2024.
[Ang88] Dana Angluin. Queries and concept learning. Machine learning 2(4):319-342, 1988.
[A007] Peter Auer and Ronald Ortner. new PAC bound for intersection-closed concept classes, Machine Learning, 66(2):151-163, 2007.
[BBOS] Nader Bshouty and Lynn Burroughs. Maximizing agreements with one-sided error with applications to heuristic learning. Machine Learning, 59(1):99-123, 2005.
[BBHS22] Maria-Florina Balcan, Avrim Blum, Steve Hanneke, Dravyansh Sharma. Robustly-reliable learners under poisoning attacks. Conference on Learning Theory (COLT), pages 4498-4534. PMI.R 2022.
[BBL06]
Maria-Florina Balcan, Alina Beygelzimer, and John Langford. Agnostic active learning. In Proceedings of the 23rd International Conference on Machine Learning, pages 65-72, 2006.
[BCD+22] Nataly Brukhim, Dan Carmon, Irit Dinur, Shay Moran, and Amir YehudayofI. A characterization of multiclass learnability, 2022 IEEE 63rd Annual Symposium on Foundations of Computer Science (FOCS). pages 943-955, 2022.
[BHPS23] Maria-Florina Balcan, Steve Hanneke, Rattana Pukdee, and Dravyansh Sharma. Reliable learning in challenging environments. Advances in Neural Information Processing Systems (NeurIPS), 36:48033-48050, 2023.
[BLM*25] 25] Edoardo Botta, Yuchen Li, Aashay Mehta, Jordan T Ash, Cyril Zhang, and Andrej Risteski. On the query complexity of aesifier-assisted language generation. In Forty-second International Conference Machine Learning, 2025.
[BS24] Avrim Blum and Donya Saless. Regularized robustly reliable learners and instance targeted attacks. arXiv preprint ar 2410: 10572, 2024.
[BS25]
Maria-Florina Balcan and Dravyansh Sharma. Learning reliably under adversarial attacks, distri- bution shifts and strategic behavior. Workshop on Reliable ML Unreliable Data (NeurIPS). 2025.
[CKB 21] Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, Christopher Hesse, and John Schulman. Training verifiers solve math word prohlems. arXiv preprint arXiv:21 14168, 2021.
[CP24] Itay Cohen and Doron Peled. LLM-based scheme for synthesis of formal verification algorithms. In Bridging the Gap Between Al and Reality AISoLA, 2024.
[CW96] Edmund Clarke and Jeannette Wing. Formal methods: state of the and future directions. ACM Computing Surveys (CSUR), 28:626-643, 1996.
[Dar15] Malte Darustädt. The optimal PAC bound for intersection concept classes. Information Processing Letters, 115(4))458-461, 2015.
[Den98] François Denis. PAC learning from positive statistical queries. In International Conference on Algorithmic Learning Theory (ALT), 1998.
[DGL05] François Denis. Rémi Gilleron, and Fabien Letouzey. Learning from positive and unlabeled examples. Theoretical Computer Science, 348:70-83, 2005.
[ЕYI00] Ran El- Yaniv and Yair Wiener, On the foundations of noise-free selective classification. Journal of Machine Learning Research, 11(5), 2010.

---

[GLLS25] András György, Tor Lattimore, Nevena Lazić, and Csaba Szepesvári. Beyond statistical learning: Exact learning essential for general intelligence. arXiv preprini 233,,88,,,,,3908 2025.
[GRSY2I] Shafi Goldwasser, Guy N Rothblum, Jonathan Shafer, and Amir Yehudayoff: Interactive proofs for verifying machine learning. In 12th Innovations in Theoretical Computer Science Conference (ITCS 2021). pages 41-1. Schloss Dagstuhl-Lent Lei--LLeiinnninnieee Zentrum für Informatik, 2021.
[Han16] Steve Hanneke. The optimal sample complexity of PAC learning. Journal of Machine Learning Research (JMLR), 17(38), 2016.
[HGM*23] Shibo Hao, Yi Gu, Haodi Ma, Joshua Hong, Zhen Wang, Daisy Wang, and Zhiting Hu. Reasoning with language model planning with world model. Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, pages 8154-88 8173, 2023.
[3MR*23] Steve Hanneke, Shay Moran, Vinod Raman, Unique Subedi, and Ambuj Tewari. Multiclass online learning and uniform convergence. The Thirty Sixth Annual Conference on Learning Theory (COLT7) pages 5682-5696. PMLR, 2023.
[HMZ24] Steve Hanneke, Shay Moran, and Qian Zhang. Improved sample complexity for multiclass PAC learning. In Neural Information Processing Systems (NeurIPS), 2024.
[HSW90] David Helmbold, Robert Sloan, and Manfred K. Warmuth. Learning nested differences of intersection-closed concept classes. Machine Learning, 5(2):165-196, 1990.
[JV 25] Nirmit Joshi, Gal Vardi, Adam Block, Surbhi Goel, Zhiyuan Li, Theodor Misiakiewicz, and Nathan Srebro. A theory of learning with autoregressive chain of thought. Conferennce on Learning Theory (COLT), 2025.
[Kiv95] Jyrki Kivinen. Learning reliably and with one-sided error. Mathematical systems theory, 28:141- 172, 1995.
L3] Zhan Ling, Yunhao Fang. Xuanlin Li, Zhiao Huang. Mingu Lee, Roland Memisevic, and Hao Su. Deductive verification of chain-of thoouuh reasoning. Advances in Neural Information Processing Systems (NeurIPS), 36:36407-36433, 2023.
ILKB 24] Hunter Lightman. Vineet Kosaraju, Yuri Burda. Harrison Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe. Let's verify step by step. In The Twelfih International Conference on Learning Representations, 2024.
[Ma124] Eran Malach. Auto-regressive next-token predictors universal learners. In International Conference on Machine Learning (ICML), pages
PMLR, 2024.
[Nat87] B. K. Natarajan. On learning boolean functions. In Proceedings of the nineteenth annual ACM Symposium on Theory of computing (STOC), pages 296-304, 1987.
[Nat04] B. K. Natarajan. On learning sets and functions. Machine Learning, 4:67-99 97, 2004.
[NHB*21] Reiichiro Nakano, Jacob Hilton, Suchir Balaji, Jeff Wu, Long Ouyang, Christina Kim, Christopher Hesse, Shantanu Jain, Vineet Kosaraju, William Saunders, al. Webgpt: Browser-assiste question-anssering with human feedback. arXiv preprint 1:X0v:2112.09332, 2021.
[RS88] Ronald Rivest and Robert Sloan. Learning complicated concepts reliably and usefully. In Pro- ceedings of the Seventh AAAI National Conference on Artificial Intelligence, pages 635-640, 1988.
[RSS 25] Dhruv Rohatgi, Abhishck Shetty, Donya Saless, Yuchen Li, Ankur Moitra, Andrej Risteski, and Dylan J Foster. Taming imperfect process verifiers: A sampling perspective on backtracking. arXiv preprint arXiv:2510.03149, 2025.
[SS25] Dravyansh Sharma and Alec Sun. Conservative classifiers do consistently well with improving agents: characterizing statistical and online learning. Advances in Neural Information Processing Systems (NeurIPS), 2025.
[SVK24] Kaya Stechly, Karthik Valmeekam, and Subbarao Kambhampati. Chain of thoughtlessness? An analysis of CoT in planning. In The Thirty-eighth Annuul Conference Neurul Information Processing Systems (NeurIPS), 2024.
[TB07] Ambuj Tewari and Peter Bartlett. On the consistency of multiclass classification methods. Journal of Machine Learning Research (JMLR), 8:1007-1022 1025, 2007.
12

---

[VV85]
Leslie Valiant and Vijay Vazirani. NP is easy detecting unique solutions. In Proceedings of the seventeenth annual ACM Symposium Theory Computing, pages 458 3584463, 1985.
[WWS 22] Jason Wei, Xuezhi Wang. Dale Schuurmans, Maarten Bosma, Fei Xia, Ed Chi, Quoc V Le,, and Denny Zhou. of prompting elicits reasoning in large language models. Advances in Neural Information Processing Systems (NeurIPS), 35:24824 24837, 2022.
[3WS*23] Xuezhi Wang, Jason Wei, Dale Schuurmans, Quac V Le, Ed H Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou. Self celf-consistency improves chain thought reasoning in language models. In The Eleventh International Conference on Learning Representations (ICLR), 2023.
[YSAN22] Mengjiao Sherry Yang, Dale Schuurmans, Pieter Abbeel. and Ofir Nachum. Chain thought imitation with procedure cloning. Advances in Newral Information Processing Systems, 35:36366- 36381, 2022.
[3Y Shunyu Yao, Dian Yu, Jeffrey Zhao, Izhak Shafran, Tom Griffiths, Yuan Cao, and Karthik Narasimhan. Tree of thoughts: Deliberate problem solving with large language models. Ad- vances in Neural Information Processing Systems (NeurIPS), 36:1 06:11809--1 1809-18822, 2023.
[ZSL 24] Jin Peng Zhou, Charles Staats, Wenda Li, Christian Szegedy, Kilian Q. Weinberger, and Yuhuai Wu. Don't trust: Verify grounding LLM quantitative reasoning with autoformalizaionn. International Conference on Learning Representations (ICLR), 2024.
[ZZLS23] Zhuosheng Zhang, Aston Zhang, Mu Li, and Alex Smola. Automatic chain of thought prompting in large language models. The Eleventh International Conference Learning Representations (ICLR), 2023.
13

---

A Additional Related Work
Multiclass classification. Our verifiers not only predict whether a proof is correct or faulty, but also indicate the first incorrect step in the chain of reasoning. The output of the classifier thus takes one of T+1 values (correct, or first fault at step E [T]) and can be thought of special type of structured multiclass classification. Multiclass classification has been extensively studied to understand how learnability is affected by the number of different label classes [Na004] [B07], with a recent focus on infinite class size [BC++22 |MR+23] [MM244] The latter raises an interesting open question regarding the learnability of CoT reasoners and verifiers for arbitrarily long traces.
Exact learning. Recent work [GLLS25] argues for the need to study exact learning [Ang88) for sound deductive reasoning. Our work represents advances towards exact learning for verifiers in several ways. First, our "trustable" verifiers are robust to distribution shifts of reasoning traces (although not of problem statements, so not exact learning)-in particular when we are "correct" for a problem statement, we are sound on all the reasoning traces for it. Second, we give an example where we achieve online verification with finite mistake bounds (see Example|E.3) which can be viewed as an example of exact learning. Here we bound the total number of mistakes over problem and reasoning pairs on an arbitrary sequence. [GLLS25 argue that powerful verifiers may be useful in achieving exact learning for the reasoners as well.
B Omitted proofs from Section
3
We include here proof details for the results on SVPAC learning in Section S
B.1 Proof of Theorem
Proof. We will simply output any verifier h E H that is consistent with the training sample (i.e. makes no error) and show that it achieves the desired low error for any sample size that is larger than the stated sample complexity. Fix some verifier with error 2 é over D. This means that for random reasoning trace x (Zo: (....... 2x)) ~ D. with probability 2 c, h makes mistake, that is. (x(x) = 1. So, this means that the probability that h does not make mistake on any example E S is at most (1 e)1s1, We now set this to | and solve for |S| = (log( H)) + log }).
L
B.2 Proof of Theorem 3.3
Proof. We will select l E H by ERM (Empirical Risk Minimization) over the training sample (in the realizable case this corresponds to selecting a consistent verifier). Note that we will run a verifier up to T' times on any sample trace to determine whether it runs correctly on it. We adapt the analogous proof for CoT generation due to JJV Let Ty be shorthand for reasoning sub-trace (I1,..,,,) xz)). Recall that the loss function on a given input (Zo. (x1 22 ..,, (.)) is given as
en (To, T) [[h(Fo, Tj) + h" (2o. T;) for some j S f(h', (zo, 7))]
and we define the corresponding function class C# {lr h H}.
Now, given a sample S = ((=g0) ,(1)), (x) (m) (=(mm),(())) (m)))) ) of size m, we are interested in the number of different behaviors of functions E H over the sample. The shattering coefficient
Tex (S) ([((((=0) (1) ,())),)))))))))),),)))))))))),
(n(abm)) ((m))) h E H)|
- 1((((a0)) 15 Mie h HY < (nntt))
(1) (10)
where we have used that if l,, (Zo, T) # (In, T) then (2o, Ty) # h2 TT) for some j e [T].
Using Sauer's 's lemma, for any m > T
VCDim(H) H)
we have
VCDim(H)
em?
Tea (m) < (m((m))
<
VCDim(H)
14

---

A standard lemma (e.g. [BB9)] Appendix 1) now implies that VCDim(Cx) - VCDim (H) log T. where T is the maximum length of a reasoning trace.
C Proofs from Section
We include here proof details for our results on TVPAC learning in Section
C.1 Proof of Theorem
Proof. We will simply output any verifier H that makes no error on the training sample. Assume that h has error 2 c over D. This means that for each Zo E S, with probability 2 h will make a mistake on at least one of the examples created from zg. Recall that a mistake here may be one of two kinds, either (a) h accepts any other reasoning trace [(x) & g(zo), in which case h must say YES to at least one of the negative examples in that was produced from zig specifically, must have mistakenly accepted one of the traces (ro,,... -......... 1(, where is the index of the first step where fzo) deviates from Ty (zo). or (b) h fails to accept some reasoning trace in g g(20), which
is labeled YES in the sample. So. the probability that h does not make a mistake on any example To E S is at most (1 - c)
We now set this to 5/|H| and solve for [S].
C.2 Proof of Theorem 4.5
Proof. We select h e H by Empirical Risk Minimization over the augmented training sample (with positive and negative examples created using g(z)) described above (by realizability this corresponds to returning any consistent verifier). Note that we will run verifier h up to k7 k times on any sample trace to determine whether it runs correctly on it. The proof is similar to that of Theorem 3.3 Let Ty be shorthand for a reasoning sub-trace (Z.,.....,)) Define loss function on given input (zo, T = (I1, F2, .... zx))
(x T) =- [1/ Tτ) # h" (1o, Ty)] for some j [t],
where h" is the verifier in H that accepts exactly the correct traces according to g, and let the corresponding function class be L (ēn h E H).
Now given sample S ((=g)) _g(=0)) )) ..., (=) (a(()) (((=))))) of size m, we interested in the number of different behaviors of functions h E H over the sample. Given a collection of correct traces g(zo). define Tg (zo) as the collection of all the sub-traces of traces in g(zo) along with one-step deviations of these sub-traces. Notice (Tg S KT|E for any 20. The shattering coefficient
T2(S)= = ((() (a(t gg(0
(m)
h E HH
S [(h(z)') ()) 5)) s))e E H)]
< <T (mkTT))))
where we have used that if e, (zo. T) # (0o, r) then hy (z0, F) # h2(wo, 7) for some i E (2o).
Using Sauer's lemma, for any m 2
VCDim(H) we have
kT
emkTTj]
VCDim(H)
[e(m) < I mn
VCDim
A standard lemma (e.g. [AB99] Appendix 1) now implies that VCDim(C) s VCDim(H) log where T is the maximum length of a reasoning trace.
k7 D))
C.3 Proof of Theorem 4.10
Proof. Select an arbitrary problem 2o E X and set D to be the constant distribution with support {zo}. Also set the conditional trace generating distribution D imo to be the uniform distribution over
g(2o) (we will set g later). Let | = b > 2, so there are 6" possible reasoning traces of length T
15

---

from To. Given H I b". arbitrarily partition the 6" reasoning traces into H disjoint sets Si.... Sg. each of size least 1 Now, define the verifier class II {K1,.... heg where h; accepts all reasoning traces except those in S,.. That is, if Cn = (t ΣT h(t) = Y denotes the set of traces accepted by h, then Cz, = Σ"' \ S₁. Since we have no assumptions on which or how many traces are correct besides realizability, we stipulate that all b" traces are correct except for those in Si- for some uniformly randomly chosen index 8".
Now, proper learner must output some h; E Н. Suppose that the size of the training set S is at most H/2. The learning algorithm which is required to output some h; E H can correctly choose h; = h4- with probability at most 2/H since it is equally likely that any of the consistent verifiers is the right one. Note that in our construction hę- is the only sound verifier in H. Thus,
Pr[h not sound] 2 21- 2 1 - 2 z/4 Thus, is impossible to achieve error 1/4 using m S H/2 samples, establishing the desired lower bound of (HH)).
C.4 Proof of Theorem 4.11
Proof. Our initial setup is similar to the proof of Theorem 4.10 { D, p0 9 and H. For simplicity, assume that H is multiple of 4.
That is, we have the same X
Suppose the training set S has size at most H/4 (i.e. there are at most H/4 labeled reasoning traces available, selected uniformly at random from g()))). Any learned verifier h that is 2 j-complete (i.e. accepts at least half of the reasoning traces accepted by h4-) must accept traces from at least H/4 distinct sets S, that were not observed in training data. Notice that these H/ 4 sets constitute at least 1/3 of the 3H/ 4 sets S; not observed in the training traces. This means that for i* randomly selected from these 3H/4 values, with probability at least 1/3, h accepts a trace in Si.. Thus any 2 ccomplete verifier fails to be sound with probability at least 3-- Thus, it is impossible to achieve error e < using m S H/4 samples, establishing the desired lower bound of (H)..
D Intersection-closed Verifier Classes and 7- TVPAC Learning
The learnability of intersection-closed concept classes in the standard PAC model is well-studied problem (HS ACB98 A007 Dar15). Optimal sample complexity for these classes was known before Hanneke established the celebrated optimal bounds for (improper) PAC learning of arbitrary concept classes [6 Here we will show that our lower bounds on sample complexity of arbitrary -TTVPAC learning Section 4.2 can be circumvented for intersection-closed verifier classes H. We will use X' ;= X x n to denote the domain of the verifiers. We start with some standard definitions restated in the context of verifier classes.
Definition D.1 (Closure operator of a set). For any set S C X and any verifier class H C 2*x the closure of S with respect to H, denoted by CS) 2 + 22x is defined as the intersection of all verifiers in that contain S, that is, Closx(S) hEH,
N h.
In other words, the closure of S is the smallest verifier in H which contains S. (h H S 9, then Closs(() = X. This allows us to formally define intersection-clos verifier classes.
Definition D.2 (Intersection-closed classes). A verifier class H c 2 is intersection-closed if for all finite S C X. Clos и (S) E H. That is, the intersection of all verifiers in H containing an arbitrary subset of the domain belongs to H. For finite verifier classes, this is equivalent to saying that for any h1, h2 E H, the intersection h, O h2 is also in H [at877]
Examples of intersection-closed classes include axis- parallel d-dimensional hyperrectangles, intersec- tions of halfspaces, k-CNF boolean functions, and subspaces of a linear space.
The Closure algorithm is a learning algorithm that generates a verifier by taking the closure of the positive examples in given dataset, and negative examples do not influence the generated verifier (in fact, negative examples are not available our 7- TVTPAC model). The verifier returned by this algorithm is always the smallest verifier consistent with all of the positive examples seen so far in the training set. Note that Algorithm Tis is exactly the closure algorithm for intersection-closed verifier classes.
16

---

Definition D.3 (Closure algorithm N HSW90)) Let S = {( = (z1))), ..... (Tm. Mm
(z))) be set of labeled examples, where f E H, 3; E X and yi E {0, 1}. The verifier hi
produced by the closure algorithm is defined as:
hz(z)) = 1, i Closh (1a; S y4 = 13),
0, otherwise.
Here, CloSH (fa; S: 1/4 = 1}] denotes the closure of the set of positive examples in with respect to H.
The closure algorithm learns intersection-closed classes with VC dimension with an optimal sample complexity of θ (d + log })) [A007 Dar1S]. We can use this to establish 7-TVPAC learning for arbitrary intersection-closed verifier classes with finite VC dimension. Note that our sample complexity bounds in this case are independent of the length T of the reasoning trace.
Theorem D.4. Let 1 E (0, 1). Let be class of verifiers that is intersection-closed and has finite VC dimension VCDim(H)) (H). Algorithm [ TVPACCleaass H with sample complexity
O 1 (VCDim(H) + log ))) Moreover, Algorithm never accepts faulty trace for any problem X.
Proof. Let D denote the joint distribution over problem-trace pairs (æz, r) induced by the marginal distribution D and the conditional distribution Í used to sample positive traces from g(x). Note that in Algorithm| [ the intersection of consistent verifiers h H since H is intersection-closed. We define the population error of E H positive examples as Lp+ (h) == PI(x,7)~D++ [h(z, r) NOj.
Let Ph (r( [h((z; r) NO and h" (2 = YES] be the probability that h' incorrectly rejects valid reasoning trace.
By construction, 1 7)) - YES only if all consistent E Hs output YES for (x, T). Since we assume by the realizability assumption that h² H, we have h Hs which is the of all verifiers consistent with the sample S. Therefore, if h'(2, T) = YES, then h (x, = YES as well. Or, h never accepts an invalid reasoning trace.
Thus, (hh) = Lp (h') Piz- But, by known results for PAC learning of intersection-closed classes [007 Dar15), m (VCCDiim(I)) + log 4)) training examples are sufficient to ensure Lp (h') S argued the proof of Theorem 4.9 we have 1/c S Lp+ (h'), which establishes the claimed sample complexity.
We have the following corollary for learning finite and intersection-closed verifier classes H. Corollary D.5. For finite intersection-closar H, Algorithm [ -)-PPAAC-lss H with sample complexity O (log([H)) + log 3))
E
Examples
Here we will see several examples to illustrate our verification model. We start with a simple interval- based toy example which shows that SVPAC and 7-TVPAC learning may be possible even when !/ and Σ are infinite.
Example E.1 (A toy example with interval verifiers). Let X Σ R. The verifier class consists of functions
H = (hrrrr (No, T (x.....,,..)) Mir S vo
xx))
Σ tj S r2] 1=1
ri, E R20.7 & r2)-
That is, all reasoning traces for which the sum of reasoning steps at some distance from Zo that is within an unknown interval [r1, r2] are valid. Notably, both Σ and H are infinite here. But VCDim(H) 2. For example, the training set consisting of the following reasoning traces
S {(0, (1)), (1, (3)), (2, (2, 3))}
cannot be labeled [YES,NO, YES} by any h E Н. This is because the distance of the trace sum from the problem To Σj= zy for the training points 1, and 3 respectively. So, any h
17

---

which labels (0, (1)) and (2, (2) as YES must also label (1, (3)) as YES. The finite VC dimension bound implies H is SVPAC learnable with sample complexity O ( log }) by Theorem 3.3 Our results in Section 4.1 for 1-complete and sound verification do not apply as |Σ] is not finite, but interestingly, the verifier class is still --TVPAC learnable (by Theorem D.4) with sample complexity O (: log since H is intersection-closee
The following example is a simple extension of the autoregressive linear thresholds studied as a family of Chain-of-Thoughe generators by [5]. Intuitively, for token space Σ = {0, 1). linear threshold w E _d looks at the last = min { |zr.
- bits of the text æ generated so far 2 O, where al :| denotes the last elements
and generates the next bit as 1[w; + w| :]][-[]]] - (coordinates or tokens) of a. Instead, here we use linear thresholds for verification of reasoning traces as described below. In this case, the binary classes induced by the linear thresholds more naturally correspond to the outcomes (YES, NO} of verification (while generation beyond binary tokens needs some extension).
Example E.2 (Linear threshold verifiers). Let X = R, Σ C R, |>] = 8. The verifier class consists of functions induced by d-dimensional linear thresholds
H wo : (Iu, T) + (1tlgt/100000 :|]--1 0| w E R wo E R,, = min (11,
Thus on a given problem and reasoning trace (x) the verifier applies a linear threshold to the
problem To and the last d - 1 reasoning steps (or all reasoning steps if |r| < <d- dd-1) 1). Note that // is
SVPAC learnable with sample complexity 0 (1 (d + log !)) by Theorem 3.3 Similarly, we get
sample complexity of O (? (dlog(k:sT)) + log })) for TVPAC learning using Theorem 4.5
We can use the discreteness of Σ to give a bound on the number of distinct functions in H. Indeed, there are |Σ| distinct values of (zo, T[ :)) that would determine the number of distinct behaviors
of any hw aro E H. By Sauer's lemma, we have T (8*) S
2ee" d+I
d+1
= O(()), This allows us to
use Theorem 4.4 to give a bound of O ( (d log(s) learning that independent of the length T of the trace.
+ log !)) on the sample complexity for TVPAC
As an example of a naturally discrete and finite setting, where the problems, the reasoning steps and the verifiers all come from finite sets, consider the following example.
Example E.3 (Valid reasonings on a graph). In this example, valid reasonings are paths in a graph, part of which is given by zo and part of which is implicit, defined by an unknown ground-truth verifier h" Formally, let G (V, E) denote the complete graph on n nodes. Let X V x 2 and Σ = E. The verifier class consists of functions
H = [he: (Io (vo, En), (x
(vo, vI),... T2 -:=--;;--1 (v;-1,
I[ 12g Eo UEN É E}
that verify whether each step (Iz-1. of the reasoning trace is valid, where a valid step is either an edge from En specified in the problem Zo. or in the (unknown) set of edges E* corresponding to h" = hg. Note that H is intersection-closed and |H| 2 2n(n 1)/2 The natural approach of building an estimate É of E* by collecting only the edges in the positively labeled traces in the training examples that are not already included in the problem up corresponds to the closure algorithm. Therefore, we have SVPAC, TVPAC and T-TVPAC learning with Ó(n² /t) sample complexity (using Theorem 3.2 Theorem 4.4 and Corollary (D.5).
The above example could be used to model discrete puzzle like the farmer-fos farmer-fox-chickee www.-ccccknncoorccc puzzle or the sliding tile puzzle. The vertices would correspond to the different discrete states of the puzzle. The final goal state is assumed to be fixed (for example, the sliding tiles make the desired picture), and the problem statement zn = (vo. 0), where Up is some initial state.
Since one of our main motivations is to learn good verifiers for Chain-of-Thhught Thought reasoning, for which Large Language Models (LLMs) have been proposed as good candidate generators, it is natural to try to understand our results for verification of natural language reasoning produced by these generators. In the following example, we suppose that we have finite collection of K verifiers which are also LLMs.
18

---

Example E,4 (Finite set of LLM verifiers). Let A denote the (finite) set of tokens in natural language. Let X Σ Aa. where R is the maximum number of tokens allowed a single problem statement or reasoning step. Let H be collection of K LLM verifiers. Under realizability, our results imply that the sample complexity of learning a verifier with small error is Ô log for
SVPAC and TVPAC learning, and Ô
K
for T-TVPAC learning (using Theorem 3.2 Theorem
[1-
and Theorem 4.9 respectively). We show sample complexity bounds without the realizability assumption in Appendix
We conclude this section with an example where it is possible to learn verifier online with a bounded number of mistakes.
Example E.5. The problem space is X = Rd that is, each problem 2o consists of a finite number of vectors in Rt Reasoning steps also vectors in E R. h" is also given by a set of vectors in R (unknown to the learner). For a given problem 2o, a reasoning step æ; is said to be valid if it lies in span(an, h"), the subspace spanned by the problem do and the hidden vectors h" and incorrect otherwise. The verifier is presented by a sequence of problem-reasoning pairs (1) ,z("),, (#0)
), (= _=(""),.. )...,,.. and gives assessment YES NO for each pair. The verifier is said (2)
to suffer a mistake if either it accepts a faulty reasoning 21 $ span(x0 (6) hh), or says NO for a valid reasoning o/ E span (5) hh)).
First, we make simplifying assumption that all problem vectors in any problem To lie in space orthogonal to span(h"). For this case, we will show online learner that is sound (i.e. never accepts
a faulty reasoning) and makes at most dim (span((n()"")) S mistakes. We initialize = O and
will maintain the invariant that span(h) is a subspace of span(hi). Given (x , (()), we accept
the reasoning if 21 lies in span(x))) h),, and reject otherwise. Our invariant span(h) (h) S span(h")
implies that we never accept an invalid reasoning. If make mistake on (x/0 21()), then
add the component of 21(") orthogonal to span(z)) h)) (i.e., 21 (i.e., - proj(zi) sppnnpaaaa (z) h)), where
proj(u, SS denotes the projection of vector v onto the subspace S) to h. This increases dim(span(h)) by and maintains our invariant span(h) S span(h"). Therefore, this algorithm makes at most dim(span(h))) I d mistakes.
Next, we show small mistake bound even when we remove the orthogonality assumption above. Any problem zo is given by finite collection of vectors in Rd as above, and assume that ht is given by a single vector in IRd, In this case, we will show a mistake bound of d 1, but will allow two-sided error (in the previous case, algorithm never resulted in false positives). Let S denote subspace maintained by the algorithm that has the invariant that it always contains At" Initialize S = IRd. Given a problem (xo, 21). first check if 21 span(2o), and return YES if so (which is always correct). Else, we return NO until the first mistake. At this point we set S = span(ap, x1). For any new instance (Zo, T1), we update S upon mistakes. We consider the following cases.
1. S Spann(To. F1).
a. S C span . In this case, h² E spon or span (Zo, h²) = span(ao). Thus, it suffices to output YES iff span(Zo). We do not make any mistakes in this case.
b. S* E span(To). In this case, we say YES. Since h² E S" S span(Zu, (7,)),),)). we can write h- = a.r. bō. If we made mistake, then Fa & span(To, (h), This implies b 0 and h" E span(z)). Thus, we can set 5 to S n span(x)). The dimension is reduced by at least one, since we assumed 5* & span
2. S" & span(To. FT). In this case, we say I[T; E span(Z)))- We don't make mistake when we say YES. If we made a mistake, then J. E span ht) and Fi & span(To). This implies T a.To + bh* with 3 0. Therefore, h² span(To, T Thus, we can safely update S* to S* n span Zi), and the dimension of 5* goes down by least
Thus, dSm(S*) goes down by every time we make a mistake except possibly for the first time, for a total mistake bound of d + 1.
19

---

F Beyond Realizability
The main focus of our work is the realizable case, where perfect ht lies in verifier class H which makes no mistakes on any problem-trane pair (i.e., accepts exactly the right reasoning traces for all problems in X). This property is particularly desirable for verification. However, it might be the case that our search space for verifiers is limited and no verifier in H perfectly verifies all the reasoning traces for all the problems of interest. This is known as the agnostic setting in PAC learning terminology, and the goal is to learn a verifier that has error almost as small as the verifier with the smallest error in H. Here use arguments from standard PAC learning theory to show sample complexity bounds for agnostic learning of verifiers. Note that the corresponding question for Chain-of- ofTohhghhhhtht generation was left open by prior work [JVB 25).
will formally define agnostic SVPAC and TVPAC learning and
F. Agnostic simple verifiers
The "label" for a problem-trae trace pair (To.T ( 22 ..,,,))))) is given by y (Ui,..., V1) E (YES, N Given y E (YES, NOJ" let fly) denote the smallest index E [?] such that yı NO (and f(y) if YES for all i). For a verifier h E H define its loss w.r.t. label y as
(x, = (Ii, TT): - (v1,...,77)) ))- = l[,(wo, (II,,.., z;)) + usl for some S f(y).
That is, we penalize the verifier for rejecting a trace while it is still correct according to the label y, or failing to reject at the first index that the label indicates as faulty (the rest of the label does not matter in this case). Formally, we have the following definition for agnostic learning.
Definition F1 (agnostic SVPAC-lcarabblitt), Let X denote the problem space and H S (YES, NO)XX3 denote the class of verifiers. Then a learner is said to be agnostic simply- verifiably-PAC learner for H with sample size m = ((, 6) (sample complexity is the small- est such m) if for any o, (0, 1), for any distribution D over X x Σ x {YES, NOJ" for h* E argmin z (.). -l (1r, Ti y)], given a sample S ~ D the learner outputs a verifier such that with probability least 1 over the draw of S.
B( 1 (wo, T, y) la- (No, T,y)] S..
The learner is said to be proper if h H.
We now show that it is possible agnostically SVPAC learn a verifier with small sample complexity for any finite class of verifiers H. A simple Hoeffding's 's bound based argument familiar from standard agnostic PAC learning implies that we can learn a good verifier with Ô ( log (i]) labeled problem-trace samples.
Theorem F.2. Any finite class verifiers H is agnostically SVPAC-leamable with sample complexity O 2 (log( + log )).
Proof. We use ERM, i.e. simply output any verifier h H that achieves the smallest total loss é, on the training sample and show that it achieves the stated sample complexity. Since the examples in the training sample S are iid draws from D, the loss a fixed h on the examples is an iid {0, 1 vvluud variable. By Hoeffding's bound,
Pr EollA(E,TTV))
Σ
(x(1)) (La(0,,00)))
(1)
2
< 2c -18--
[s]
2
By union bound,
Pr
3h E s.t. Ep (x
(, :(0g((0)
$ 2 H|e -11-
[
2
(z(1), (1) Jes
Applying this to ERM h and h², and noting that the enror of h S is no larger than that of h² implies that
E B( (2o, v, ly (.o.T,1) S E,
with failure probability 8 5 2|Hle -18/2
Solving for |S] gives the desired bound.
20

---

Since our proof for Theorem 3.3 involves bounding the relevant shattering coefficient, we can also readily adapt the proot of the fundamental theorem of PAC learning to establish Ó VCDim H) log T) bound on the sample complexity of agnostic SVPAC-learning for verifier classes H with finite VC dimension.
F.2 Agnostic trustable verifiers
We give a similar agnostic extension for TVPAC learning where the learner has access to a gold standard reasoner that provides to k correct reasoning traces for any problem æ E X, and when E finite. For a verifier h, we denote its population error as
errp(h): 1
Pr [h is 1-complete w.r.t. y and sound for sr.. 2nD
Let X denote the problem space and H S (YES,NO) NO) XxX" denote the class of verifiers. Let g(x) C Σ denote the set of correct reasoning traces for any X. Then a learner is said to be agnostic trustably-eerfiably-PA. learner for H with sample size m = (e, d) (sample complexity the smallest such m) for any 6, E (0, 1), for any distribution D over X, for h" E argmin ee (t) and OPT = err er")(h"), given sample ~ D and for each æ E S given access to the set g(z), the learner outputs a verifier h such that with probability at least 6 over the draw of S, errp(h) OPT + e. The learner is said to be proper if E H.
Definition E3 (agnostic TVPAC-
We show that ERM the samples constructed using the gold standard reasoner in Section 4.1 is an agnostic SVPAC learner with small sample complexity for any finite class of verifiers H. The argument similar that of Theorem F2
Theorem F4. Any finite class of verifiers H is agnostically TVPAC-learnable with sample complexity O ( (log() H + log )))
Proof. The key observation is that our training sample S = (xx(1, gzx()))) allows to determine I[h is 1-complete w.r.t g and sound for z] for any problem in the sample, by using the tree T, (x) and finiteness Σ. This gives us the 0-1 loss of h on æ which can be used to implement the ERM, and we can apply the same argument in the proof of Theorem F2 for this loss conclude the proof.
As before, we can use the bound on the shattering coefficient our proof of Theorem 4.5 and adapt the proof of the fundamental theorem of PAC learning to establish a Ö VCDim H) log { bound on the sample complexity of agnostic TVPAC-learning for verifier classes H with a finite VC dimension.
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:
The claims accurately reflect prior work and contributions of this work.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made in the paper.
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.
21

---

It is fine to include aspirational goals as motivation as long as it is 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:
All limitations have been discussed in context.
Guidelines:
The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those not discussed in the paper.
The authors are encouraged to create a separate "Limitations" section in their paper.
The paper should point any strong assumptions and how robust the results these assumptions (e.g., independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.
violations of
The authors should reflect the scope of the claims made, e.g., if the approach only tested on a few datasets or with a 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 approach. 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 to provide closed captions for online lectures because it fails 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 address problems of privacy and faimess.
While the authors might fear that complete honesty about limitations might be used by reviewers grounds for rejection, worse outcome might be that reviewers discover limitations that aren't I acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an important role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory assumptions and proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
Answer: [Yes]
Justification: Full proofs are included and assumptions are clearly stated.
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 cross-eeference..
All assumptions should be clearly stated or referenced in the statement of any theorems.
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 to provide short proof sketch to provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
22

---

4. Experimental result reproducibility
Question: Does the paper fully disclose all the information needed to reproduce the main experi- mental results of the paper to the extent that it affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Answer: [NA]
Justification:
The main contribution theoretical.
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 dataset and/or model, the authors should describe the steps taken make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is novel architecture, describing the architecture fully might suffice, the contribution is specific model and empirical evaluation, it may be necessary to either make it possible for others to replicate the model with the same dataset, or provide access to the model. general. releasing code and data often one good way to accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to hosted model (e.g., in the case of large language model), releasing of model checkpoint, or other means that are appropriate to the research performed.
While NeurIPS does not require releasing code, the conference does require all submissions 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 clear how to reproduce that algorithm.
(b) If the contribution is primarily a new model architecture, the paper should describe the architecture clearly and fully.
(c) If the contribution 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 reproduce the model (e.g.. with an open-source dataset or instructions how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors 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 to have some path to 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 instructions to faithfully reproduce the main experimental results, as described supplemental material?
Answer: [NA]
Justification:
The main contribution theoretical.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurIPS code and data submission guidelines (httpp://nips.cc/ppnn for more details.
While we encourage the release of code and data, we understand that this might not be possible, so "No" is an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (c.g., for a new open-source benchmark).
23

---

The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurIPS code and data submission guidelines httpps///iiis.cc/pubbbpe guides/Codeeuumi es onyllicy) for more details.
The authors should provide instructions on data access and preparation, including how 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 a subset of experiments are 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 much information as possible in supplemental material (appended to the paper) is recommended, but including URLs data and code is permitted.
6. Experimental setting/details
Question: Does the paper specify all the training and details (e.g., data splits, hyperparameters. how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [NA]
Justification:
The main contribution is theoretical.
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should presented in the core of the paper to level 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
Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Answer: [NA]
Justification:
The main contribution is theoretical.
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, confidence 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, or overall run with given experimental conditions).
The method for calculating the error bars should explained (closed form formula, call to library function, bootstrap, etc.)
The assumptions made should be given (e.g., Normally distributed errors).
It should be clear whether the error bar is the standard deviation or the standard enror of the mean.
is OK to report I-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have a 96% CI. if the hypothesis 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 (c.g. negative error rates).

---

If eπror bars are reported in tables plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables the text.
8. Experiments compute resources
Question: For each experiment, does the paper provide sufficient information the computer resources (type of compute workers, memory, time of execution) needed to reproduce the experi- ments?
Answer: [NA]
Justification:
The main contribution theoretical.
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU or 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 well as estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't make into the paper).
Code of ethics
Question:
Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics huttps:/neurre httphhwwwwp....pppppppppeecp Btt//Ehhhhhhtte
Answer: [Yes]
Justification:
We reviewed the NeurIPS Code of Ethics.
Guidelines:
The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics.
If the authors answer No, they should explain the special circumstances that require a deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g., if there is a special consideration due to laws or regulations in their jurisdiction).
10. Broader impacts
Question: Does the paper discuss both potential positive socictal impacts and negative societal impacts of the work performed?
Answer: [NA]
Justification: Theoretical work with no direct societal impact.
Guidelines:
The answer NA means that there is 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 or unintended uses (e.g.. disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deploy- ment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point 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
25

---

other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people train models that generate Deepfakes faster.
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 or unintentional) misuse of the technology.
If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses addition to attacks, mechanisms for moni- toring 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 or models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification:
The main contribution theoretical.
Guidelines:
The answer NA means that the paper poses no such risks.
Released models that have high risk for misuse dual-use should be released with necessary safeguards to allow for controlled use the model, for example by requiring that users adhere to usage guidelines restrictions access the model 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 is challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Question: Are the creators original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms use explicitly mentioned and properly respected?
Answer: [NA]
Justification:
The main contribution theoretical.
Guidelines:
The answer NA means that the paper does not use existing assets.
The authors should cite the original paper that produced the code package or dataset.
The authors should state which version of the asset is used and, if possible, include a URL.
The name of the license (c.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 service of that source should be provided.
If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, papprswittttie www.whthhod...o com/ datasets has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if has changed) should be provided.
If this information is not available online, the authors are encouraged to reach out to the asset's creators.
13. New assets
26

---

Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [NA]
Justification:
No new assets.
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details the dataset/code/mmoel as part of their sub- missions 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 is used.
At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsourcing and research with human subjects
Question: For crowdsoureing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well as details about compensation (if any)?
Answer: [NA]
Justification: No crowdsourcing.
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 contribution of the paper involves human subjects, then much detail as possible should be included in the main paper.
According to the NeurlPS Code of Ethics, workers involved data collection, curation, or other labor should be paid at least the minimum wage in 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 equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification:
No study over human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Depending on the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurIPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applica- ble), such as the institution conducting the review.
16. Declaration of LLM usage
27

---

Question:
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, or originality of the research, declaration is not required.
Answer: [NA]
Justification: LLM does not impact the core methodology, scientific rigorousness, originality of the research.
Guidelines:
The answer NA means that the core method development in this research does not involve LLMSs any important, original, or non-standard components.
Please refer our LLM policy httpp:///oorrreccccc///arrrreeee for what should or should not be described.
28


Reviews:
[{"review_id": "5XwGAhFSS1", "reviewer": "Reviewer_ANSN", "summary": "This paper studies the sample complexity of learning verifiers for CoT reasoning in LLMs. The presented formulation of PAC learning on two types of problems, learning a weak verifier and a strong verifier, shows the paper's assumptions and derivation of the bounds.", "questions": "Could you revisit two cases in this paper, the weak and the strong verifiers, and explain how the assumption fits the CoT reasoning in LLMs?\nFor example, we could imagine verifying a reasoning step in a common math reasoning problem. \nIt seems decomposing a CoT thought into steps is not an obvious task, but assuming that the step is given well, what would the dataset D and the problem set S look like? According to the paper, the reasoning steps are sampled from the entire dataset, and some steps are correct while others are incorrect. Does it imply that the steps can be applied to multiple problems and they can still be correct? \nThe method also assumes that the labels for the correctness of each step are available. The strong verifier has access to the gold standard reasoner. What would be a rough estimate for |H| in terms of the size of the dataset and the number of steps?", "limitations": "YES", "rating": 3, "confidence": 2, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 2, "significance": 2, "originality": 3, "strengths_and_weaknesses": "**Strength**\nThe formalization of the learning verifier for LLM reasoning.\nThis paper will provide a good theoretical basis for learning verifiers.\n\n**Weakness**\nThere's no discussion on the validity of the assumptions made. \nThe result is bound, and it avoids being grounded in concrete situations.\nIt is not apparent whether the assumptions made in this paper apply to CoT reasoning in LLMs.", "was_revised": true, "final_justification": "From the rebuttal, I think this paper is a fancy theory paper that provides the bounds and sample complexity results in statistical learning theory. I am not an expert in theory, so this would be a good paper.\n\nOne thing that I wish to clarify was the connection to the actual situations by using concrete examples like GSM8K. However, I couldn't find any strong connection to the real use case. I felt some detachment between the theory and practice.\n\nI will keep the current score.", "rebuttal": "We thank the reviewer for their time spent reading our paper and we address their various questions and concerns below. In particular, we provide simplified discussions of our models (which we are happy to add to the paper) and also point out that we do have concrete examples illustrating our theoretical results in the supplement which the reviewer might have missed.\n\n\n**Concrete examples**: We have included some simple examples in the main body (Section 2, lines 322-325) and also provide several detailed concrete examples for instantiating our theoretical results in Appendix C (Examples C.1 to C.5) in the “Supplementary Material” due to space constraints. We are happy to take the reviewer’s feedback into account and move more examples into the main body in the final version.\n\n\n**Connection to CoT (Chain-of-Thought)**: The decomposition of the reasoning into steps has been previously studied in the literature on CoT generation e.g. Joshi et al. (COLT 2025), Malach (ICML 2024), so it is natural to study it for CoT verification as well. We illustrate below our weak and strong verification goals in the context of CoT reasoning for solving math problems.\n\n\n*Weak (simple) verifiers*. Each problem statement here will be some math problem. The distribution (and unlabeled sample from it) would correspond to problems coming from some domain (e.g. high school, graduate course, international mathematics olympiad, etc.) along with step-wise solutions generated by a CoT LLM reasoner. A labeled dataset will be annotated with verifications of these solutions, either marked correct or the first incorrect step is indicated (this could be done by a human labeler). A learned verifier (potentially another LLM) will use this dataset to learn how to verify unseen (problem+solution) pairs from the same distribution (e.g. more problems from the same domain solved by the same CoT reasoner).\n\n*Strong (trustable) verifiers*. Each problem statement is again (say) some math problem. The distribution (or unlabeled sample) here would correspond to problems coming from some domain (e.g. grad course, olympiad, etc.), but without any solutions. In a labeled dataset, each problem will be annotated with either a small number of correct “gold standard” solutions (say solution key by the problem setter, Section 4.1), or one random correct solution (possibly auto-generated but known to be correct, Section 4.2). A learned verifier (potentially another LLM) will use this dataset to learn how to verify unseen (problem+solution) pairs, with the problems coming from the same distribution but the solutions could be generated by *any* CoT reasoner (LLM in the wild, student-written proof, etc.)\n\nWe will be happy to update our title to “On learning verifiers for *stepwise* reasoning” to reflect the generality of our work beyond the reasoning pattern generated by Large Language Models (even though it is currently the most relevant reason to study this).\n\n\n*“According to the paper, the reasoning steps are sampled from the entire dataset, and some steps are correct while others are incorrect. Does it imply that the steps can be applied to multiple problems and they can still be correct?”*\n\n\nWe would like to clarify that as explained above, we either sample (problems+reasoning steps pairs) in the simple model; or only the problems in the stronger model (where reasoning steps can be arbitrary). We focus on the realizable setting where the correctness is given by an unknown verifier $h^{\\ast}$ and depends not only on the current step but also the problem statement and the sequence of steps so far (recall verifiers in $H$ are functions from $X\\times\\Sigma^\\ast\\rightarrow \\{\\text{YES, NO}\\}$). We go beyond the realizable setting in Appendix D where we study the sample complexity of agnostic learning of verifiers.\n\n\n*“What would be a rough estimate for |H| in terms of the size of the dataset and the number of steps?”*\n\n\nNote that we establish upper and lower bounds on the sample complexity i.e. the size of the dataset need to learn a verifier class H in terms of the size |H| of the verifier class (or VC dimension if H is infinite) and the number of reasoning steps T (in cases it impacts sample complexity). This size is logarithmic or linear in |H| depending on the strength of the verification goal and properties of H. For example, if H is intersection-closed, then all our verification goals can be achieved using dataset that is logarithmic in |H|. \n\n\nIn terms of a rough estimate for |H|, this would depend on the application; for example, if we are considering verifiers that can be created by fine-tuning a given initial suboptimal verifier, then |H| would be the number of ways this initial verifier could be fine-tuned (say, number of possible weights in the final layer)."}, {"review_id": "2N37exokBE", "reviewer": "Reviewer_9kqw", "summary": "The paper tackles the problem of learning a verifier that can check whether a given sentence in natural language is correct in the sense that the reasoning steps it takes are correct according to the distribution used to learn the verifier. The problem is formulated in a PAC setting making the verification thereby probabilistic.", "questions": "1) It is not very clear what you mean by chain-of-thought. Because when you introduce chain-of-though you cite the papers that introduced chain of thought prompting. However, none of prompting plays any role in any of the proofs. Could you clarify this?\n\n2) Could you comment on my (possible wrong observation) that your proofs have nothing to do with chain of though (prompting)?\n\n3) Could you comment on the availability of actual data to train such a verifier. For the different scenarios, i.e. for the different flavors of verifiers.", "limitations": "yes", "rating": 4, "confidence": 2, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 1, "significance": 2, "originality": 3, "strengths_and_weaknesses": "The title of the paper is \"on learning verifiers for chain-of-thought reasoning\". However, it seems that nowhere in the proofs chain-of-thought is actually used as an assumption. If I understand things correctly, is that we have a data set with a sequence of symbols, we then learn a verifier on this set of sequences. After having learned the verifier we check whether a new sequence is from the same distribution as that of the dataset. This happens in Section 3. The remainder of the paper are then variations of this idea.\n\nTo me it seems that this has, on a theoretical basis, nothing to do with chain-of-thought reasoning. One could argue that verifying that a sequence of symbols produces by a transformer-based LLM (or any other autoregressive model for that matter) is an application of this sequence PAC learning approach.\n\nAn other problem I have is that the paper makes many assumption on availability of data and how the data is given. For instance, the data is assumed to be given on an almost sub-sentence level. This seems like a rather strong assumption. Also, in case that chain-of-thought plays indeed a role in the proposed method (contrary to what I understand) then this would also mess up certain things, as the LLM is seeing only tokens and not these sub-sentence entities.", "was_revised": true, "final_justification": "The authors have proposed to change the framing of the paper by moving away from \"chain of thought reasoning\" and focusing more on learning verifiers of sequences. Of course with the use LLMs as sequence models for language as a main application.\n\nI also appreciate the authors addressing my concern regarding availability of data and grounding their claim in the literature.\n\nI am increasing my score to a \"borderline accept\".", "rebuttal": "We thank the reviewer for their time and address their concerns below.\n\n\n**Clarification of “chain-of-thought” terminology**: You are right that our usage of chain-of-thought is different from that in the original paper, where it is used primarily as a prompting technique. We use CoT to refer to the standard generation pattern of reasoning models like o3, Deepseek R1, i.e., the model generates the ordered list of intermediate reasoning steps $(s_{1},\\dots ,s_{T})$ before its final answer.\n\nOur use of the terminology chain-of-thought is consistent with prior theoretical work e.g. Joshi et al. (COLT 2025), Malach (ICML 2024) which studies chain-of-thought generation (in contrast, we study verification of the reasoning produced by such models). Suppose the language model is given some input question, and it produces an output consisting of intermediate steps (we discuss these steps below in response to your other question) before arriving at the final answer. This behavior may be due to the nature of training data with such chain-of-thought sequences as studied in the prior works mentioned above, or because the language model was prompted to “think step by step”. This nature could also be elicited or amplified by the use of reinforcement learning. As with these theoretical papers on chain-of-thought generation, the study of how to do the chain-of-thought “prompting” itself (which is more related to the ability of the language-model to do in-context learning) is beyond the scope of our work, the applied works we cite indicate challenges with this approach and motivate the need for verification. \n\n\nWe will add the above discussion to our paper to clarify the exact sense in which we study chain-of-thought. We will also update our title to “On learning verifiers for *stepwise* reasoning” to reflect the generality of our work beyond the reasoning pattern generated by Large Language Models (even though it is currently the most relevant reason to study this).\n\n\n\n\n**Clarification related to data format**: We describe below the format of training data for the different verification goals studied in our paper.\n\n1. Simple verification (SVPAC). Here the training data consists of problem statement and reasoning-sequence pairs. This could be generated for example by asking an LLM to solve some randomly drawn problems while “showing its reasoning”. This is similar to the training data for chain-of-thought generation studied in prior theoretical works [Joshi et al. (COLT 2025), Malach (ICML 2024)]. For learning a verifier, we assume these are annotated as either correct or with the first incorrect reasoning step.\n\n2. Trustable verification (TVPAC). Here our training set consists of problem statements along with a small number of “gold standard reasoning” steps that solve each problem. For example, this could be a set of homework problems in a graduate course and the solutions provided by the instructor. The goal of the verifier is to verify whether the reasoning matches one of the standard solutions (even in unseen problems and reasoning sequences), and work correctly (only accept correct proofs) for most typical problems.\n\n3. A stronger trustable verification model ($\\gamma$-TVPAC). Here our training set consists of problem statements along with one correct sequence of reasoning steps that solves each problem. The goal of the verifier is to verify whether the reasoning is correct (even in unseen problems and reasoning sequences), for most typical problems. Our verifier is sound (never accepts a wrong reasoning) and almost complete (accepts nearly all typical correct reasonings).\n\n\n*“ the data is assumed to be given on an almost sub-sentence level… LLM is seeing only tokens and not these sub-sentence entities.”*\n\nOur theory does not make any particular assumption on the data (only that the reasoning steps come from some set $\\Sigma$ which could be anything). The use of an abstract set $\\Sigma$ to denote the reasoning steps is consistent with prior theoretical work on chain-of-thought. A natural setting for verification however would be to think of $\\Sigma$ as consisting of a reasoning step in natural language. Note that we are learning verifiers here, so even if the LLM that generated the chain-of-thought does next-token prediction, we may ask it to separate its reasoning into “steps” that can be individually verified by the verifier."}, {"review_id": "N3I5r9LiEU", "reviewer": "Reviewer_oW28", "summary": "This is a theoretical paper that analyzes verifiers' computational complexity. It mostly concerns the standard bounds using the Vapnik-Vitanyi framework for PAC theory; the novelty is in considering the soundness and completeness of a verifier. The natural application is to validate CoT reasoning in LRM. One important conclusion is given for strong completeness (learning verifiers accepting all correct reasoning and refusing all incorrect ones). Without Oracle, the sample grows prohibitively with the reasoning alphabet size and (maximum) trace length. Key insight is that, under normal conditions, learning robust and trustworthy (trustable) CoT verifiers is fundamentally constrained.", "questions": "1. Given the impossibility of an effective CoT verifier with sufficiently many traces, what implication would one expect for trustable/trustworthy verifiers? Perhaps, you can elaborate on this in the paper.\n2. Given the impossibility of a sound and complete verifier in an infinite space, what feasible recommendations can be provided for designing a robust LRM? The recommendation can point to problems and closed systems where  CoT is proven efficient and/or practical (e.g., problem solving for Euclidean geometry, medium-complexity math problems, code generation (with limited verification), etc.\n3. An interesting research question is how to describe domains admitting a trusted verifier that almost surely gives a correct answer to a new question.", "limitations": "N/A", "rating": 5, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 4, "significance": 3, "originality": 4, "strengths_and_weaknesses": "Originality. \nA useful view of the problem is simple verifiers vs. trustable verification within a formal framework. Moreover, this paper establishes the complexity boundaries for these cases.   \nThe approach associating the completeness and soundness of a classifier/verifier with its complexity is original. However, the terminology may be a little bit confusing in this context since it clashes with the well-known and established notions from standard logic.  One can feasibly talk about classifiers and verifiers within their domain's first-order logic. The completeness and soundness would mean something else. \n\nSignificance. \nThe bounds and key limitations are significant and correlate with recent results in automated proving. The results provide an additional view and framework for tracing the complexity of CoT verifiers. This, in turn, generates some interesting research questions for this key area of LRM (the authors posed some implicitly).\nThe reasoning alphabet for the CoT scenario is infinite since there is proof of any length in the space. We cannot generalize the results of this paper to this case. And for trustable verification, validating almost surely requires samples of unbounded complexity (due to no free lunch, and other classic considerations).\nHowever, it is easy to see examples of the TVPAC classifiers with infinite VC-dimension (if we relax the PAC requirement for TVPAC). Check one that solves the problem, whether a randomly selected number is transcendental.   Almost surely, classifying it, in all cases, would constitute a PVAC classifier regardless of sampling size. \n \nIs it possible to get close to that kind of behavior for the PAC case, i.e., for the classifier with finite VC dimension depending on overall complexity?\nLimitations of the framework: The authors claim, \"All limitations have been discussed in context\". They are among the key results. Thus, the limitations are properly addressed.", "was_revised": true, "final_justification": "Recommended score: 5 (accept). The issues raised by reviewers have been resolved, in my opinion. \n\nThe paper opens up a promising direction in understanding the limitations of LRM reasoning, with the author's rebuttal on the mathematical context and the Math benchmark GSM8K. \n\nThe natural next step for further theoretical and experimental research is benchmarking for novel problems (cf. Benchmarking LLMs on Advanced Mathematical Reasoning, the Berkeley report No. UCB/EECS-2025-121 by J. Yue and D. Klein), and FrontierMath (Glazer et al., 2024). Of particular interest are benchmarks based upon the formal languages (Lean) because they provide a verifier with an opportunity to self-check the validity of each step in CoT. \n\nThat leads to a trustworthy (trustable) verification. The paper establishes a bound for sample complexity when the number of correct samples $\\textit{k}$ is small: loosely, a function of $\\Omega(log|\\Sigma|)$, while for large $\\textit{k}$, verification requires $\\Omega(|H|)$ samples ($H$ is a hypothesis class, and $\\Sigma$ is the set of reasoning steps). These are important practical limitations for the scalability of trustable verification.", "rebuttal": "We thank the reviewer for their time and their appreciation of our contributions.\n\n\n\n*“One can feasibly talk about classifiers and verifiers within their domain's first-order logic.”*\n\nThis is a great point. While we clearly distinguish our work from formal verification in the introduction and related work (we learn verifiers for natural language instead of formal language), we will make sure to clarify the differences in our terminology by adding the following remark near our definitions of soundness/completeness. \n \nWe note that soundness and completeness of proof systems is a terminology also used in formal verification and logic, and caution the reader from conflating them with our notions.  A soundness guarantee for a deductive system expresses that all provable sentences are true. Completeness states that all true sentences are provable. While there is an analogy, we remind the reader that our study applies to natural language reasoning while formal logic involves proofs expressed in a very precise formal language and their verification.\n\n\n*“Given the impossibility of an effective CoT verifier with sufficiently many traces, what implication would one expect for trustable/trustworthy verifiers”*\n\n\nOur impossibility results (in our strongest verification model of $\\gamma$-TVPAC learning) set up a situation where there are many different “types” of proof (think of each $S_i$ in our proof as a different proof type), some of which are legitimate and some of which are not, and where seeing some legitimate types gives no information about which are not.  So our results suggest that situations of this kind may require a large amount of training data.   \n\n\nOur theory suggests another way around in the absence of large amounts of data. One may relax the verification goals to a trustable verifier that is sound, but only complete with respect to a small set of gold standard reasoners (Section 4.1) where the sample complexity upper bounds are more reasonable.\n\n\n\n\n*“Given the impossibility of a sound and complete verifier in an infinite space, what feasible recommendations can be provided for designing a robust LRM?”*\n\nThis is an interesting question. We remark (lines 318-325) that one way to overcome our impossibility results (Theorems 4.8, 4.9) for building a trustable verifier is to restrict the domain to intersection-closed verifier classes (which may be infinite). An interesting example is noted in Appendix C (Example C.3) where this intersection-closed property holds — here we use a graph-based construction to model discrete puzzles (e.g. the farmer-fox-chicken-corn puzzle or the sliding tiles puzzle) where nodes of the graph can denote different states of the puzzle.\n\nBut this is only one example of a sufficient condition for infinite classes and one example of a domain where sound and complete verification is possible. An interesting direction for future research (as you note) is to characterize exactly when trustable verification is possible (necessary and sufficient conditions).\n\n\n\n\n*“An interesting research question is how to describe domains admitting a trusted verifier that almost surely gives a correct answer to a new question.”*\n\n\nWe agree with the reviewer that this is a very interesting question for future research."}, {"review_id": "8k5w9owGrv", "reviewer": "Reviewer_1Yc9", "summary": "The authors present a series of analyses and theoretical results on the PAC-learnability of correct verifiers for step-by-step sequential reasoning, a process that has become increasingly popular in the application of LLMs. The authors' key results show that you can PAC-learn a consistent in-disttribution (with respect to some known prior) verifier with a log-bounded sample complexity, and present trustable verifiers where accepted proofs must come from a known and fully correct line of reasoning. These trustable verifiers, while more challenging to PAC-learn, do have a lower bound on sample complexity if the number of gold standard proofs is small.", "questions": "Questions:\n* is there not a relationship between this work and LLMs that use interactive theorem provers that also ensure the soundness and correctness of intermediate steps? can the authors comment on what their work can do that others, such as LeanDojo?\n* Line 158: Can you comment on what distributional assumptions we can reasonably make when actually dealing with certain classes of LLM-guided reasoning problems? is there other work on such analysis?\n* How reasonable is the gold-standard assumption in lines 163-164? how does this affect the tractability of the overall approach? More concretely, in what kinds of problem settings do we expect this assumption to be valid and when do we not?\n* line 186: does a satisfactory learner exist for all values of $\\eta$ greater than zero? does $\\eta$ exist for sample efficiency reasons or is it a necessary assumption?\n* Line 190: why do we make this assumption?", "limitations": "The assumptions necessary for the theory to hold are generally laid out but lack a bit of detail regarding their relative strength in the main text.", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 2, "significance": 2, "originality": 3, "strengths_and_weaknesses": "Strengths:\n\n* Achieving PAC-bounds and formal guarantees on the correctness and achievability of reasoning is a very very valuable problem to look at and a nice step forward from an algorithmic perspective.\n* The formulation of the problem setting is done in a rather understandable way and the key results are accompanied by intuition and explanation to ground the reader. It’s a nice and approachable way to write a theory paper for the ML community.\n* The results and commentary on the results do provide some interesting insights towards LLM-guided sequential reasoning. In particular, I found Theorem 4.4 and Theorem 4.8 particularly compelling in terms of their implications for how easy it will be to learn verifiers for LLMs at scale.\n* The writing in section 4 (the bulk of the paper) is fairly easy to follow. The theoretical results are compelling despite the assumptions made.\n\nWeaknesses:\n\n* The writing in the introduction, in my opinion, doesn’t do a good enough job of making the problem statement, motivation, and overall contribution clear. Paragraph 1 is light on detail and doesn’t make the scope immediately clear or tight. Later on in the introduction, it is also unclear what the exact contribution of the work is (paragraph 4, line 39.) if there are many correct reasoning traces starting from x0 why not accept all of them? what exactly is the difference between a ‘gold standard’ correct reasoning trace and some other correct reasoning trace? These questions are answered in section 4 but there needs to be a more rigorous explanation of the key results in the introduction to properly ground the reader.\n* The related work section feels rather light - there has been a huge amount of effort in auto formalization, formal reasoning with LLMs, verification of LLMs both in a formal methods-y and not formal methods-y sense, and so forth. The authors would be well suited to make a more substantial effort in contextualizing their work in the large amount of recent work to better situate their contribution.\n* It’s broadly unclear to me how this work is specific in any capacity to LLMs, besides the fact that LLMs are being used to generate step-by-step reasoning based proofs and the work applies to this problem setting. The actual usage of LLMs doesn’t actually appear in the paper whatsoever and it begs questions of relevance towards its claimed application. That is not to say that the theoretical contributions aren’t of interest to the community in general - they certainly are, but the paper is written with the central motivation coming from LLM applications. The paper doesn’t however actually apply the theory to LLMs at all. So either the framing of the story ought to change or there need to be results that actually demonstrate the efficacy and reasonableness of the theory by applying it to LLM-guided formal reasoning.\n* A number of assumptions are made throughout the paper to facilitate the theory. This is fine in a nutshell, but there is little to no commentary on (1) why these assumptions are made in the context of the theory, or (2) whether or not these assumptions are reasonable when actually performing LLM-guided formal reasoning. I’ve asked about some of them in my questions.\n\n    * Line 240 provides an interesting insight but is not immediately followable from the preceding theory.\n\nOverall I think the paper presents a nice contribution but the writing and framing of the story causes consternation on my end. I will recommend acceptance but would suggest the authors reframe the story a bit to match their contribution.", "was_revised": true, "final_justification": "My score was predicated on the changes that were promised by the authors in the rebuttal; as such, I will maintain my score.", "rebuttal": "We thank the reviewer for their detailed review. We also appreciate their comments that our paper is approachable, and that our results provide compelling insights for a valuable problem. We provide our response to the reviewer’s comments and questions below.\n\n\nWe propose the following updates to improve our writing based on the suggestions in the review.\n\n**Introduction**. We propose to add the following list of contributions to make our problem statement and overall contribution clear.\n \n• We introduce a formal framework for studying verifiers for Chain of Thought reasoning. Given any problem statement and a sequence of reasoning steps for the problem, we propose the problem of learning verifiers that examine the steps for correctness, and for an incorrect reasoning trace return the first faulty step in the reasoning.\n\n• We formally define simple verifiers which have access to random Chain of Thought reasoning sequences labeled as “correct” or “incorrect” along with the first faulty step. We establish sample complexity bounds for learning good simple verifiers in a PAC sense for verifier classes that are finite or have a finite VC dimension.\n\n• We next introduce the more powerful trustable verifiers, that only have access to random problems and a gold standard reasoner that provides a small number of guaranteed correct reasoning traces for each sampled problem. We establish PAC learnability of designing verifiers that accept all the gold standard reasoning traces on most problems and never accept faulty reasoning traces, provided the space of reasoning steps is finite.\n\n• Finally, we extend our trustable verification goal to the case where there may be a large number of gold standard reasoning traces, but only a random correct trace is available to the learner. We establish upper and lower bounds on the sample complexity of learning a verifier that is always sound (i.e., never accepts an incorrect trace) and accepts most of the gold standard traces on most problems.\n\n\n**Related Work**. We will significantly expand on our related work section to discuss more key works related to chain-of-thought generation and verification. This would include theoretical works that study verifier-assisted generation e.g. Amit et al. (2024), Botta et al. (2025), as well as more applied works e.g. Nakano et al. (2021), Hao et al. (2023), etc.\n\n**Overall framing**.  We will be happy to change the title to something like “On learning verifiers for stepwise reasoning” to reflect the generality of our work beyond chain-of-thought reasoning by Large Language Models (even though it is currently the most relevant reason to study this).\n\n**Discussion of assumptions and implications**. Our assumptions mainly correspond to different verification goals that one might have.\n\n1. Simple verification (SVPAC). Here the training data consists of problem statement and reasoning-sequence pairs. This could be generated for example by asking an LLM to solve some randomly drawn problems while “showing its reasoning”. This is similar to the training data for chain-of-thought generation studied in prior theoretical works [Joshi et al. (COLT 2025), Malach (ICML 2024)]. For learning a verifier, we assume these are annotated as either correct or with the first incorrect reasoning step.\n\n2. Trustable verification (TVPAC). Here our training set consists of problem statements along with a small number of “gold standard reasoning” steps that solve each problem. For example, this could be a set of homework problems in a graduate course and the solutions provided by the instructor. The goal of the verifier is to verify whether the reasoning matches one of the standard solutions (even in unseen problems and reasoning sequences), and work correctly (only accept correct proofs) for most typical problems.\n\n3. A stronger trustable verification model ($\\gamma$-TVPAC). Here our training set consists of problem statements along with one correct sequence of reasoning steps that solves each problem. The goal of the verifier is to verify whether the reasoning is correct (even in unseen problems and reasoning sequences), for most typical problems. Our verifier is sound (never accepts a wrong reasoning) and almost complete (accepts nearly all typical correct reasonings).\n\n\n\n\n**Relation with other works that use \"interactive theorem provers\"**: Theoretical work on using interactive theorem provers e.g. Amit et al. (2024) assume a sound and complete verifier as given, and show how the reasoning generator can use this verifier to improve their correctness. In contrast, we study how to actually learn these verifiers from data. \n\nLeanDojo extracts proofs in the functional programming language Lean into datasets for training machine learning models. It also enables the trained model to prove theorems by interacting with Lean's proof environment. Note that the “verifier” in this interaction is the Lean proof system, which only accepts formal language and prior applied work (e.g. Yang et al., NeurIPS 2023) has tried to use language models to write proofs in the Lean system (while they also generate natural language descriptions of their proof steps, the evaluation is through correctness of the lean proof). In contrast, our work studies the learnability of verifiers that potentially evaluate natural language reasoning directly. \n\n\n**On distributional assumptions [Line 158]**\n\nIn our trustable verification model, we only assume that the problem statements are coming from some distribution but the reasoning traces that we verify may be arbitrary (and out-of-distribution with respect to the training set). This roughly corresponds to building verifiers that are trustable for problems coming from a specific application domain (e.g. solving math problems or logic puzzles), in the sense that they are sound and (nearly) complete.\n\n\n**On gold standard assumption [Line 163-164]**\n*“Line 190: why do we make this assumption?”* [the number of gold standard reasonings is small]\n\nDiscrete puzzles like the farmer-fox-chicken-corn puzzle may have one or a small number of correct solutions. Another example is a set of homework problems in a graduate course and the gold standard solutions provided by the instructor. Verifying all (potentially out-of-distribution) proofs for unseen problems and proofs from a given domain is a more challenging goal than simple verification (Section 3), but under the gold standard verification goal we only aim for completeness with respect to the gold standard proofs (but still always sound).\n\n[Line 190] The main reason for assuming the number $k$ of gold standard reasonings to be small is for computational efficiency (linear in $k$) and sample efficiency (logarithmic in $k$) of learning verifiers. \n\nWe further relax this assumption in our strongest verification goal of $\\gamma$-TVPAC learning (Section 4.2), but have stronger impossibility results for this goal (Theorems 4.8, 4.9). So the gold standard assumption is a nice intermediate setting, where we can get robust verification with small sample complexity.\n\n\n*“line 186: does a satisfactory learner exist for all values of η greater than zero? does η  exist for sample efficiency reasons or is it a necessary assumption?”*\n\nYes, there is a learner for each value of $\\eta$ greater than zero (the sample complexity upper bound depends on $\\eta$) and our sample efficiency depends inversely on $\\eta$ (Theorem 4.7). Perfect completeness ($\\eta = 0$) is achieved under the gold standard assumption (Theorems 4.3, 4.4).\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n**References**\n\n\n[1] Amit, Noga, Shafi Goldwasser, Orr Paradise, and Guy N. Rothblum. \"Models That Prove Their Own Correctness.\" In ICML 2024 Workshop on Theoretical Foundations of Foundation Models.  \n[2] Botta, Edoardo, Yuchen Li, Aashay Mehta, Jordan T. Ash, Cyril Zhang, and Andrej Risteski. \"On the Query Complexity of Verifier-Assisted Language Generation.\" In Forty-second International Conference on Machine Learning 2025.  \n[3] Hao, Shibo, Yi Gu, Haodi Ma, Joshua Jiahua Hong, Zhen Wang, Daisy Zhe Wang, and Zhiting Hu. \"Reasoning with Language Model is Planning with World Model.\" In The 2023 Conference on Empirical Methods in Natural Language Processing.  \n[4] Nakano, Reiichiro, Jacob Hilton, Suchir Balaji, Jeff Wu, Long Ouyang, Christina Kim, Christopher Hesse et al. \"Webgpt: Browser-assisted question-answering with human feedback.\" arXiv preprint arXiv:2112.09332 (2021).  \n[5] Yang, Kaiyu, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J. Prenger, and Animashree Anandkumar. \"Leandojo: Theorem proving with retrieval-augmented language models.\" Advances in Neural Information Processing Systems 36 (2023): 21573-21612."}]

Author rebuttal:

Meta-review: The paper introduces a PAC‑learning framework for verifiers that assess step‑wise Chain‑of‑Thought (CoT) reasoning, distinguishing simple (SVPAC), trustable (TVPAC) and strong (‑TVPAC) verification goals. It delivers new sample‑complexity upper and lower bounds for finite and VC‑dimension‑bounded verifier classes, clarifies the role of gold‑standard solutions, and connects these theoretical results to concrete settings such as math‑problem benchmarks (e.g., GSM8K) and interactive theorem‑proving scenarios. Reviewers liked the originality of formalizing verification goals, the clarity of key theorems, and the potential impact on reliable LLM reasoning, while noting that the exposition could better situate the work within existing LLM‑verification literature and provide more concrete examples. It seems that the authors’ rebuttal addressed most concerns. Given the solid theoretical contributions, relevance to emerging verification pipelines for LLMs, and the overall consensus that leans to towards accept as well as my own reading, I am recommending acceptance.
Decision: Accept (poster)