On Learning Verifiers and Implications to Chain-of-Thought Reasoning

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.

We propose the following updates to improve our writing based on the suggestions in the review.

Introduction. We propose to add the following list of contributions to make our problem statement and overall contribution clear.

• 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.

• 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.

• 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.

• 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.

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.

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).

Discussion of assumptions and implications. Our assumptions mainly correspond to different verification goals that one might have.

1. 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.

2. 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.

3. 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).

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.

LeanDojo 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.

On distributional assumptions [Line 158]

In 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.

On gold standard assumption [Line 163-164] “Line 190: why do we make this assumption?” [the number of gold standard reasonings is small]

Discrete 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).

[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.

We 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.

“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?”

Yes, 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).

References

[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.
[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.
[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.
[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).
[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.

We thank the reviewer for their time and address their concerns below.

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.

Our 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.

We 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).

Clarification related to data format: We describe below the format of training data for the different verification goals studied in our paper.

1. 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.

2. 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.

3. 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).

“ the data is assumed to be given on an almost sub-sentence level… LLM is seeing only tokens and not these sub-sentence entities.”

Our 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.

We thank the reviewer for their time and their appreciation of our contributions.

“One can feasibly talk about classifiers and verifiers within their domain's first-order logic.”

This 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.

We 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.

“Given the impossibility of an effective CoT verifier with sufficiently many traces, what implication would one expect for trustable/trustworthy verifiers”

Our 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.

Our 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.

“Given the impossibility of a sound and complete verifier in an infinite space, what feasible recommendations can be provided for designing a robust LRM?”

This 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.

But 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).

“An interesting research question is how to describe domains admitting a trusted verifier that almost surely gives a correct answer to a new question.”

We agree with the reviewer that this is a very interesting question for future research.

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.

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.

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.

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).

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.)

We 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).

“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?”

We 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.

“What would be a rough estimate for |H| in terms of the size of the dataset and the number of steps?”

Note 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|.

In 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).

Examples in the Appendix are still abstract. Would it be possible to make a concrete example using Math benchmark problems (like easy problems, GSM8K)?

Decomposing a CoT thought Can we divide a chunk of text from LLM into separate blocks of tokens? Do (Joshi 2025) or (Malach 2024) show how to decompose the text? Those papers are more like showing LLM can generate CoT in a theoretical sense, not like providing a way to divide a chunk of text into separate steps. Could you correct if I misunderstood those two papers and your response?

Weak and strong verifiers

• weak verifier is a model trained on human annotated CoT dataset (step correctness, the first one is annotated by human).
• strong verifier: no solution or intermediate evaluation on CoT given. This verifier is a model trained on problem sets with a small fraction of them having a gold standard or one random correct answer.

How to design verifiers from this principle? How do you prepare the training set, and what is the sample complexity given the analysis result?

Additional question When we sample a math problem in the whole problem set, some problem instances are similar to each other, but every instance is different. The steps may follow similar mathematical concepts, but each step is all different; at least some numbers plugged into the formula used are different. Both weak and strong verifiers make correct decisions on unseen problems in the training set, when some labels are given in that training set. I am confused about this. Maybe GSM8K dataset is an easy case to illustrate the idea. Could you explain why such learning is possible?

We thank the reviewer for taking the time to read our response and following up. Please find further clarification below.

Connection with Math benchmark problems like GSM8K. The GSM8K dataset consists of grade school math problems and was introduced by Cobbe et al. who train verifiers on the reasoning traces generated by the generator (large reasoning model). The difference between our setting and theirs is that we assume we have the correctness information for the reasoning trace up to the first incorrect step, while they use the exact correctness (whether the solution matches tokenwise) to serve as the correctness for every token in the reasoning trace generated by the generator. Here the reasoning steps consist of single calculations expressed as an English sentence, see Cobbe et al. for examples.

Decomposing a CoT thought. In addition to the GSM8K example above, there has been theoretical work studying LLM generation in terms of reasoning steps (e.g. Shai Shalev-Shwartz and Amnon Shashua [2025]). While Joshi et al. (2025) and Malach (2024) motivate their framework as token-wise generation, their analysis also applies to generating reasoning steps consisting of a collection of tokens by replacing the set $\Sigma$ of tokens by a sequence $\Sigma^{\le n}$ of tokens of length at most $n$ (i.e. larger vocabulary size, but sample complexity bounds are still reasonable).

Weak and strong verifiers. To design the weak/strong verifiers, one could simply find the verifier in the verifier class (e.g. neural networks with a specific architecture) that minimizes the training error on a training set of sufficient size. As the reviewer notes, one way to prepare the training sets is by human annotation (semi-supervised or weakly supervised extensions are interesting research questions). We provide various sample complexity upper bounds in our paper that depend on the verification goal and the complexity of the verifier class, for example scaling with $\log |H|$ for finite classes $H$ (Theorems 3.2 and 4.3) and with the VC dimension of $H$ for infinite classes (Theorems 3.3 and 4.4). Please refer to the following table for a summary of the data, learning algorithms and sample complexities for the different verification goals.

Additional question. It is correct that different problems will have different proofs and the verifier will encounter unseen problems and steps that were never encountered in the training set. The verifier's task is to check stepwise if the last step in the proof follows from all the steps so far. For example, for a step-by-step arithmetic reasoning showing the digitwise calculation for adding two positive integers, the verifier needs to simply be able to check if the carry-on was done correctly and be able to check additions of up to three single-digit numbers.