PaperlayerView exact revision on arXiv

Source-linked AI summary

Prover-Verifier Games improve legibility of LLM outputs

Jan Hendrik Kirchner, Yining Chen, Harri Edwards, Jan Leike, Nat McAleese, Yuri Burda

arXiv:2407.13692v2cs.CL

TL;DR

The paper asks whether making capable LLM outputs checkable by smaller LLMs can improve their legibility to humans, which matters for judging trust in system outputs. It proposes iterative checkability training and finds a better performance–legibility trade-off and transfer of legibility to human evaluation.

  • Problem

    The paper asks whether making capable LLM outputs checkable by smaller LLMs can improve their legibility to humans, an important consideration for trusting system outputs.

    Source: §1 · p. 1

  • Method

    The paper proposes iterative checkability training inspired by the Prover-Verifier Game to produce solutions that smaller verifiers can check.

    Source: §1 · pp. 1–2

  • Results

    Checkability training achieved a better performance–legibility trade-off than correctness-only optimization, and legibility to smaller LLMs transferred to human evaluation.

    Source: §1 · p. 3

  • Takeaways & Limitations

    Checkability training is a promising candidate for scalable oversight when future LLMs may exceed human capabilities.

    Source: §1 · p. 3

    The setup requires ground-truth answers, and the paper does not study out-of-domain generalization because it trains on only one dataset.

    Source: §6.1 · p. 15

Abstract

from arXiv · show

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

The paper studies whether training LLM provers to produce solutions checkable by smaller verifiers can make their outputs more legible to humans. Its checkability training aims to balance solution correctness with legibility, and the reported findings indicate that legibility to smaller verifiers transfers to human evaluation.

1 INTRODUCTION

  • The study tests smaller LLM verifiers as a scalable proxy for human legibility, motivated by their use in judging LLM outputs and the possibility of varying the prover–verifier capability gap.The authors present verifier checkability as a complementary approach to direct human-feedback optimization and as potentially useful when human feedback for advanced systems is limited.Source: §1 · p. 1
  • Correctness-only optimization achieves high math performance but produces solutions that are difficult for humans to evaluate; checkability training retains legibility with intermediate accuracy.The paper describes this as a legibility tax: checkability training has lower test performance than correctness-only optimization, while helpful-prover pass rates improve in later rounds.Source: Figure 1 · p. 2, §1 · p. 3
  • The paper defines relaxed checkability through high helpful-solution pass rates and verifier recall, alongside low false-positive rates on adversarial inputs produced through limited optimization.These relaxed completeness and soundness criteria reflect that models and humans in informal domains cannot be expected to be perfectly complete or sound.Source: §1 · p. 2
  • Checkability training alternates supervised verifier training on balanced samples with reinforcement-learning optimization of helpful and sneaky provers for convincing, correct or incorrect solutions, respectively.The verifier predicts solution correctness; the prover’s reward combines correctness and verifier acceptance, with the role sampled uniformly.Source: §1 · pp. 2–3
  • Verifier soundness increases over training, sneaky solutions become harder for humans to detect, and helpful solutions achieve higher pass rates and are judged correctly more often at high rounds.The paper reports that human accuracy decreases on sneaky solutions and increases on helpful-prover solutions; it concludes that legibility to smaller LLMs seems to transfer to humans.Source: §1 · p. 3

2 RELATED WORK

The paper positions checkability training among prover-verifier games and scalable oversight, distinguishing it through learned verification of solution correctness and human-checkable reasoning in a capability-gap setting.

Computational complexity

  • Unlike prior prover-verifier work, this study trains a learned verifier to judge solution correctness under a capability constraint and empirically studies checkability at scale.Prior work includes interactive proofs for PAC verification (Mutreja and Shafer, 2023), prover-verifier games for alignment (Anil et al., 2021), interpretability (Wäldchen et al., 2024), and LLM provers against a manually defined verifier (Amit et al., 2024).Source: §2 · p. 4

Scalable oversight

  • Unlike debate and consultancy work often using fictional-story question answering, this setup has a single judge view one prover’s answer in a more challenging reasoning domain with a capability gap.The setup assumes ground-truth labels for improving both provers and the verifier, and resembles consultancy because the judge does not see both sides simultaneously.Source: §2 · p. 4

Chain-of-Thought

  • Checkability training does not enforce a structured chain of thought or use step-wise human supervision; it relies on final-answer supervision, with legibility emerging from training dynamics.The method is presented as general for domains with ground-truth labels.Source: §2 · p. 4

Explainability and legibility as complementary properties

  • Explainability accounts for a prover’s reasoning whether correct or not, whereas legibility concerns whether people can verify solution correctness from coherent, accessible outputs.The two properties can occur independently.Source: §2 · p. 4

Adversarial Robustness

  • Checkability training can be viewed as adversarial training on the verifier, and its robustness transfers to test attacks different from the training attacks.The passage notes that perfect verifier robustness is unrealistic for both models and humans.Source: §2 · p. 5

Legibility in concrete applications

  • This study measures human legibility as time-limited accuracy in judging solution correctness, one measure among broader applications such as interpreting robotic intent or tracing code execution.Prior coding measures also include finding bugs and summarizing goals.Source: §2 · p. 5

3 SETUP

The setup formalizes checkability as correct, convincing helpful solutions and rejection of incorrect solutions from a same-family adversarial prover, then connects this objective to a verifier-led game. The training procedure approximates these properties with iterative verifier and prover optimization, using role-conditioned rewards.

3.1 FROM CHECKABILITY TO THE PROVER-VERIFIER GAME

  • Checkability requires a helpful prover to produce correct solutions accepted by the verifier, while no incorrect solution from a same-family sneaky prover is accepted.The formal definition expresses these requirements as completeness and soundness.Source: §3.1 · p. 6
  • In practice, checkability is approximate: helpful solutions must be correct with high probability, while verifiers face limited black-box attacks near the honest prover.The sneaky prover is restricted to the helpful prover’s model family; neural-network training seeks an approximate local equilibrium, without formal guarantees of finding one efficiently.Source: §3.1 · pp. 6–7
  • With H containing all deterministic mappings from X to Z, completeness and soundness hold if and only if the game has a verifier-leading Stackelberg equilibrium.The verifier leads, anticipating the prover’s best response; the theorem’s equivalence assumes the stated hypothesis class.Source: §3.1 · p. 7

3.2 CHECKABILITY TRAINING

  • Training alternates verifier-first rounds and PPO prover updates; verifiers rank correct solutions above incorrect ones with a regularized Bradley–Terry comparison loss.Verifier-training samples mix the base and previous-round provers, balanced for correct and incorrect solutions; the prover reward combines verifier score with role-alignment.Source: §3.2 · pp. 7–8
  • Signed Relative Convincingness rewards role-aligned solutions by their batch-centered verifier scores, but assigns below-average-scoring solutions −1 to prioritize convincingness.This variant satisfies the stated reward assumptions for above-average scores and is reported as practically useful for convergence.Source: §3.2 · p. 8
  • Correctness-Gated Convincingness performs worse than Signed Relative Convincingness, while Iterative Goodharting rewards only convincingness without role alignment.The CGC reward uses a low constant for role-misaligned outputs; Iterative Goodharting applies the verifier score to both helpful and sneaky provers.Source: §3.2 · p. 8

4 RESULTS

Across training rounds, checkability training produces verifiers and helpful and sneaky provers evaluated for robustness and legibility. Compared with correctness-only optimization, it improves the helpful prover’s accuracy while preserving human legibility.

4.1 BASELINE: DIRECT OPTIMIZATION FOR CORRECTNESS

  • Correctness-only optimization achieves strong math performance but produces increasingly long, unintelligible solutions that time-constrained humans struggle to evaluate.In a 45-second-per-solution task, human accuracy and speed deteriorated on trained-prover solutions, especially for problems the model could not reliably solve.Source: §4.1 · pp. 8–9, Figure 4 · p. 9

4.2 DYNAMICS OF CHECKABILITY TRAINING

  • Within rounds, both provers improve their convincingness to the verifier, but only the helpful prover largely becomes more correct; the sneaky prover eventually produces incorrect solutions matching or surpassing early helpful-prover verifier scores.Dynamics remained largely unchanged for verifier compute from 10−3 to 10−1.8 of prover compute, but 10−4 verifiers were unstable and verifiers matching prover compute produced strong yet poorly legible provers; the authors note hyperparameters may contribute.Source: §4.2 · pp. 9–10, Figure 5 · p. 10

4.3.1 THE VERIFIER BECOMES MORE ROBUST THROUGHOUT CHECKABILITY TRAINING

  • Attacks took more steps to exploit verifiers across rounds; none exploited 10−2-size verifiers beyond round 0 within 8k RL steps, while 10−3-size verifiers remained exploitable through round 4.Balanced best-of-n accuracy for current-round helpful prover–verifier pairs also increased at higher rounds, controlling for pass rates. The attacks are not exhaustive, so robustness to all sneaky provers remains unestablished.Source: Figure 6 · p. 11, §4.3.1 · pp. 11–12

4.3.2 THE SNEAKY PROVER BECOMES INCREASINGLY SUBTLE THROUGHOUT CHECKABILITY TRAINING

4.3.3 THE HELPFUL PROVER BECOMES INCREASINGLY LEGIBLE THROUGHOUT CHECKABILITY TRAINING

  • Across rounds, the helpful prover’s accuracy and human-evaluation accuracy improve while evaluation time falls; at training’s end it matches initialization legibility but trails correctness-only performance.Its solutions also remain coherent throughout training, unlike those from correctness-only optimization.Source: Figure 8 · p. 13, §4.3.3 · p. 13

5 ALTERNATIVE REWARDS

The section evaluates CGC and iterative goodharting as alternative training rewards: CGC has worse training dynamics, while goodharting improves verifier robustness to some extent but does not establish improved human legibility.

5.1 CHECKABILITY TRAINING WITH THE CORRECTNESS-GATED CONVINCINGNESS (CGC) REWARD

  • CGC training did not consistently require more RL steps across rounds; sneaky accuracy fell quickly while convincingness rose more slowly than under SRC.CGC rewards correctness for helpful outputs and incorrectness for sneaky outputs, assigning a constant penalty otherwise; human evaluation was not performed because of the poor dynamics.Source: Figure 9 · p. 14, §5.1 · p. 14
  • CGC serves as a strong alternative-reward attack for evaluating the robustness of verifiers trained with SRC.Source: §5.1 · p. 14

5.2 ITERATIVE GOODHARTING TRAINING

  • In iterative goodharting, an unassigned-role prover maximizes verifier score, and its correct and incorrect samples are used to train the verifier in subsequent rounds.Each round uses PPO until prover training accuracy drops below 0.2, then adds balanced correct and incorrect samples from prover checkpoints while keeping samples per problem constant.Source: §5.2 · pp. 14–15
  • Across verifier sizes 10^-4 to 100, overoptimization generally took longer; medium verifiers (3 × 10^-3 ∼10^-2) benefited most, while smaller and largest verifiers benefited less.Robustness under SRC and CGC attacks increased sometimes but not always; balanced best-of-n robustness increased.Source: Figure 10 · p. 15, §5.2 · p. 15
  • Human judge accuracy showed no significant difference across goodharting rounds, so the results do not establish improved human legibility.The cited human study was a pilot with design flaws; the authors conclude that goodharting increases verifier soundness to some extent but lack sufficient evidence for improved human legibility.Source: §5.2 · p. 15

6 DISCUSSION

The discussion frames checkability training as a promising approach to legibility while emphasizing limits in its domains, data, and training setup. It identifies unsupervised signals, more legible explanations, interactive games, and systematic human evaluation as directions for future work.

6.1 LIMITATIONS

  • The approach is limited to domains with natural-language justifications and a finite set of final answer labels; the study used the relatively easy, standardized GSM dataset.The authors propose extending the framework to harder math, coding, and fuzzier domains such as human preference data (Ouyang et al., 2022).Source: §6.1 · pp. 15–16
  • The setup requires ground-truth answers, and the paper studies no out-of-domain generalization; training across diverse labeled domains could potentially support transfer to unlabeled domains (Burns et al., 2023).Where trusted correctness labels are unavailable, future work could explore unsupervised signals such as consistency (Wang et al., 2023) and convincingness (Khan et al., 2024).Source: §6.1 · pp. 15–16, §6.2 · p. 16
  • Training chain-of-thoughts for legibility may limit prover accuracy, so the measured accuracy-legibility tradeoff could be overly pessimistic.A proposed alternative is to first maximize answer accuracy, then train a second model to turn the reasoning into a legible justification; the paper notes no principled early-stopping method for legibility.Source: §6.1 · p. 16
  • The experiments used a math-finetuned prover initialization containing some GSM training data, though initialization from a base model produced qualitatively similar training dynamics.Training schemes also used different stopping criteria, with no qualitative difference observed between early-stopped and fixed-step rounds; hyperparameters were not thoroughly tuned across schemes.Source: §6.1 · p. 16

6.2 FUTURE WORK

  • A future direction is translating an illegible solution into a legible proof, which may avoid limiting prover performance or exacerbate deceptive alignment through optimization pressure on the chain-of-thought.The authors suggest converting the model’s scratch-space reasoning into a well-written proof (Denison et al., 2024; Hubinger et al., 2024).Source: §6.2 · p. 16
  • Interactive, multi-round verifier-prover games could improve sample efficiency, and a proposed mind-changing game alternates attempts to convince the verifier of either binary outcome.The proposal is compared to market-making.Source: §6.2 · pp. 16–17
  • Because the paper mainly studies legibility to smaller models, future work should more systematically examine what assistance helps humans judge large-model solutions.The authors expect more extensive human studies to be fruitful.Source: §6.2 · p. 17

6.3 CONCLUSION

  • The paper presents a tension between model performance and solution legibility in grade-school math, and proposes an approach to address it.The authors hope this work encourages semi-supervised or unsupervised methods for improving human judge legibility when ground-truth labels are scarce or unavailable.Source: §6.3 · p. 17

PROOF OF THEOREM 1 (VERIFIER-LEADING STACKELBERG EQUILIBRIUM IS NECESSARY AND SUFFICIENT FOR COMPLETENESS AND SOUNDNESS)

Under the stated assumptions, a verifier-leading Stackelberg equilibrium exists if and only if its verifier and helpful prover satisfy completeness and soundness.

PROOF OF THEOREM 1 (VERIFIER-LEADING STACKELBERG EQUILIBRIUM IS NECESSARY AND SUFFICIENT FOR COMPLETENESS AND SOUNDNESS)

  • The proof assumes discrete positive-mass inputs, deterministic mappings as the prover hypothesis class, and at least one correct and incorrect solution per input.The verifier loss is minimized only by matching correctness, and the reward favors a correct label over an incorrect one and higher verifier scores for correct solutions.Source: PROOF OF THEOREM 1 (VERIFIER-LEADING… · p. 21
  • A verifier-leading Stackelberg equilibrium exists exactly when its verifier and helpful prover satisfy both completeness and soundness.Completeness requires some helpful prover to give every input a correct solution accepted with score 1; soundness requires every incorrect sneaky solution to receive score 0.Source: PROOF OF THEOREM 1 (VERIFIER-LEADING… · pp. 21–22
  • If completeness and soundness hold, choosing any incorrect solution for each sneaky-prover output makes the prover incentives and verifier loss consistent with equilibrium.The proof shows the helpful prover’s correct accepted solutions and the sneaky prover’s incorrect rejected solutions maximize their respective rewards, while the verifier’s loss is minimal.Source: PROOF OF THEOREM 1 (VERIFIER-LEADING… · p. 21
  • At any equilibrium, an incorrect helpful output could be replaced to increase prover reward, while a correct helpful output scored 0 would contradict the verifier’s zero loss.These deviations establish completeness for the helpful prover.Source: PROOF OF THEOREM 1 (VERIFIER-LEADING… · pp. 21–22
  • If an incorrect sneaky output receives a positive score, changing the sneaky prover’s output to it can increase reward, contradicting equilibrium and establishing soundness.The proof considers whether the current sneaky output is incorrectly scored 0 or correctly scored 1; in either case, switching to the positively scored incorrect output is profitable.Source: PROOF OF THEOREM 1 (VERIFIER-LEADING… · p. 22

B SAMPLES FROM SEVERAL EXPERIMENTS

The figures provide examples of strong performance with poor legibility and of incorrect solutions that receive high verifier scores.

B SAMPLES FROM SEVERAL EXPERIMENTS

  • At 3k and 7k training steps, Supplementary Figure S1 shows that learning from a binary grader leads to strong performance but poor legibility.The figure contrasts example solutions from early and late training.Source: Figure S1 · p. 23
  • Four examples in Supplementary Figure S2 show incorrect solutions with high verifier scores from different points during training, with flaws highlighted in red.Source: Figure S2 · p. 24

C SEPARATION MIGHT INHIBIT PROGRESSION OF CHECKABILITY TRAINING

Helpful and sneaky provers can become distinguishable through easy-to-learn features, allowing verifiers to exploit format cues rather than learn generalizable correctness prediction. The authors hypothesize that this separation can inhibit verifier robustness and caution that game formulations should avoid encouraging early separation.

C SEPARATION MIGHT INHIBIT PROGRESSION OF CHECKABILITY TRAINING

  • Because correctness correlates with which prover produced a solution, a verifier may use easily identifiable format features instead of learning a generalizable correctness algorithm.Helpful solutions are incentivized to be correct and sneaky solutions to be incorrect; this correlation applies to verifier training rounds after the first.Source: C SEPARATION MIGHT INHIBIT PROGRESSION… · p. 25
  • Under SRC reward, helpful and sneaky provers become easily separable early, but grow less separable as training progresses; under CGC reward, they remain highly separable.A small discriminator’s ROC AUC reaches close to 1 by the end of the first round and stays close to 0.5 throughout the last round.Source: Figure S3 · p. 25, C SEPARATION MIGHT INHIBIT PROGRESSION… · p. 25
  • The authors hypothesize that solutions from completely separated provers, distinguishable by small verifiers through surface-level statistics, do not improve verifier robustness.They advise checking whether a particular Prover-Verifier Game formulation encourages early separation of the helpful and sneaky players.Source: C SEPARATION MIGHT INHIBIT PROGRESSION… · p. 25

D WHEN THE VERIFIER IS TOO SMALL OR TOO LARGE, CHECKABILITY TRAINING IS INHIBITED.

Checkability training is inhibited when the verifier is too small or too large: very small verifiers destabilize training, while verifiers as large as the prover fail to gain robustness over rounds.

D WHEN THE VERIFIER IS TOO SMALL OR TOO LARGE, CHECKABILITY TRAINING IS INHIBITED.

  • A very small verifier makes training dynamics unstable and leads to degenerate solutions.Supplementary Figure S4 also plots helpful and sneaky prover accuracy across training rounds.Source: Figure S4 · p. 26
  • A verifier as large as the prover does not become more robust over rounds and leads to degenerate solutions.Supplementary Figure S5 also includes time-constrained human evaluations, which the caption says come from a potentially flawed campaign.Source: Figure S5 · p. 27

E ADDITIONAL EVALUATIONS FOR THE GOODHARTING BASELINE

Additional evaluations of the goodharting baseline cover human trainer accuracy, iterative attacker performance, and balanced best-of-n samples.

E ADDITIONAL EVALUATIONS FOR THE GOODHARTING BASELINE

  • Test samples from provers trained through three rounds of goodharting showed no significant increase in human trainer accuracy across R0–2.The experiment used a verifier roughly 10^-3 the prover’s size and came from a potentially flawed campaign.Source: Figure S6 · p. 28
  • Iterative goodharting evaluations measured RL steps until the attacker matched the prover’s verifier score while reaching 95% incorrect, using SRC or CGC rewards.The verifier relative sizes were 10^-3 and 3 × 10^-3.Source: Figure S7 · p. 28
  • Balanced best-of-n evaluations used current-round last-checkpoint prover samples balanced at 50% correct and 50% incorrect, with verifier relative size 3 × 10^-3.Source: Figure S8 · p. 29

F VALIDATION WITH PROVERS WITH NO MATH-SPECIFIC PRETRAINING. · G SYSTEM PROMPT · H FEW-SHOT PROMPT

The appendices report that checkability-training dynamics remain qualitatively unchanged without math-specific pretraining and document the prover system and initialization prompts.

F VALIDATION WITH PROVERS WITH NO MATH-SPECIFIC PRETRAINING.

  • Checkability-training dynamics remain qualitatively unchanged with LLMs not finetuned on math-specific text.This result comes from repeating the proposed training with those LLMs.Source: Figure S9 · p. 30

G SYSTEM PROMPT

  • The system prompt is provided to both honest and sneaky provers before they receive a grade-school math problem.Source: Figure S10 · p. 31
  • For the sneaky prover, the system prompt formats maybe_dishonest_mode with MATH_DISHONEST_MODE_TEMPLATE.Source: Figure S10 · p. 31

H FEW-SHOT PROMPT

  • A few-shot prompt is used to sample solutions from the prover initialization.Source: Figure S11 · p. 32

I DETAILS ON THE HUMAN LEGIBILITY EVALUATION CAMPAIGN

The human evaluation campaign tested whether people could judge solution correctness under time limits, using helpful-prover and baseline samples. An earlier pilot included sneaky and Iterative Goodharting solutions but may have been affected by learning or fatigue.

Human legibility evaluation campaign

  • The main evaluation randomized GSM test-problem solutions from helpful-prover checkpoints, a correctness-only baseline, and few-shot initialization across 75 trainers.Each trainer judged correctness within 45 seconds per problem; samples included up to one correct and one incorrect solution per prover and problem, when available.Source: I DETAILS ON THE HUMAN LEGIBILITY… · p. 33
  • After excluding problems with only correct or only incorrect samples and four trainers performing statistically indistinguishably from chance, the campaign collected 15,983 datapoints.Each trainer spent at most four hours on the task to limit learning and fatigue effects.Source: I DETAILS ON THE HUMAN LEGIBILITY… · p. 33
  • An earlier pilot showed sneaky and Iterative Goodharting solutions to 10 trainers, but its sequential presentation over a month may have introduced learning or fatigue effects.Tasks had a one-minute limit; only Figures 7b, S5c, and S6 report results from this potentially flawed campaign.Source: I DETAILS ON THE HUMAN LEGIBILITY… · p. 33

Related papers

Loading 2407.13692v2…