Prover-Verifier Games improve legibility of LLM outputs

## Abstract

Abstract One way to increase confidence in the outputs of Large Language Models (LLMs) is to support them with reasoning that is clear and easy to check — a property we call legibility. We study legibility in the context of solving grade-school math problems and show that optimizing chain-of-thought solutions only for answer correctness can make them less legible.
To mitigate the loss in legibility, we propose a training algorithm
inspired by Prover-Verifier Game from Anil et al. ( 2021 ) . Our algorithm iteratively trains small verifiers to predict solution correctness, “helpful” provers to produce correct solutions that the verifier accepts, and “sneaky” provers to produce incorrect solutions that fool the verifier. We find that the helpful prover’s accuracy and the verifier’s robustness to adversarial attacks increase over the course of training. Furthermore, we show that legibility training transfers to time-constrained humans tasked with verifying solution correctness. Over course of LLM training human accuracy increases when checking the helpful prover’s solutions, and decreases when checking the sneaky prover’s solutions. Hence, training for checkability by small verifiers is a plausible technique for increasing output legibility. Our results suggest legibility training against small verifiers as a practical avenue for increasing legibility of large LLMs to humans, and thus could help with alignment of superhuman models.

## 1 Introduction

Figure: Figure 1: Key result. Optimizing for solution correctness leads to high accuracy, but poor legibility. Initialization (pretrained on a variety of human-written math derivations) has higher legibility, but worse accuracy. Our proposed method retains high legibility with an accuracy in between the initialization and the correctness-only baseline. The resulting trade-off illustrates a legibility tax.
Refer to caption: x1.png

As machine learning systems find uses in higher stakes areas, it becomes increasingly important to justify why we can trust their outputs and delineate when such trust should not be placed. One possible way to gain trust in the output of a complex system is to require that the system produces an explanation of its output that is *legible* to humans or another trusted system, i.e. can be fully understood to the extend that any possible errors would be spotted. For example, to build trust in the judicial system we ask courts to produce clear and legible written opinions that explain and support their decision making.

In this paper we ask whether we can make outputs of capable LLMs more legible to humans. One direct approach is to optimize model outputs for legibility via human feedback (e.g., RLHF; ), which has its limitations (Casper et al., ). We study a complementary approach, and ask whether optimizing larger LLM provers to produce Chain-of-Thought (CoT) solutions checkable by smaller LLM verifiers makes them more legible to humans. Our motivations for studying smaller verifiers as a proxy for humans include: (1) LLMs are already used to aid with judging LLM outputs and this approach is more scalable than relying on humans alone (Bai et al., ; Saunders et al., ; Markov et al., ), (2) varying the capability gap (in terms of pretraining compute) between prover and verifier lets us study legibility as a function of this gap, and (3) when human feedback is limited for advanced systems, making outputs verifiable by less capable verifiers may incrementally aid human legibility (Leike et al., ; Christiano et al., ).

Checkability — i.e. the capacity of a verifier to independently check the correctness of solutions generated by a helpful prover — can be defined by a combination of two properties:

- 1.
Completeness. For any input in the domain of interest, the helpful prover generates correct solutions and the verifier accepts them as correct.
- 2.
Soundness. The verifier rejects all incorrect solutions produced by any adversarial provers of the same model class as the helpful one.

The definitions are inspired by literature on Probably-Approximately Correct (PAC) verification and interactive proof systems (Goldwasser et al., ; Mutreja and Shafer, ). In informal domains, neither models nor humans can be expected to be perfectly complete or sound. We instead study relaxed versions of completeness and soundness. Instead of perfect completeness we expect the helpful prover to have high pass rate and the verifier to have high recall on helpful samples. Instead of perfect soundness we expect the verifier to have low false positive rate on adversarial inputs produced through limited amounts of optimization. When we find helpful provers and verifiers with such limited completeness and soundness properties, we say that the helpful prover is legible to the verifier. This is analogous to saying that outputs are legible to humans if humans accept them as correct and can’t be fooled by similar-looking incorrect outputs.

To obtain legible provers and robust verifiers, we propose using checkability training - an iterative algorithm inspired by the Prover-Verifier Game (PVG;   ). We formulate a version of the game where the verifier moves first assuming that the prover will play best response strategy conditioned on the verifier’s strategy (i.e., the verifier "leads" and the prover "follows"), and show that for provers with unconstrained model class, finding a verifier-leading Stackelberg equilibrium is equivalent to finding a perfectly legible protocol with respect to the verifier (Theorem 1). Our iterative algorithm is inspired by that version of the game, while optimizing losses that have better convergence properties in practice.

In practice we alternate between training a verifier language model and a prover language model that we prompt to act either helpful or sneaky on disjoint subsets of grade-school math problems with known ground truth answers (Cobbe et al., )(^1^11We focus on the easier case where some ground truth labels are available for improving the players, and leave the semi-supervised or unsupervised settings for future work (see Section 6.1 for more discussions).). In each round, we first train the verifier using supervised learning to predict correctness of solutions sampled from a balanced mixture of provers from previous rounds. Next, we optimize the prover using reinforcement learning with respect to a reward combining the solutions’ correctness and the current round verifier acceptance rate ("convincingness"). The prover is conditioned on a role sampled uniformly from "helpful" and "sneaky". In the helpful role, we reward being convincing and correct. In the sneaky role, we reward being convincing and incorrect.

Our main results are illustrated in Figure 1:

- •
Direct reinforcement learning on solution correctness produces solutions that are difficult for humans to evaluate. If we optimize our prover only for solution correctness, it can achieve high performance on grade-school math problems. However, the solutions produced by the model are very different from human-written solutions and consequently are difficult to evaluate for time-constrained humans (Section 4.1).
- •
Our proposed checkability training achieves decent performance while retaining legibility.
After checkability training, we obtain a a prover that produces solutions that have better performance-legibility trade-off. It has lower test performance than the prover optimized for correctness alone, which represents an instance of a legibility tax (Leike, ). The checkability training partially closes the gap, as the prover’s pass rate improves in later rounds of training (Section 4.3.3).

Verfiability training produces three useful artifacts — a robust verifier, a sneaky prover, and a helpful prover. We evaluate the legibility of the sneaky and helpful prover as well as the soundness of the verifiers. The main findings are:

- •
The verifiers show increasing soundness over training rounds, as measured via difficulty of various sneaky-only attacks and balanced best-of-$n$ accuracy (Section 4.3.1).
- •
The sneaky prover generates increasingly subtle flaws, since the average step-by-step correctness judged by GPT-4 increases, and the average human judge accuracy on sneaky solutions decreases (Section 4.3.2).
- •
The helpful prover achieves higher pass rates, and human trainers judge them correctly more often at high rounds (Section 4.3.3).

Figure: Figure 2: Checkability training produces legible and well structured solutions. Three sample solutions produced by the helpful prover from different rounds of checkability training.
Refer to caption: x2.png

Overall, we found it surprising that legibility to smaller LLMs seems to transfer to legibility to humans — sneaky solutions that are harder to detect for smaller verifiers are also harder to detect for humans, and helpful solutions that are more legible to smaller verifiers are also more legible to humans. In the case that future LLMs acquire superhuman capabilities, training them to be more legible will help humans evaluate their correctness. Hence, prover-verifier game is a promising candidate for a scalable oversight method.

## 2 Related work

##### Computational complexity.

Our training setup is most similar to learning a verification protocol for NP (Micali, ). If we allow more interactions, we can extend the PVG setup to interactive proofs (Babai, ; Goldwasser et al., ).
Goldwasser et al. () and Mutreja and Shafer () applied interactive proofs to Probabilistic-Approximately Correct (PAC) verification. They showed that a verifier can learn a hypothesis class with much less data by interacting with an untrusted prover ($O(\sqrt{VC(\mathcal{H})})$ sample complexity for a hypothesis class of Vapnik-Chervonenkis dimension $VC(\mathcal{H})$). In our work, we assume capability (instead of data) constraint on the verifier (it cannot independently produce a solution without the help of a prover even with infinite data). Anil et al. () first made the connection from prover-verifier games to the alignment problem. They proved that different game setups lead to equilibria of different desirability, and empirically showed promise in toy experimental settings. Wäldchen et al. () applied prover-verifier games to interpretability for image classification. Unlike all those previous works, our verifier’s task is not classifying the inputs but rather judging the correctness of solutions. Amit et al. () trained LLM provers against a manually-defined verifier; in contrast, our verifier is learned. We take inspirations from those theoretical works and aim to empirically train for checkability on a nontrivial domain at scale.

##### Scalable oversight.

The central hypothesis that discrimination is easier than generation is common to many scalable oversight methods (Bowman et al., ) including critiques (Saunders et al., ; McAleese et al., ) and debate (Irving et al., ). Parrish et al. () showed negative results for improving time-limited human judge accuracy though human debate. Previous works have also studied using LLMs as judges or debaters, although they differ on whether ground truth labels are available for training. Our setup is similar to single-turn simultaneous debate where the helpful and sneaky provers try to convince the model judge of different answers, assuming that some ground truth labels is available for improving both the provers and the verifier. Similarly, using supervised training, Radhakrishnan () trained model debaters and judges and showed that the optimization makes the debaters more convincing and the judges more accurate. Michael et al. () showed that debate works better than consultancy (showing the argument from a helpful prover half the time and sneaky half the time) for human judges. In our setup the judge does not see both sides at the same time, so it is more similar to the consultancy approach. Khan et al. () showed that LLMs trained using persuasiveness signal only (no ground truth labels) can help both non-expert model and human judges. All of those works mainly use the QuALITY dataset (Pang et al., ), where the task is question-answering about a fictional story, so the justifications mainly consistent of verified quotes from the text. In contrast, we focus on a less artificial, more challenging reasoning domain where the difference between provers and verifiers isn’t privileged information but capability gap.

##### Chain-of-Thought.

Prompting LLMs to produce Chain-of-Thought (CoT) solutions is useful for boosting accuracy (Wei et al., ) and CoTs can be used as natural justifications for the final answer.
However, CoTs are not guaranteed to be legible a priori and our checkability training is one way to train CoTs to be more legible. Many works guide the model to produce a specific type of structured CoT, such as task decomposition (Christiano et al., ; Radhakrishnan et al., ; Wen et al., ), recursive summarization (Wu et al., ), and symbolic reasoning (Lyu et al., ). Lightman et al. () use expensive step-wise human supervision to train models that can solve math. In contrast, we do not enforce any output structure, and rely solely on final answer supervision. Our checkability training method is general and can be readily studied in any domain where we have some ground truth labels. Legibility emerges as a natural consequence of the training dynamics (Figure 2).

##### Explainability and legibility as complementary properties.

Explainability (Zhao et al., ) tries to give an account of the prover model’s reasoning, whether the reasoning is correct or not. The resulting explanations can be arbitrarily complex (Nanda et al., ). In contrast, legibility of a prover model’s output allows to verify if a given solution is correct, ignoring how the prover reasoned about it. Consequently, legibility requires model outputs that are coherent and accessible to human understanding (Rudin, ). It is possible to have either without the other, but especially in high-stakes settings correctness is more important than understanding (Ziegler et al., ).

##### Adversarial Robustness.

Deep neural networks are susceptible to adversarial attacks (Szegedy et al., ; Biggio et al., ). The decade-long work on adversarial defenses had limited success for vision models (Croce et al., ). Language models have discrete input-output tokens and hence its not as straight-forward to perform gradient-based attacks (Carlini et al., ) but white-box (Zou et al., ) and black-box (Shah et al., ; Hayase et al., ) jailbreaks that can undo the alignment process are still found. Requiring a perfectly robust verifier is not realistic either for models or humans (Elsayed et al., ). Our checkability training can be viewed as adversarial training on the verifier, and we show that robustness transfers to test attacks different from training attacks in Section 4.3.1, which is similar to common methods in the adversarial robustness literature (Carlini et al., ).

##### Legibility in concrete applications.

Prior works have studied legibility in different contexts. For example, in robotics, legibility refers to being able to interpret an agent’s intent based on its action (Dragan et al., ). For coding, human legibility has multiple facets including being able to correctly trace the execution, find bugs, or summarize goals (Oliveira et al., ; Wen et al., ). In this work we measured human legibility via the accuracy of their judgement of solution correctness in time-limited settings, which is only one of many ways to measure human legibility.

Figure: Figure 3: Schematic illustrating the legibility problem. A poorly aligned, superhumanly capable AI might produce highly efficient code that sacrifices legibility for conciseness or performance. Code is slightly adapted from the bitonic sorter for parallelized sorting of elements in a list (Wikipedia contributors, ).
Refer to caption: extracted/5769164/figures/comic_v3.png

## 3 Setup

In general, we consider a dataset of problems with ground truth answers $(x,y)\in\mathcal{X}\times\mathcal{Y}$, where $x$ denotes a problem statement and $y=y(x)$ denotes the known and unique ground truth answer. Given a proposed solution $z$ to the problem $x$ including a final answer, we let $\mathds{1}_{\text{correct}}\left({x,z}\right)$ be the correctness indicator that is $1$ if the solution proposes an answer that is the same as $y(x)$ and 0 0 otherwise. We use a SymPy grader (Meurer et al., ) for evaluating $\mathds{1}_{\text{correct}}\left({x,z}\right)$ on grade-school math (GSM) problems.

We have a prover $\pi(z|x)$ proposing solutions given a problem statement, and a verifier $v(x,z)\in[0,1]$ that estimates the correctness of the solution’s answer. We call the output of the verifier the *convincingness score*.

### 3.1 From checkability to the Prover-Verifier Game

We start with a formal definition of checkability. Prover $\pi$ from model family $\mathcal{H}$ is *verifiable* to verifier $v$ on the data distribution $P_{XY}$ if and only if the prover always generates *correct* and convincing solutions, and no adversarial / "sneaky" prover from the same model family $\mathcal{H}$ can fool the verifier into accepting incorrect solutions. Formally,

- •
Completeness:
$\forall x\in\mathcal{X},\mathds{1}_{\text{correct}}\left({x,\pi(x)}\right)=v(x
,\pi(x))=1$.
- •
Soundness: $\forall\pi^{\prime}\in\mathcal{H},\forall x\in\mathcal{X}$, $\mathds{1}_{\text{correct}}\left({x,\pi^{\prime}(x)}\right)=0\implies v(x,\pi^
{\prime}(x))=0$.

A few notes on the definition above: First, checkability doesn’t necessarily capture everything we intuitively want from legibility, and we hope to inspire other definitions in future works. Second, we restricted the sneaky prover to be from the same model family as the helpful one. This is because we are interested in answering the question “Can one intelligent system trust another intelligent system of a certain size, architecture, and trained with certain algorithms?". Hence we only have to ensure that the verifier is robust to the class of models we solicit answers from. Third, in empirical work we only seek to find approximate completeness and soundness. Since the verifiers and provers we study are neural networks, it is impractical to find perfect completeness and soundness. Therefore we study a relaxation of completeness and soundness in the following sense: (1) for the helpful prover we require that the it is correct in distribution $P_{XY}$ with high probability; and (2) for the verifier, we require that it is robust to a limited set of black-box attacks that are relatively "close" to the honest prover (intuitively, we want the verifier not to miss small errors that would make the conclusion invalid). We will compare verifiers’ soundness via their ranking on a variety of attacks, and the more comprehensive the attacks are the closer we get to measuring soundness.

We propose to train legible prover and sound verifier using variants of the prover-verifier game (Anil et al., ). We formulate it as a two-player game between a role-conditioned prover $\pi$ and the verifier $v$. We use shorthand $h(x)=\pi(x,\text{role=helpful})$ for the prover conditioned on the helpful role and $s(x)=\pi(x,\text{role=sneaky})$ for the prover conditioned on the sneaky role.

We define the verifier’s utility as a negative classification loss on a uniform mixture between the helpful and the sneaky samples,

$$ $\displaystyle R_{V}=-\frac{1}{2}\mathbb{E}_{x\sim P_{X}}{l(v(x,h(x)),\mathds{1 }_{\text{correct}}\left({x,h(x)}\right))}-\frac{1}{2}\mathbb{E}_{x\sim P_{X}}{ l(v(x,s(x)),\mathds{1}_{\text{correct}}\left({x,s(x)}\right))}$ $$

where $l(v,c):[0,1]\times\{0,1\}\rightarrow\mathbb{R}$ is a loss function minimized if and only if $v=c$, such as the cross-entropy loss. We assume without loss of generality that $l(c,c)=0$. In practice we optimize $R_{V}$ via gradient descent on $l_{V}=-R_{V}$.

The policy is conditioned on either the helpful or the sneaky role with equal probability, and the combined reward is

$$ $\displaystyle R_{P}=\frac{1}{2}\mathbb{E}_{x\sim P_{X}}{r(v(x,h(x)),\mathds{1} _{\text{correct}}\left({x,h(x)}\right))}+\frac{1}{2}\mathbb{E}_{x\sim P_{X}}{r (v(x,s(x)),1-\mathds{1}_{\text{correct}}\left({x,s(x)}\right))}$ $$

where $r(v,q):[0,1]\times\{0,1\}\rightarrow\mathbb{R}$ is a reward function that satisfies:

$$ $\displaystyle\forall v_{1},v_{2}\in[0,1]:r(v_{1},1)>r(v_{2},0),$ $\displaystyle\forall v_{1},v_{2}\in[0,1],v_{1}>v_{2}:r(v_{1},1)>r(v_{2},1).$ (1) $$

Here $q\in\{0,1\}$ indicates that the correctness of the solution is role-aligned — it is 1 if the prover is assigned to be helpful and the solution is correct, or the prover is assigned to be sneaky and the solution is incorrect. The two assumptions on the prover reward functions above are: First, any role-aligned solution gets higher reward than any role-misaligned solution; Second, for any role-aligned solution, the prover gets higher reward when the verifier gives the solution higher score. In practice we optimize $R_{P}$ via reinforcement learning since we cannot differentiate with respect to the solution, because it requires iterative auto-regressive sampling of LLM tokens, a non-differentiable operation.

We show a connection between the prover-verifier game and the completeness and soundness objectives as follows:

###### Theorem 1 .

Assuming that $\mathcal{H}$ is the set of all deterministic mappings from $\mathcal{X}$ to $\mathcal{Z}$, in the PVG where verifier’s utility is $R_{V}$ and the prover’s utility is $R_{P}$, the existence of a verifier-leading Stackelberg equilibrium $(v^{*},h^{*},s^{*})$ is necessary and sufficient for the completeness and soundness properties to hold for $(v^{*},\pi^{*})$.

One of the players (in our case, the verifier) is the leader, and the other player (the prover) is the follower. We assume that given a leader strategy, the follower will always play its best response, and the leader picks its strategy based on this knowledge. A Stackelberg equilibrium means that none of the players have incentives to change its strategy. The proof is in Appendix A. Compared to Theorem 2 in Anil et al. (), we have more relaxed assumptions on the loss function and reward.

In practice, LLMs are probabilistic models and the hypothesis class of LLMs is only a subset of all mappings from $\mathcal{X}$ to $\mathcal{Z}$, so our empirical setup does not match the theoretical assumptions exactly. Furthermore, when the players are nonconvex models like neural networks, we do not have formal guarantees for finding a Stackelberg equilibrium efficiently. However, we can train the models using coordinate descent to find an approximate local equilibrium.

###### Theorem 1 .

### 3.2 Checkability training

In practice, we design training objectives for the verifier and the provers using slight variations on $l$ and $r$. Most notably, we train the verifier using a relative loss based on comparisons between correct and incorrect solutions for each question (Bradley and Terry, ), instead of an absolute loss for each solution. For the prover reward $r$, we have three variants that prioritizes verifier score $v$ and role-alignment $q$ differently. Both provers and verifiers are from the GPT4 family (Achiam et al., ). We initialize the prover and the verifier with different sized models that have been lightly finetuned on a variety of math data from the pretaining distribution, including human written proofs and derivations. We discuss the algorithmic details below.

First, we augmented the GSM (Cobbe et al., ) dataset using $100k$ synthetically generated and validated datapoints from ChatGPT, similar to the method in Liu et al. (). We made the dataset larger so as not to be bottlenecked by sample efficiency in order to focus on the training dynamics. We validated that the the original test set accuracy is not impacted by using real vs. synthetic data. Next, we randomly partitioned the training dataset $\mathcal{D}$ into two equally-sized subsets $\mathcal{D}_{\pi}$ and $\mathcal{D}_{V}$ that are used for training the prover $\pi$ and the verifier $V$ respectively. This way the verifier and the prover are never optimized on the same prompt.

The training proceeds in multiple rounds, and each round the verifier training phase precedes the prover training phase. The only change between rounds is the data mixture used to train the verifier; no other state, such as model weights, is carried over between rounds.

In the verifier training phase of round $i$ we train verifier $V_{i}$ to minimize the regularized comparison loss

$$ $\displaystyle\mathbb{E}_{x\sim D_{V}}\left[\mathbb{E}_{z_{1},z_{2}\sim\pi^{*}} \log\sigma\left[\left(V(x,z_{1})-V(x,z_{2})\right)\cdot\text{sign}{(}\mathds{1 }_{\text{correct}}\left({z_{1}}\right)-\mathds{1}_{\text{correct}}\left({z_{2} }\right))\right]+\lambda E_{z\sim\pi^{*}}V(x,z)^{2}\right]$ $$

Here $V(x,z)\in\mathbb{R}$ is a scoring function and not restricted to range $[0,1]$ like the theoretical formulation. We use capitalized $V$ to avoid confusion. The first term is the reward modeling objective that maximizes log likelihood of correct solutions being ranked higher than incorrect solutions under the Bradley-Terry model, similar to Ouyang et al. (). The second term is a regularizer that is meant to center $V$ at 0 0.
Without this term, adding an arbitrary per-problem constant to $V$ would not change the objective. In preliminary experiments we found the this objective to be interchangeable to the cross-entropy loss for the overall dynamics of checkability training and we adopted this form due to engineering convenience.

The prover $\pi^{*}$ used for sampling solutions for verifier training is a mixture of an initial base prover and previous round provers, each balanced to have equal number of correct and incorrect solutions. Each of the previous rounds has equal ratio in the mixture, which is tuned as a hyperparameter.
In round 0, the solutions are from the base prover sampled via a few-shot prompt (App. H). In later rounds of training, we replace part of the solutions with those from the new provers. Hence we always use the same number of solutions per problem. The amount of verifier optimization is constant over the rounds.

During the prover training phase we use Proximal Policy Optimization (PPO; ) to maximize an expected reward $R$ derived from the current round verifier score and whether the correctness is aligned with the assigned role. The prover’s objective is to maximize the following reward (minus a small KL regularization towards the initialization):

$$ $\displaystyle\mathbb{E}_{x\sim D_{\pi},\text{role}\sim\{\text{helpful, sneaky} \},z\sim\pi(\cdot\mid x,\text{role})}R(z\mid x,\text{role}).$ $$

We experimented on three variants of $R$. We call the first reward variant the Signed Relative Convincingness (SRC) reward. Given a problem $x$, let the role indicator $\mathds{1}_{\text{helpful}}\left({\text{role}}\right)$ be 1 if the prover is assigned to be helpful and 0 otherwise. Suppose conditioned on a role and $x$, the prover generated a batch of solutions $\{z_{0},\dots,z_{b}\}\sim\pi(\cdot\mid x,\text{role})$ with verifier scores $\{V(x,z_{0}),\dots,V(x,z_{b})\}$. Since the scores are not normalized, we first batch-normalize the scores to mean 0, i,e. $V^{\prime}(x,z_{i})=V(x,z_{i})-(\sum_{j=1}^{b}V(x,z_{j}))/b$, and then set the reward as follows:

$$ $\displaystyle R_{\text{SRC}}(z_{i}\mid x,\text{role})=\begin{cases}(2\mathds{1 }_{\text{correct}}\left({x,z_{i}}\right)-1)\cdot(2\mathds{1}_{\text{helpful}} \left({\text{role}}\right)-1)\cdot V^{\prime}(x,z_{i})&\text{if $V^{\prime}(x, z_{i})>0$}\\ -1&\text{otherwise}\end{cases}$ (2) $$

Ignoring the verifier score range discrepancy, the first case is equivalent to setting $r(v,q)=v\cdot(2q-1)$, i.e. when $\mathds{1}_{\text{correct}}\left({x,z_{i}}\right)=\mathds{1}_{\text{helpful}}
\left({\text{role}}\right)$, the reward equals the normalized verifier score, otherwise it equals negative score. This case satisfies our assumptions (3.1) that any role-aligned solution has higher score than any non-aligned one, and for any two role-aligned solutions, the one with higher verifier score gets higher reward. However, the second case where any solution below average score is directly assigned a score of -1 deviates from the theoretical formulation. The rationale for this case is to prioritize convincingness over role-alignment. We show in section 4.2 that this is practically useful for convergence.

The second reward variant that prioritizes role-alignment is the Correctness-Gated Convincingness (CGC) reward:

$$ $\displaystyle R_{\text{CGC}}(z\mid x,\text{role})=\begin{cases}V(x,z)&\text{if $\mathds{1}_{\text{helpful}}\left({\text{role}}\right)=\mathds{1}_{\text{ correct}}\left({x,z}\right)$}\\ V_{0}&\text{otherwise}\end{cases}$ (3) $$

where $V_{0}$ is a constant that is practically lower than all verifier scores (we used -2 in our experiments). This reward corresponds to $r(v,q)=qv+(1-q)\inf{v}$ which satisfies the reward assumptions (3.1) ignoring the discrepancy in verifier score range. Empirically, this reward leads to worse dynamics than the SRC reward (Section 5.1).

We also consider a setup that we call Iterative Goodharting where the helpful and sneaky provers both use the following reward,

$$ $\displaystyle R_{\text{goodhart}}(z\mid x)=V(x,z)$ (4) $$

which means the reward encourages only convincingness, i.e. $r(v,q)=v$. This version does not satisfy assumptions (3.1) because $r(v,0)=r(v,1)$. The empirical results are in Section 5.2.

## 4 Results

### 4.1 Baseline: Direct Optimization for Correctness

Figure: Figure 4: Learning from a binary grader leads to strong performance, but poor legibility. a Model accuracy as a function of RL training steps. The pronounced drop at 8k steps is due to solutions reaching the maximum completion length. b Mean accuracy of time-constrained human contractors when evaluating solutions from the initialization ($\bullet$), after 3k steps ($\blacktriangle$), or 7k steps ($\star$). c Mean time required by the time-constrained human contractor to correctly label solutions. d Mean accuracy of contractors per solution as a function of model accuracy on the same solution for solutions from the initialization (grey), the prover after 3k steps (dashed blue), or 7k steps (solid blue). For each experiment, we separate data into quartiles according to the model accuracy before averaging. See Appendix I for details on the experiment set-up.
Refer to caption: x3.png

A natural baseline for our setup is to train the prover model directly to optimize for the correctness of the solutions without the intermediate verifier. Specifically, we can use Proximal Policy Optimization (PPO) against a binary grader that checks if the solution is correct or not. This approach has been explored in works such as Havrilla et al. (), where a language model is fine-tuned using reinforcement learning (RL) with a reward based on the correctness of the answers. We use a KL regularization towards prover initialization with the same small coefficient for all methods in this paper.

We find that, indeed, optimizing our prover with correctness as the only goal achieves strong performance on grade-school math problems (Fig. 4a). When inspecting samples from the resulting prover, we notice that the solution becomes longer as the prover solves each question in multiple ways and later in training become largely unintelligible (Appendix Fig. S1) despite still producing the correct answer.

To measure how much the peculiar style affects legibility of solutions, we presented samples from different points during training to human contractors and asked them to determine the validity of the solutions under a strict 45 second time limit per solution. They were asked to judge the correctness of the given solution rather than the final answer (see Appendix I for full instructions and a task example). While the contractors were able to reliably distinguish correct and incorrect solutions from the prover initialization, their accuracy and speed deteriorated noticeably when presented with solutions from the trained prover (Fig. 4b,c). This decrease in human legibility is most pronounced for questions that the model cannot reliably solve (Fig. 4d).

In summary, we observe that when trained solely for correctness, our model learns to produce useful but unintelligible solutions that time-constrained humans struggle to evaluate.

### 4.2 Dynamics of checkability training

To study whether it is possible to retain legibility while improving performance, we ran several rounds of checkability training on the augmented GSM dataset. In this section, we present results where the provers are trained using the Signed Relative Convincingness (SRC) reward (Eq. (2)), which is the reward that that we found most effective for improving legibility.

Figure: Figure 5: Dynamics of the prover training phase across rounds for one pair of verifier and prover. Mean verifier score of correct (solid) and incorrect (dashed) solutions (a) and accuracy (b) as a function of RL training steps, for subsequent rounds (columns) and for the helpful (red) or sneaky (brown) prover. Arrow indicates increasing number of steps before the accuracy of the sneaky prover drops below 10%. We early stop when sneaky incorrect solutions become as convincing as helpful correct solutions. This verifier is $10^{-3}$ the size of the prover. c Average accuracy for the helpful (top) and sneaky (bottom) provers as a function of the completed fraction of each round.
Refer to caption: x4.png

Within each round of the prover training phase, both the sneaky and the helpful prover monotonically improve their convincingness to the small verifier (Fig. 5a). In contrast, the fraction of correct solutions produced by the provers evolves non-monotonically (Fig. 5b,c). While the helpful prover largely produces increasingly correct solutions, the sneaky prover eventually produces incorrect solutions that match or surpass the verifier score of correct solutions from the helpful prover in the first few rounds of training. The helpful prover’s performance decreases at the end of each round potentially due to weight sharing with the sneaky prover (they are a single LLM with different prompts). Note that the prover and the verifier have the same initializations at the beginning of each round, and the only difference between rounds is the data mixture used to train the verifier.

We were curious to see if the above dynamic holds also for a wider range of pairs of verifier and prover effective compute amounts. When only varying the size of the verifier by a few orders of magnitude ($10^{-3}$ to $10^{-1.8}$-times the compute of the prover), the dynamics remain largely unchanged (Fig. 5c). However, when using a much smaller verifier ($10^{-4}$-times the compute of the prover), the checkability training becomes unstable and produces weak provers with poor legibility (Sup. Fig. S4). Similarly, using a verifier that matches the size of the prover ($10^{0}$-times the compute of the prover) prevents the verifier from becoming more robust in subsequent rounds and produces provers with strong performance but poor legibility (Sup. Fig. S5). We cannot exclude the possibility that the poor performance of very small and large verifiers is due to non-optimal hyperparameters, but we also suspect there are real reasons for checkability training to not work well for these verifiers. In particular, if the verifier’s capability is too limited, it may be fundamentally impossible to perform verification. If the verifiers are very similar to the provers, the sneaky prover can more easily simulate the verifier’s mistakes (Burns et al., ), making it more difficult for the verifier to become robust.

To summarize, our checkability training exhibits a characteristic dynamic where the helpful prover improves at solving math problems while over subsequent rounds the sneaky prover struggles to produce incorrect, convincing solutions.

### 4.3 Evaluations of checkability to smaller verifiers and legibility to humans

At the end of each round of checkability training, we obtain three artifacts:

- 1.
a verifier trained on diverse adversarial examples,
- 2.
a sneaky prover that produces convincing, subtly incorrect solutions,
- 3.
a helpful prover that produces convincing, correct solutions.

In this section, we perform various evaluations of the soundness of verifiers and the legibility of sneaky and correct solutions across rounds of training shown in Figure 5.

#### 4.3.1 The verifier becomes more robust throughout checkability training

The verifier’s sound evaluation of adversarial inputs from a sneaky prover (of equal capability as the helpful prover) is one requirement of legibility by our definition. We observe that throughout checkability training, the sneaky prover requires increasingly many steps to discover highly convincing, incorrect solutions (Fig. 5b). However, it is unclear whether this increase is due to the sneaky and helpful provers sharing weights. Hence, we perform a variety of additional attacks by separately training sneaky-only provers that do not share weights with the helpful prover to evaluate whether the verifier becomes able to discern correct from incorrect completions beyond the exact set-up during training.

Figure: Figure 6: Verifiers increase in robustness as measured by difficulty of sneaky-only attacks and balanced best-of-$n$ accuracy a Number of steps until sneaky finds an exploit for the SRC (blue), goodharting (orange), and CGC (green) adversaries as a function of verifier sizes. We declare an attack ‘successful’ for the SRC and CGC adversaries when the sneaky becomes $95\%$ incorrect and the average verifier score of sneaky incorrect samples become as high as that of helpful correct samples from the same round. We declare a goodharting adversary ‘successful’ when optimizing a prover on the verifier score reaches accuracy $<0.2$. b Fraction of correct solutions when selecting the most convincing out of $n$ balanced samples for varying $n$ and different rounds. The solutions are from the last checkpoints of current-round helpful provers, balanced to have 50% correctness.
Refer to caption: x5.png

We performed three attacks with sneaky-only provers using the following reward functions:

- 1.
the SRC reward (2) to ablate the effect of weight sharing between the helpful and the sneaky prover.
- 2.
the CGC reward (3) to test generalization of verifier soundness to different variations of checkability training
- 3.
the goodharting reward (4) to straightforwardly test robustness to optimization for convincingness (Gao et al., )

We performed the above attacks on verifiers of different sizes across five rounds of checkability training (Fig. 6a). We observe an increase in the number of steps each adversary takes until finding an exploit. Larger verifiers are harder to exploit. For example, none of the sneaky attacks found exploits for verifiers of relative size $10^{-2}$ beyond round 0 within 8k RL steps, whereas verifier of relative size $10^{-3}$ remain exploitable by the goodharting and SRC adversaries until round 4.

The test attacks we perform are far from complete and there is no simple way to evaluate whether the verifiers are robust to all sneaky provers within the model family. Nevertheless, the rank correlation between those robustness measures do reflect a general increase in compute budget if some actor trains an adversarial prover to fool the verifier. A more complete evaluation of the verifier’s adversarial robustness would include a variety of common white-box and black-box attacks (Zou et al., ; Shah et al., ; Hayase et al., ).

Another way to assess the checkability of the helpful prover to the verifier is via best-of-$n$ accuracy at higher $n$ (Gao et al., ), where we analyze the correctness of the highest-scoring solution according to the verifier out of $n$ solutions (Fig. 6b). In order to fairly compare provers with different average pass rates, we collect balanced incorrect and correct samples and only use problems that have at least $n/2$ correct and $n/2$ incorrect samples for evaluating best-of-$n$. We sample up to 2560 solutions for each test problem and the helpful prover from each round. In Figure 6(b), for each $n$, we combine $n/2$ correct and $n/2$ incorrect solutions from the current-round helpful prover $\pi_{i}$, and evaluated the best-of-$n$ performance of verifier $V_{i}$. The balanced best-of-$n$ performance increases for ($V_{i}$, $\pi_{i}$) pairs at higher rounds, indicating that the verifier can better judge the helpful prover’s correctness even when controlling for pass rates.

#### 4.3.2 The sneaky prover becomes increasingly subtle throughout checkability training

Having established that the verifier becomes increasingly robust to adversarial attacks, we turn to analysing the sneaky attacks that do fool the verifier.

Figure: Figure 7: Flaws introduced by the sneaky prover become more localized and harder for time-limited humans to spot. a Mean (circle) and minimum (triangle) validity score over portions of correct (solid) and incorrect (dotted) solutions from the initialization (left) and from different rounds of checkability training. b Mean accuracy of time-constrained human contractors when evaluating solutions from the sneaky prover at different rounds of checkability training. This plot is from a potentially flawed campaign (see Appendix I). c Two examples of incorrect solutions with high verifier score from different points of training. Flaws are highlighted in red. Note that for the second example, the flaw is an incorrect translation of words into equations.
Refer to caption: x6.png

While sneaky incorrect solutions from early rounds often contain multiple obvious mistakes and non-sequitur, incorrect solutions from later rounds contain increasingly subtle flaws (Fig. 7c and Sup. Fig. S2). To quantify this shift, we used GPT-4 to assess the validity of small portions of sneaky solutions from different rounds (Fig. 7a). We observe that while the minimum score over portions of a solution remains very low (indicating a flaw detectable by GPT-4), the average score increases over rounds (indicating the general soundness of the remaining portions).

We were interested to see whether the adversarial attacks against the small verifier might transfer to humans. Interestingly, when presenting the sneaky solutions to the time-constrained contractors, the fraction of correctly labeled solutions was comparatively high, but decreased throughout the rounds (Fig. 7b). This indicates that the sneaky prover produced by checkability training might be useful as a tampering model for training critique models (Saunders et al., ; McAleese et al., ). Note that Fig. 7b is from a pilot study that has some design flaws (see Appendix I).

In sum, the sneaky prover produced by our checkability training is capable of generating subtly flawed solutions that are non-trivial to spot for time-constrained humans.

#### 4.3.3 The helpful prover becomes increasingly legible throughout checkability training

We finally turn our attention to the helpful prover and its evolution through successive rounds of checkability training. A key desideratum of our framework is that the helpful prover not only achieves high correctness but also maintains legibility for human evaluators.

Figure: Figure 8: Checkability training jointly increases model performance and legibility. a Mean accuracy of the helpful prover at different rounds of checkability training. b,c Mean accuracy (b) and time required to correctly label solutions (c) of time-constrained human contractors when evaluating solutions from the helpful prover at different rounds of checkability training.
Refer to caption: x7.png

We observe that as the checkability training progresses, the helpful prover produces solutions with increasing accuracy (Figure 8a). In contrast to the training for correctness only (Fig. 4), solutions from the helpful prover remain coherent throughout training (Fig. 2). This improvement indicates that the prover is effectively leveraging the feedback from the verifier to enhance its problem-solving capabilities.

To assess the human legibility of the helpful prover’s solutions, we again conducted evaluations with time-constrained human contractors. We observe that both the contractors’ mean accuracy in evaluating solutions (Figure 8b) and the time required for evaluation (Figure 8c) improve as the prover advances through successive rounds. At the end of training, the helpful prover matches the legibility of the initialization while achieving substantially stronger performance. However, the performance falls short of the performance achieved by a prover trained for correctness only (Fig. 4), revealing a tension between achieving high performance and retaining legibility (Leike, ). We note that one way to resolve this tension is to separate the model’s chain-of-thought from proof of correctness, see Appendix 6.1 for more discussion.

In summary, our findings demonstrate that checkability training facilitates the development of a helpful prover whose outputs are increasingly correct and legible. This dual improvement is critical for applications where human oversight and collaboration with AI systems are essential.

## 5 Alternative rewards

We now investigate whether using the alternative rewards for prover training affects convergence as well as legibility.

### 5.1 Checkability training with the Correctness-Gated Convincingness (CGC) reward

Figure: Figure 9: Dynamics of the prover training phase with the CGC reward across rounds. The average training verifier score (top), and the training prover accuracy for the helpful and sneaky provers (bottom). The verifier is $10^{-3}$ times the size of the prover in terms of pretraining compute. The number of RL steps until sneaky incorrect become as convincing as helpful correct decreases from round 1 to round 3 and increases from round 3 to round 5.
Refer to caption: x8.png

The Correctness-Gated Convincingness (CGC) reward (3) prioritizes correctness (for the helpful prover) and incorrectness (for the sneaky prover) over convincingness. When the helpful prover produces incorrect answers (or the sneaky prover produces correct answers), the reward is set to a constant penalty; otherwise it is the verifier score. In this section, we show that the CGC reward empirically leads to worse training dynamics.

In each round of CGC reward training, we train the prover until the average verifier score of the sneaky’s incorrect samples become as high as that of the helpful’s correct samples, and the sneaky reaches low ($<5\%$) accuracy. Figure 9 shows the prover training dynamics — the number of RL steps until the sneaky prover succeeds does not consistently increase over rounds. We observe that the sneaky prover’s accuracy quickly decreases and the convincingness rises more slowly for the CGC reward in comparison to the SRC reward. Our hypothesis is that in this case, the sneaky and helpful players quickly exploits different modes with distinct styles, and hence there are obvious spurious statistical clues that separates sneaky and helpful which won’t help the verifier learn the correctness signal. See section C for more discussion. It is possible that we did not tune the hyperparameters for the CGC reward optimally, or the verifier requires more rounds to become robust. We did not perform human evaluation for the CGC reward training due to its worse training dynamics.

Nevertheless, this alternative reward formulation serves as a strong attack for evaluating the robustness of verifier trained using the SRC reward (Section 4.3.1).

### 5.2 Iterative goodharting training

Figure: Figure 10: Iterative goodharting prover training dynamics across verifier sizes $10^{-4}$ to $10^{0}$. Overoptimization happens later at higher rounds, with some degradation for one verifier size ($10^{-3}$). Larger verifiers lead to better maximum prover accuracy and reach better robustness in fewer rounds.
Refer to caption: x9.png

We run an alternative training scheme where the prover does not have an assigned role. It is trained with reward (4), which is just the verifier score. We call this the ‘goodharting’ baseline because usually during Reinforcement Learning from Human Feedback (RLHF) (Ouyang et al., ), the prover is directly optimized to maximize the score of a reward model. When the reward model is not robust enough, it is easy to over-optimize so the prover overfits to the imperfect proxy reward. This phenomenon is called ‘goodharting’ or ‘reward hacking’ (Gao et al., ; Skalse et al., ). The verifier can learn from the incorrect and correct samples from the same prover.

In more details, for each round, we train the prover using PPO with reward (4) until its training accuracy drops below $0.2$. Next, we sample balanced correct and incorrect samples on the verifier split of the training data for all prover checkpoints throughout PPO. The samples are then mixed into the verifier training dataset for the next round. We still keep the total number of samples per problem constant for training the verifier in each round.

Figure 10 shows the training dynamics. We early stop each round when the prover’s training accuracy tanks below 0.2 on average in the last 80 RL steps. Across verifier sizes $10^{-4}$ to $10^{0}$ of the prover, the number of steps it takes for the prover to over-optimize generally increase. Up to size $10^{-2}$, the larger the verifier is, the fewer number of training rounds it requires to reach perfect goodharting robustness within 8k RL steps. Verifiers of medium size ($3\times 10^{-3}\sim 10^{-2}$) benefit most from the iterative goodharting training, where as smaller ($\leq 10^{-3}$) and larger ($10^{0}$) verifiers benefit less. We further evaluated the robustness of verifier trained using goodharting reward under attacks from the SRC reward (2) and the alternative CGC reward (3), and the verifiers’ robustness go up sometimes but not always (Figures 7(a), 7(b)). The balanced best-of-$n$ robustness increases (Figure S8).

However, when we showed the samples from the goodharting training to humans trainers, there is no significant difference in human judge accuracy across rounds (Fig. S6), although Fig. S6 is from a pilot study that has some design flaws (see Appendix I). Overall, our results on the iterative goodharting training show that it increases verifier soundness to a certain extent, but we do not have enough evidence showing that it improves human legibility.

## 6 Discussion

### 6.1 Limitations

##### Only domains that allow natural language justifications.

We studied the math domain because natural language explanations are common and often required for building trust in mathematical conclusions. However, in some domains it is difficult to support conclusions with natural language explanations. For example recognizing particular faces is easy for humans, but it’s hard to communicate to others in natural language why a particular face belongs to a particular person.

##### Need for ground truth answers and reliance on generalization.

One prerequisite for our setup is being able to certify correctness of answers of solutions produced by the prover. For the grade school math domain we rely on having a training dataset of problems with known ground truth answers (Cobbe et al., ). We anticipate this setup to be less relevant to domains where collecting any ground truth is too hard or expensive. One possible approach in this case could be to hope for favorable out-of-distribution generalization properties of legibility from solutions to problems with known ground truth answers to other domains. We don’t study out-of-domain generalization in this paper because we train on only one dataset, but we expect that training on a diverse set of domains could potentially lead to good generalization from domains with ground truth labels to the domains without labels (Burns et al., ).

##### Conflating the model’s chain-of-thought with legible solutions.

By training the CoTs to be legible, we potentially limited the provers’ accuracy. A better method could be training a first model using CoT to maximize accuracy, and then training a second model to turn the CoT used to produce the answer into a legible justification to humans. Hence, our measurement of accuracy-legibility tradeoff may be overly pessimistic; the prover may be able to achieve legibility at less or no cost to accuracy. For the correctness-only baseline, we could have early stopped at less accurate but more legible checkpoint. However, we don’t know of a principled way to do early stopping for legibility.

##### Dataset diversity and difficulty.

We conducted our empirical study on only one dataset (GSM). The dataset is relatively easy and the solutions are quite standardized. Using ChatGPT to augment this dataset could result in some incorrect labels, but based on preliminary data analysis we did not see significant difference between verifier test accuracies trained on synthetic vs. real data. We would like to extend the checkability training framework to harder math datasets and coding, as well as fuzzier domains such as human preference data (Ouyang et al., ). Our method is fully general as long as there is a finite set of final answer labels.

##### Initialization with human-written math derivations.

Our prover initialization has relatively high performance in GSM. We used a prover that has been lightly finetuned on a variety of math data to learn the correct format, and the finetuning dataset contains some of the GSM trainset data. We believe this doesn’t qualitatively affect our results and only makes it easier for the helpful prover to produce correct answers. Figure S9 shows that initialization with a base model without math finetuning leads to qualitatively similar training dynamics.

##### Heterogeneous experiment set-ups.

We have different stopping criteria for different training schemes presented throughout the paper. We trained the prover for a fixed number of RL steps in each round for certain training schemes (4k steps in Fig. 6a, 5c, 8k steps in Fig. 4, 5c, S4, S5), whereas in Fig. 5, 9, 10 we trained until early stopping criteria are met (the criteria are already discussed in those section). We do not observe qualitative different between early stopping and non early stopping rounds in our experiments.

##### Hyperparameters.

We did not tune all hyperparameters thoroughly for all training schemes in this paper. The main hyperparameter we tuned are the ratios of samples from each of the previous rounds. We tuned the ratio for one verifier size ($10^{-3}$) for the SRC reward based on whether training robustness increases across rounds, and used the same ratio for other sizes with SRC and CGC rewards, which could result in other training schemes being worse in robustness and legibility. We separately tuned the ratio for one verifier size ($10^{-3}$) for the iterative goodharting training. We used the default ChatGPT post-training hyperparameters such as the optimizer, learning rate, or KL regularization coefficient for prover and verifier training.

### 6.2 Future Work

We studied the setting in which correctness labels are available at training time for all problems. A more realistic scenario is one where not all answers have a trusted final correctness label, in which case the verifier would rely on unsupervised signals such as consistency (Wang et al., ) and convincingness (Khan et al., ). Unsupervised methods for improving legibility are an important future direction.

Another direction is developing a method to turn an illegible solution into a legible one. The CoTs that the model first uses to solve a problem are not legible to a smaller model per se but we could train a translation model that turns the ‘scratch space’ CoT to a well-written proof. This approach might be favorable over directly training the CoT to be legible since exerting any optimization pressure on the CoT may limit prover performance as well as exacerbate deceptive alignment (i.e., the model hiding its own intent) (Denison et al., ; Hubinger et al., ).

The training schemes we consider are adaptations of single-turn simultaneous games. With an interactive tool such as ChatGPT, the verifier can interact with the prover in more rounds which should increase the sample efficiency vastly based on complexity theory (Goldwasser et al., ). An example of multi-turn prover game is a “mind-changing" game: for binary outcome predictions, the prover maximally tries to convince the verifier that the answer is true / false alternatingly in context. This is similar to the market-making proposal (Hubinger, ).

We mainly studied legibility to smaller models in this paper. However, legibility to humans is what we eventually care about, so future work should more systematically study what type of assistance better help humans judge the validity of large model solutions. We expect more extensive human study to be fruitful.

### 6.3 Conclusion

We presented a tension between model performance and solution legibility in a concrete setting of judging grade-school math solutions, and proposed one way to address the tradeoff. Our results show promising signs for establishing trust in LLM outputs even if they become more capable than humans in the future. We hope to inspire future work on semi-supervised / unsupervised setups for improving human judge legibility with few or no ground truth labels.

## 7 Acknowledgements

We would like to thank Jeff Wu for valuable technical insights and discussions. We are grateful to Boaz Barak, Jeff Wu, Jenny Nitishinskaya, and John Schulman for helpful feedback on earlier drafts of this paper. We also thank the Platform team for infrastructure help. We thank Mati Roy, Spencer Papay as well as all contractors who contributed to the the human data collection effort.

## Appendix A Proof of Theorem 1 (Verifier-leading Stackelberg equilibrium is necessary and sufficient for completeness and soundness)

We first make a few more mild assumptions. We restrict $\mathcal{X}$ to be the set of inputs where $P_{X}$ has non-zero probability mass. We treat $\mathcal{X}$ as discrete for simplicity, although the same result can be extended to continuous domain using measure theory. We remind the reader that $x\in\mathcal{X}$ is the input, $v(x,z):\mathcal{X}\times\mathcal{Z}\rightarrow[0,1]$ is the verifier, $h(x),s(x):\mathcal{X}\rightarrow\mathcal{Z}$ are helpful and sneaky provers, and $\mathds{1}_{\text{correct}}\left({x,z}\right)\in\{0,1\}$ is the indicator for the correctness of solution $z$ given input $x$. We assume the hypothesis class $\mathcal{H}$ is the set of all deterministic mappings from $\mathcal{X}\rightarrow\mathcal{Z}$. We also assume that for any $x\in\mathcal{X}$, there exists any least one correct solution and one incorrect solution in $\mathcal{Z}$.

The verifier loss is

$$ $\displaystyle l_{V}=\frac{1}{2}\mathbb{E}_{x}{l(v(x,h(x)),\mathds{1}_{\text{ correct}}\left({x,h(x)}\right))}+\frac{1}{2}\mathbb{E}_{x}{l(v(x,s(x)),\mathds {1}_{\text{correct}}\left({x,s(x)}\right))}$ $$

where $l(v,c)$ is a loss function minimized if and only $v=f$ (we assume without loss of generality that $l(c,c)=0$). The prover reward is

$$ $\displaystyle R_{P}=\frac{1}{2}\mathbb{E}_{x}{r(v(x,h(x)),\mathds{1}_{\text{ correct}}\left({x,h(x)}\right))}+\frac{1}{2}\mathbb{E}_{x}{r(v(x,s(x)),1- \mathds{1}_{\text{correct}}\left({x,s(x)}\right))}$ $$

where $r(v,q)$ satisfies:

$$ $\displaystyle\forall v_{1},v_{2}\in[0,1]:r(v_{1},1)>r(v_{2},0),$ $\displaystyle\forall v_{1},v_{2}\in[0,1],v_{1}>v_{2}:r(v_{1},1)>r(v_{2},1).$ $$

Define the completeness and soundness properties as follows

$$ $\displaystyle\exists h\text{ s.t. }\forall x\in\mathcal{X},\mathds{1}_{\text{ correct}}\left({x,h(x)}\right)=1\text{ and }v(x,h(x))=1.$ $\displaystyle\forall s,\forall x\in\mathcal{X},x,\mathds{1}_{\text{correct}} \left({x,s(x)}\right)=0\implies v(x,s(x))=0.$ $$

We prove that in the PVG where verifier’s utility is $-l_{V}$ and the prover’s utility is $R_{P}$, the existence of a verifier-leading Stackelberg equilibrium $(v^{*},h^{*},s^{*})$ is necessary and sufficient for the completeness and soundness properties to hold for $(v^{*},h^{*})$.

###### Proof.

First, assuming that the completeness and soundness properties hold for $v^{*},h^{*}$. We construct $s^{*}$ as follows: For any $x$, let $s^{*}(x)$ be an arbitrary incorrect solution, i.e. $s^{*}(x)\in\{z\mid\mathds{1}_{\text{correct}}\left({x,z}\right)=0\}$. By the soundness property, we know that we will have $v^{*}(x,s^{*}(x))=0$ and $\mathds{1}_{\text{correct}}\left({x,s^{*}(x)}\right)=0$ for all $x$. We shall show that $(v^{*},h^{*},s^{*})$ is a verifier-leading Stackelberg equilibrium.
First, at $v=v^{*}$, the first term of $R_{P}$ is already maximized since

$$ $\displaystyle\frac{1}{2}\mathbb{E}_{x}{r(v^{*}(x,h^{*}(x)),\mathds{1}_{\text{ correct}}\left({x,h^{*}(x)}\right))}=\frac{1}{2}\mathbb{E}_{x}{r(1,1)}$ $$

The second term is also maximized since

$$ $\displaystyle\frac{1}{2}\mathbb{E}_{x}{r(v^{*}(x,s^{*}(x)),1-\mathds{1}_{\text {correct}}\left({x,s^{*}(x)}\right))}=\frac{1}{2}\mathbb{E}_{x}{r(0,1)}$ $$

and $r(v^{\prime},0)<r(0,1)$ for any $v^{\prime}\in[0,1]$ hence the provers have no incentive to change. For the verifier, it’s loss is at minimum since

$$ $\displaystyle l_{V}=\frac{1}{2}\mathbb{E}_{x}{l(1,1)}+\frac{1}{2}\mathbb{E}_{x }{l(0,0)}=0$ $$

so this is a Stackelberg equilibrium.

Next, assuming $(v^{*},h^{*},s^{*})$ is any verifier-leading Stackelberg equilibrium. We already know that the utility of the verifier is at its maximum at $-l_{v}(v^{*})=0$. Suppose the completeness property is not satisfied, which means

$$ $\displaystyle\exists x,\mathds{1}_{\text{correct}}\left({x,h^{*}(x)}\right)=0 \text{ or }v(x,h^{*}(x))=0.$ $$

Suppose it is the first case, i.e. $\exists x^{\prime}$, $\mathds{1}_{\text{correct}}\left({x^{\prime},h^{*}(x^{\prime})}\right)=0$. Then letting $h^{\prime}$ to be identical to $h^{*}$ except at $x^{\prime}$, where we pick an arbitrary correct solution $h^{\prime}(x^{\prime})\in\{z\mid\mathds{1}_{\text{correct}}\left({x^{\prime},z
}\right)=1\}$. Then we would have increased the first term of $R_{P}$ since

$$ $\displaystyle r(v^{*}(x^{\prime},h^{*}(x^{\prime})),\mathds{1}_{\text{correct} }\left({x,h^{*}(x^{\prime})}\right))=r(v^{*}(x^{\prime},h^{*}(x^{\prime})),0)< r(v^{*}(x^{\prime},h^{\prime}(x^{\prime})),1).$ $$

which contradicts Stackelberg equilibrium.
Suppose it is the second case, i.e. $\exists x^{\prime},v^{*}(x^{\prime},h^{*}(x^{\prime}))=0$ but $\mathds{1}_{\text{correct}}\left({x^{\prime},h^{*}(x^{\prime})}\right)=1$. Since $P_{X}$ has non-zero probability mass at $x^{\prime}$, $\mathbb{E}_{x}[l(v^{*}(x,h^{*}(x),\mathds{1}_{\text{correct}}\left({x,h^{*}(x)
}\right)]>0$ which contradicts $l_{v}(v^{*})=0$.

Suppose the soundness property is not satisfied, which means

$$ $\displaystyle\exists s^{\prime},x^{\prime}:\mathds{1}_{\text{correct}}\left({x ^{\prime},s^{\prime}(x^{\prime})}\right)=0\text{ and }v^{*}(x^{\prime},s^{ \prime}(x^{\prime}))>0.$ $$

Due to $l_{v}(v^{*})=0$, $s^{*}$ has to satisfy

$$ $\displaystyle\forall x,v^{*}(x,s^{*}(x))=\mathds{1}_{\text{correct}}\left({x,s ^{*}(x)}\right).$ $$

If $s^{*}(x^{\prime})$ is such that $\mathds{1}_{\text{correct}}\left({x^{\prime},s^{*}(x^{\prime})}\right)=v^{*}(x
^{\prime},s^{*}(x^{\prime}))=0$, we can modify $s^{*}$ so that it outputs the $s^{\prime}(x^{\prime})$ at $x=x^{\prime}$ and then we would have increased $R_{p}$ due to $r(v^{\prime},1)>r(0,1)$ when $v^{\prime}>0$. If $s^{*}(x^{\prime})$ is such that $\mathds{1}_{\text{correct}}\left({x^{\prime},s^{*}(x^{\prime})}\right)=v^{*}(x
^{\prime},s^{*}(x^{\prime}))=1$, switching to $s^{\prime}(x^{\prime})$ also increases $R_{p}$ due to $r(v^{\prime},1)>r(1,0)$ for any $v^{\prime}$. Both of those scenarios contradict the assumption that $s^{*}$ is at Stackelberg equilibrium.

We have proved by contradiction that $(v^{*},h^{*})$ from any verifier-leading Stackelberg equilibrium satisfies both completeness and soundness properties.
∎

###### Proof.

## Appendix B Samples from several experiments

Figure: Supplementary Figure S1: Learning from a binary grader leads to strong performance, but poor legibility. Example solutions from early (left, 3k steps) and late (right, 7k steps) in training.
Refer to caption: x10.png

Figure: Supplementary Figure S2: Four examples of incorrect solutions with high verifier score from different points during training. Flaws are highlighted in red.
Refer to caption: x11.png

## Appendix C Separation might inhibit progression of checkability training

A verifier trained to predict correctness of solutions might not in fact learn a generalizable algorithm for predicting correctness, if other attributes of the solutions are highly correlated with correctness and are easier to predict.

In our experiments, all training rounds of the verifier, except the very first one, contain correct and incorrect solutions produced by helpful and sneaky provers. Since our training incentivizes helpful prover’s solutions to be correct, and sneaky prover’s solutions to be incorrect, correctness of solutions in the verifier’s training data strongly correlates with which of the two provers produced that solution. If the helpful and sneaky provers produce solutions in different easily identifiable formats, and helpful solutions are mostly correct, while sneaky solutions are mostly incorrect, then training the verifier on the correctness signal will likely generalize to identify distinctive format features of the solutions produced by the helpful and sneaky provers.

Figure S3 presents evidence that in the early rounds of checkability training, helpful and sneaky provers are in fact easily separable based on easy to learn features, but grow less separable as the training progresses. For that figure, we trained a very small discriminator to predict whether a given sample was produced by the helpful or the sneaky prover on a small balanced dataset of helpful and sneaky solutions. We trained separate discriminators for checkpoints of the prover spaced every 400 optimization steps of training. The figure shows ROC AUC of that discriminator. In the first round, ROC AUC reaches close to 1 at the end of the round. For the last round, it stays close to 0.5 for the whole duration of the round.

Figure: Supplementary Figure S3: Evolution of separability of helpful and sneaky provers over the course of training. a When training with SRC reward, in early rounds the provers become easily separable after a short number of optimization steps. In later rounds of training it’s difficult for a small discriminator to tell helpful samples apart from sneaky ones. b When training with CGC reward, the helpful and sneaky provers remain highly separable throughout training.
Refer to caption: x12.png

We hypothesize that samples produced by the helpful and sneaky provers after they separate completely in a way that is easily learnable by very small verifiers (i.e. based on mostly surface level statistics of the solutions) are not useful for increasing the robustness of the verifier. As a consequence, when designing particular formulations of a Prover-Verifier Game, one has to pay attention to whether it in fact encourages early separation of the helpful and sneaky players.

## Appendix D When the verifier is too small or too large, checkability training is inhibited.

Figure: Supplementary Figure S4: A very small verifier makes training dynamics unstable and results in degenerate solutions. a Sample completion from round zero of legibility training with a very small verifier. b Average accuracy for the helpful (top) and sneaky (bottom) provers as a function of the completed fraction of each round.
Refer to caption: x13.png

Figure: Supplementary Figure S5: A verifier as large as the prover does not increase in robustness over rounds and results in degenerate solutions. a Sample completion from round zero of legibility training with a very small verifier. b Average accuracy for the helpful (top) and sneaky (bottom) provers as a function of the completed fraction of each round. c Median accuracy of time-constrained human contractors when evaluating solutions from the helpful prover at different rounds of checkability training. This plot is from a potentially flawed campaign (see Appendix I).
Refer to caption: x14.png

## Appendix E Additional evaluations for the goodharting baseline

Figure: Supplementary Figure S6: Test samples generated by provers at the end of three rounds of goodharting training do not have significant increase in human trainer accuracy across R0-2. This experiment uses a verifier roughly $10^{-3}$ of the prover size. This plot is from a potentially flawed campaign (see Appendix I).
Refer to caption: x15.png

Figure: (a) Verifier size $10^{-3}$
Refer to caption: x16.png

Figure: Supplementary Figure S8: Balanced best-of-$n$ for iterative goodharting training with verifier relative size $3\times 10^{-3}$. The solutions are current-round last-checkpoint prover samples balanced at 50% correct and 50% incorrect.
Refer to caption: x18.png

## Appendix F Validation with provers with no math-specific pretraining.

Figure: Supplementary Figure S9: When repeating our proposed checkability training with LLMs that have not been finetuned on math-specific text, the dynamics remain qualitatively unchanged.
Refer to caption: x19.png

## Appendix G System prompt

Figure: Supplementary Figure S10: System prompt provided to the honest and sneaky prover before being presented with a grade-school math problem. For the sneaky prover, we format maybe_dishonest_mode with MATH_DISHONEST_MODE_TEMPLATE.

## Appendix H Few-shot prompt

Figure: Supplementary Figure S11: Few-shot prompt we use to sample solutions from the initialization of the prover.

## Appendix I Details on the human legibility evaluation campaign

Our main human evaluation experiment is as follows. For the training shown in Figure 5, we sample the last checkpoint helpful prover solutions to the problems from the GSM test dataset. We also sample from the correctness-only baseline at training step 3k, 7k, as well as the few-shot prover initialization. We collect up to one correct and up to one incorrect sample from each prover and each problem, if possible (around one-third of the problems per round have either all correct or all incorrect solutions among 128 samples). We randomized assignment of those samples to 75 trainers (making sure each person see balanced correct vs. incorrect samples from each checkpoint), and asked them to judge the solution correctness within a 45-second time limit per problem. We excluded all problems that yielded only correct or only incorrect solutions. We also excluded four trainers whose performance was statistically indistinguishable from chance from the dataset. We collected 15983 datapoints. Each trainer spent a maximum of 4 hours working on the task to prevent learning and fatigue effects. The instructions are shown in Fig. S12 and Fig. S13 contains an example task. The trainers are compensated based on completion, and are not told whether they judged correctly.

We also had an earlier pilot campaign where the we showed sneaky solutions as well as samples from an Iterative Goodharting training to 10 trainers with 1 minute time limit (instead of 45 seconds) per task. In this pilot run, we showed solutions from earlier rounds to the trainers first (they judged the samples in the order of R0, R1, R2, etc.) across a span of one month, and hence we suspect that the data is affected by learning or fatigue effects. The only plots from this potentially flawed campaign are Fig. 7b, S5c and S6.

Figure: Supplementary Figure S12: Instructions shown to the human trainers.

Figure: Supplementary Figure S13: Example task for human evaluation.

## Peer Reviews

confidence: 4
contribution: 4
initial_rating: 6
presentation: 2
questions: - How are the synthetic data samples for GSM8k checked for correctness? Are they checked for correctness?
- Could the authors provide more details on the ‘flawed campaign’ regarding human annotations in their experiments?
- Risk of overfitting the prover and verifier to each other’s outputs: what happens if one uses different models? How does this then extend to other domains? Will the same amount of training resources be required for legibility in every domain or are there any generalization results that the authors could present?
- What issues related to the safety literature highlighted in the weaknesses section do the authors see arising out of their iterative training setup, and how can early work be done to prevent such alignment issues?
soundness: 3
strengths: - Overall, this is a strong paper presenting alignment research in a novel, viable, and important direction. It focuses explicitly on training setups that are understudied and demonstrates strong results around legibility.
- The paper rests on a strong theoretical foundation around prover-verifier games, takes into account how an adversarial prover might work, and presents important early results about points such as verifier sizes, iterative setups when it comes to training models towards legibility/alignment, etc.
- The paper addresses concerns such as reward hacking and provides a good amount of diversity around reward functions and how these could influence future research.
- The paper is open about its limitations and future work around unsupervised learning for tasks that lack ground truth labels.
summary: The paper presents work on an important direction in AI Alignment - making the outputs of highly capable LLMs legible to humans. It describes results on a setup consisting of iterative prover-verifier training which improves accuracy and legibility. It also analyzes training dynamics (e.g. impact of the verifier’s size on iterative training), rendering the paper overall quite impactful in terms of building systems that have outputs legible to human overseers.
weaknesses: - The paper conducts all experiments exclusively on GSM8k, where explanations can indeed be step by step while being natural. Moreover, all experiments are done on a single model type (GPT-4). This raises some concerns about the generalizability of the prover-verifier setup, especially to domains such as code generation, writing, etc. and settings with different base models.
- The iterative training process might lead to overfitting and the early stopping conditions don’t seem clear and generalizable. The prover and verifier could adapt to each other’s outputs, and given that there is no cross model testing, it’s difficult to make claims about generalization in this setting.
- Lack of experiments/comparison with existing work on Explainable AI. Work on multi-agent debate for safety/legibility [1] or other methods to improve legibility [2] are not compared against.
- The iterative training setup introduces risks such as reward hacking, deception, collusion, or steganography. The paper does not address concerns highlighted in alignment literature such as [3][4][5][6][7] that this work directly impacts. The verifier could be jailbroken by a strong prover with steganographic methods arising out of training, or models may converge to deceptive strategies that jointly lead to higher rewards. It would be important to discuss the paper’s results against such prior work in safety.
- There are some points which I have raised below in my questions, such as details on the flawed campaign for collecting human data or the accuracy of synthetic GSM8k data or early stopping conditions/hyperparameter tuning.


[1]Debating with More Persuasive LLMs Leads to More Truthful Answers

[2] Usable XAI: 10 Strategies Towards Exploiting Explainability in the LLM Era

[3] Deceptive Alignment Monitoring

[4] Preventing Language Models From Hiding Their Reasoning

[5] Secret Collusion Among Generative AI Agents

[6] AI Control: Improving Safety Despite Intentional Subversion

[7] AI deception: A survey of examples, risks, and potential solutions

---

confidence: 2
contribution: 3
initial_rating: 8
presentation: 4
questions: Claim about prior work: Figure 4 shows a drop in legibility due to optimization for correctness. Are the authors sure this phenomenon is novel? I cannot find anything right now, but I personally thought this was the case and already established somewhere.
soundness: 3
strengths: I find the experiments very well-motivated.   Prior papers in adjacent areas like debate focus on question-answering datasets;
but it is obvious that research on legibility of reasoning is much more important.

Although the GSM dataset is easy, this is the first paper in this direction, and honestly the experiments would have been a good contribution even if it was on a toy dataset. I also think human legibility studies are less likely to be misleading on this sort of dataset.

The paper is extremely well-written, and also proposes many interesting follow-up ideas. I am particularly interested in whether sneaky provers resulting from this sort of training are useful in other ways, for example, as model organisms for deception evals.
summary: This paper investigates the trade-off between performance and legibility in large language models (LLMs) solving  GSM8k augmented with 100k synthetic examples.
The authors find, via a human study, that RL training for correctness reduces legibility of the solutions.
To improve legibility, the papers propose a "checkability training" method, similar to “Learning to Give Checkable Answers with Prover-Verifier Games” (Anil et al., 2021), which is in turn inspired by prior research in interactive proofs and PAC learning.
This involves iterative training of small verifier models and larger "helpful" and "sneaky" prover models. 
Checkability training achieves a balance, resulting in more legible solutions at a modest cost to accuracy.
weaknesses: **Models:** My assessment of the paper is based on the assumption that it does not matter for the purpose of this conference that the models here never available to the public in any form.


In the interest of taking everything in good faith, I see two acceptable reasons for this:
-   there is no herd of similar models over a range of compute scales used in the paper; or
-   human studies had to start before models of similar capabilities were available to the public;

This also assumes that the models used in the paper are similar in all important ways to other LLMs that the research field is aware of. I am open to reducing my score to 6 if there is a reviewer consensus that there is no good reason to do this research on the models used in the paper.


**Ground truth answers:**
As mentioned in the paper, the rewards in checkability training require ground truth labels. Most of the important applications of this line of research will be in settings where there are no ground truth labels. Given that, I am uncertain whether the method in this paper will play a major role in long-term scalable oversight research.


**Technical details:** I believe the training described in the paper might be tricky to reproduce on a different suite of models, due to the lack of details about optimization, learning rates, and so on. Would the authors be interested in disclosing whether this sort of iterative training is difficult to set up correctly, or it worked on basicaly the first try?

---

confidence: 3
contribution: 2
initial_rating: 5
presentation: 2
questions: - Could the proposed prover-verifier training framework be adapted for complex, non-mathematical reasoning tasks such as legal or medical document analysis?
- What are the practical challenges in deploying this approach for real-time systems where rapid responses are required?
- How does the model handle ambiguous or contextually complex questions where the verifier might struggle to discern correctness?
- Would integrating human-in-the-loop feedback during training rounds enhance the verifiers' robustness and prover legibility further?
soundness: 2
strengths: - The paper presents an innovative adaptation of the Prover-Verifier Game to train LLMs for legibility.
- It includes both theoretical proofs and empirical studies showing the benefits of their method in improving solution checkability.
- The study extends beyond automated verification to demonstrate human evaluators' performance, indicating real-world applicability.
- The authors acknowledge trade-offs between optimizing for accuracy and maintaining human-legible outputs, highlighting practical insights for future applications.
summary: This paper investigates how to make outputs from large language models (LLMs) more legible and reliable through a method inspired by Prover-Verifier Games (PVG). The authors focus on the challenge of maintaining both correctness and legibility in outputs when solving grade-school math problems. The proposed iterative training algorithm trains a verifier to predict solution correctness and conditions, and provers to create either correct or subtly incorrect solutions. This approach enhances verifier robustness and human assessability of solutions over time.
weaknesses: - The study primarily focuses on grade-school math problems; exploring broader applications could demonstrate the method's generalizability.
- The paper could benefit from more discussion on integrating this training into existing LLM frameworks and the computational resources required.

---

confidence: 4
contribution: 2
initial_rating: 5
presentation: 3
questions: Please refer to the weaknesses. Clarifications and responses to each of them would help, especially with regards to the technical contributions, lack of empirical results on OOD and other datasets which is a major flaw, clarity on definition of legibility, and potential design flaws of the human trials which are critical for the main claims of the paper.
soundness: 2
strengths: - The paper raises an interesting question of whether there is a trade-off between performance and legibility of LLM output.
- It also proposes a conceptually simple actor-critic approach of training an LLM for legibility, by iteratively training the prover model and small verifier model, the latter providing a proxy for time-constrained human for evaluating legibility.
summary: This paper tackles the problem of making LLMs generate reasoning output that is clear and easy to check (legibility), and proposes a training algorithm that iteratively trains a prover model (that generates reasoning output) and verifier model (that verifies whether a reasoning output is correct) to produce  (1) more legible solutions, (2) robust verifiers, and (3) 'sneaky' provers that can generate subtle flaws in reasoning.
weaknesses: - The comparisons to related works are relatively cursory. It would be beneficial to provide more detailed elaboration on the differences between other related works and technical contribution of this work, such as:

	○ actor-critic frameworks on reasoning and planning tasks that also involve training of both models, 

	○ how the notion of legibility is significantly different from other RLHF works where legibility would be a key implicit factor for human preference already by default, 

	○ More detailed and technical elaboration on how this work relates to the larger body of work on explainability, beyond what the authors have described as "allowing legibility to emerge naturally", among others

- The timed human evaluation trials have a very short time-window evaluation of 45 seconds, with trial length of up to 4 hours. Details of the evaluation would be important in assessing its accuracy, especially as the authors pointed out in the main paper, the study may have potential design flaws -- information from the appendix and additional details not included should be shifted to the main paper if space permits. 

	○ For example, the 45s limit significantly disadvantages longer responses even if they may be clearer or more understandable to humans -- an ablation controlling for length would be very useful.

	○ Also, details on whether there are any systemic trends of human evaluation over the trial time, similarity of questions provided during the trial, and distribution of questions shown during the trial, would be useful even if only in the appendix.
	
- The empirical evaluations are done only on 1 dataset. Especially for RL studies such as this, it would be important to assess whether the results are due to extensive tuning/fitting to this dataset or whether the method can be extended to other datasets

	○ This should include out-of-distribution results especially for claims regarding the better performance and robustness in verifiers, and legibility of provers, in case the main results of this results are specifically overfitted to just this dataset.

- The notion of legibility is vaguely defined, based primarily on the time-constrained human evaluator trials that the authors pointed out may have design flaws. A more careful design of these trials would significantly improve the paper. 

	○ For example, there could be further information on why the humans may find one solution clearer than the other. This would provide more details on the characteristics that are most influential, (e.g., 'I just don't have enough time to read it', ' the answers are more spaced out' etc) which may not even require RL training to implement in the future for better legibility.

Meta-review: This paper presented a new direction "legibility", clear and easy to check as one of the alignment goals. The authors proposed
a training algorithm inspired by Prover-Verifier Game by training small verifiers to improve the legibility of the LLM outputs.

Strength:
1. An potentially very important alignment aspect: legibility.
2. A novel method to improve the legibility

Weakness:
Though the work is very interesting, it is a bit preliminary in terms of 1) experimental validation is mainly on GSM8k. So the generalization of the method is difficult to known. The authors provided some argument along this line, though it doesn't seem to be sufficient to address the concern. 2) The definition of `legibility` is not very formal and not adequately ablated against other confounding factors, mostly argued by reviewer 5yX2.

Overall, I believe this could be an important paper, though the current form is a bit preliminary and I would encourage the authors to take into the comments to make this paper stronger.

Decision: Reject