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

LLM solutions optimized only for correctness can become difficult for humans to check, motivating methods that improve output legibility. The paper trains verifiers and helpful or sneaky provers in an iterative prover-verifier game, finding better performance-legibility trade-offs and transfer of verifier-facing legibility to humans. These results support checkability training as a possible approach to scalable oversight, subject to reliance on ground-truth answers and the paper’s potentially pessimistic accuracy-legibility measurement.

  • Problem

    The paper asks whether capable LLMs can produce Chain-of-Thought solutions that smaller LLM verifiers and humans can check, because correctness-only optimization can make solutions difficult for time-constrained humans to evaluate.

  • Method

    The paper iteratively trains small verifiers and helpful or sneaky provers, rewarding verifier-accepted correct or incorrect solutions while using known ground-truth math answers.

  • Results

    Checkability training retains legibility while achieving decent performance, with increasing verifier soundness, helpful-prover accuracy, and transfer of legibility to human judgments.

  • Takeaways & Limitations

    Training larger provers to be checkable by smaller verifiers is a plausible practical avenue for making outputs of potentially superhuman models more legible to humans.

  • Takeaways & Limitations

    The setup requires ground-truth answers and studies only one dataset, so its relevance to domains where labels are difficult or expensive and its out-of-domain generalization remain uncertain.

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 asks whether capable LLM outputs can be made more legible to humans by training larger provers to produce solutions checkable by smaller verifiers. It proposes an iterative prover-verifier procedure and finds improved performance-legibility trade-offs alongside increasing verifier soundness and human-relevant legibility.

  • Method: Checkability training alternates verifier and helpful/sneaky prover optimization to produce legible provers and robust verifiers on grade-school math problems.The verifier predicts solution correctness, while helpful and sneaky provers are rewarded for convincing correct and incorrect solutions, respectively.
  • Motivation and problem: Correctness-only reinforcement learning achieves high math performance but produces solutions that time-constrained humans find difficult to evaluate.These solutions differ substantially from human-written solutions.
  • Main findings: Checkability training retains legibility while achieving lower performance than correctness-only optimization, partially closing the gap as helpful-prover pass rates improve in later rounds.The resulting performance-legibility trade-off constitutes a legibility tax.
  • Main findings: Verifier soundness increases across training rounds, measured by resistance to sneaky-only attacks and balanced best-of-n accuracy.The training uses relaxed rather than perfect notions of completeness and soundness in this informal domain.
  • Human legibility: Sneaky solutions develop subtler flaws while helpful solutions become easier for human trainers to judge correctly at high training rounds.GPT-4 stepwise-correctness judgments increase for sneaky solutions, whereas human accuracy on them decreases; human accuracy on helpful solutions increases.
  • Implications: Legibility to smaller verifiers transfers to humans: solutions harder for verifiers to detect or easier for them to accept are correspondingly harder or easier for humans to judge.The authors identify prover-verifier games as a promising candidate for scalable oversight of potentially superhuman models.

2 RELATED WORK

Related work connects this study to interactive verification, scalable oversight, Chain-of-Thought reasoning, explainability, adversarial robustness, and application-specific notions of legibility. The paper distinguishes legibility of outputs for correctness checking from explanations of how a model reasoned.

  • Verification and prover-verifier games: Prover-verifier games connect to interactive proofs and PAC verification, while this work constrains verifier capability rather than data availability.Prior work also connected prover-verifier games to alignment and studied related toy or interpretability settings.
  • Scalable oversight: The paper places checkability training within scalable oversight methods that rely on discrimination being easier than generation, including critiques and debate.Related work includes negative results for improving time-limited human judge accuracy through human debate.
  • Chain-of-Thought: Chain-of-Thought prompting can improve accuracy and provide natural justifications, but CoTs are not guaranteed to be legible without additional training.Prior work has guided CoT structure through decomposition, recursive summarization, and symbolic reasoning.
  • Explainability and legibility: Legibility differs from explainability: legibility concerns whether an output can be checked as correct, whereas explainability concerns an account of the prover’s reasoning.The paper notes that explanations can be arbitrarily complex, while legibility requires coherent and human-accessible outputs.
  • Applications and robustness: Legibility has been studied across robotics and coding, while this paper measures human legibility through accuracy when judging solution correctness.Related adversarial-robustness work motivates attention to attacks against learned systems, including language-model jailbreaks.

3 SETUP

The setup defines checkability through correct, convincing helpful solutions and rejection of incorrect adversarial solutions, then instantiates iterative verifier–prover training for grade-school math.

  • 3 SETUP: The empirical setup models a prover that proposes solutions and a verifier that scores their answer correctness, using a SymPy grader on grade-school math problems.The verifier output is called the convincingness score, while correctness is determined against known ground-truth answers.
  • 3.1 FROM CHECKABILITY TO THE PROVER-VERIFIER GAME: Checkability requires helpful provers to generate correct solutions accepted by the verifier and sneaky provers to generate incorrect solutions rejected by it.The empirical definition relaxes these requirements to high helpful-sample correctness and robustness against limited attacks from the same model family.
  • 3.2 CHECKABILITY TRAINING: Checkability training uses a role-conditioned prover with helpful and sneaky modes, jointly optimized against a verifier in an iterative prover-verifier game.Verifier training precedes prover training in each round, and later rounds incorporate solutions from previous provers into the verifier’s sampling mixture.
  • 3.1 FROM CHECKABILITY TO THE PROVER-VERIFIER GAME: The paper connects verifier-leading Stackelberg equilibria to completeness and soundness, establishing their equivalence under deterministic unrestricted provers.The verifier commits first, the prover responds with a best response, and neither player benefits from changing strategy at equilibrium.
  • 3.1 FROM CHECKABILITY TO THE PROVER-VERIFIER GAME: The empirical setup only approximates the theory because LLMs are probabilistic, their hypothesis class is restricted, and efficient equilibrium-finding lacks formal guarantees.The authors use coordinate descent to seek an approximate local equilibrium in nonconvex neural networks.
  • 3.2 CHECKABILITY TRAINING: The verifier ranks correct solutions above incorrect ones with a Bradley–Terry comparison objective plus regularization, while provers receive role- and verifier-dependent rewards.The score function is real-valued rather than restricted to [0, 1], and the study evaluates three reward variants, including Signed Relative Convincingness.
  • 3.2 CHECKABILITY TRAINING: The Correctness-Gated Convincingness reward empirically produces worse training dynamics than the Signed Relative Convincingness reward.This variant assigns a low constant reward to role-misaligned solutions; the experiments used V0 = -2.

4 RESULTS

Correctness-only training produces high-performing but unintelligible solutions that time-constrained humans struggle to evaluate, whereas checkability training improves the helpful prover’s performance-legibility trade-off. Across training, verifier robustness and helpful-prover legibility increase, but sneaky provers learn subtler flaws that humans increasingly miss.

  • 4.1 BASELINE: DIRECT OPTIMIZATION FOR CORRECTNESS: Correctness-only reinforcement learning achieves strong math performance but produces increasingly long and unintelligible solutions that time-constrained humans struggle to evaluate.Human evaluation accuracy and speed deteriorate as training progresses, especially on questions the model cannot reliably solve.
  • 4.2 DYNAMICS OF CHECKABILITY TRAINING: Checkability training becomes unstable with verifiers far smaller than or comparable in size to the prover, producing either weak, illegible provers or strong but poorly legible ones.The authors cannot exclude non-optimal hyperparameters and suspect capability mismatches create fundamental verification difficulties.
  • 4.2 DYNAMICS OF CHECKABILITY TRAINING: Across checkability-training rounds, helpful provers become increasingly correct while sneaky provers struggle to produce incorrect solutions that remain convincing to the verifier.Both provers improve their verifier convincingness within rounds, but sneaky incorrect solutions eventually match or exceed helpful-correct verifier scores; helpful performance can dip at round ends, potentially from weight sharing.
  • 4.3.1 THE VERIFIER BECOMES MORE ROBUST THROUGHOUT CHECKABILITY TRAINING: Verifier robustness increases across rounds: adversaries require more steps to find exploits, and balanced best-of-n accuracy improves for later verifier-prover pairs.Larger verifiers are harder to exploit; however, the attack suite is incomplete and cannot establish robustness to all sneaky provers.
  • 4.3.2 THE SNEAKY PROVER BECOMES INCREASINGLY SUBTLE THROUGHOUT CHECKABILITY TRAINING: Later sneaky solutions contain more localized, subtle flaws that remain difficult for time-constrained humans to detect.The average validity of solution portions increases while the minimum remains low, and human labeling accuracy decreases across rounds; the human study is from a potentially flawed pilot campaign.
  • 4.3.3 THE HELPFUL PROVER BECOMES INCREASINGLY LEGIBLE THROUGHOUT CHECKABILITY TRAINING: Checkability training jointly increases the helpful prover’s accuracy and human legibility, though final performance remains below correctness-only training.At the end of training, the helpful prover matches initialization legibility while achieving substantially stronger performance, revealing a tension between performance and legibility.

5 ALTERNATIVE REWARDS

The section compares alternative prover rewards and finds that CGC produces worse training dynamics, while goodharting generally becomes more robust with larger verifiers but does not clearly improve human legibility.

  • 5.1 Checkability Training with the Correctness-Gated Convincingness (CGC) Reward: CGC prioritizes correctness or incorrectness over convincingness by assigning a penalty when the prover violates its role.Otherwise, the reward equals the verifier score.
  • 5.1 Checkability Training with the Correctness-Gated Convincingness (CGC) Reward: CGC training does not consistently become harder for the sneaky prover across rounds, indicating worse training dynamics.The number of RL steps until sneaky incorrect samples match helpful correct samples decreases from round 1 to round 3 before increasing through round 5.
  • 5.1 Checkability Training with the Correctness-Gated Convincingness (CGC) Reward: CGC nevertheless provides a strong adversarial attack for evaluating verifiers trained with the SRC reward.
  • 5.2 Iterative Goodharting Training: Larger verifiers generally delay goodharting, improve maximum prover accuracy, and reach stronger robustness in fewer training rounds, although verifier size 10−3 shows some degradation.The goodharting baseline directly optimizes verifier scores and stops when training accuracy falls below 0.2.
  • 5.2 Iterative Goodharting Training: Human judges show no significant accuracy difference across goodharting rounds, so the training increases verifier soundness only to a limited extent without sufficient evidence of improved human legibility.The human pilot study had design flaws.

6 DISCUSSION

The discussion identifies scope limits in the experiments and outlines extensions involving harder or unlabeled domains, separate legibility models, interactive games, and broader human evaluation.

  • Need for ground truth answers and reliance on generalization: The setup requires trusted ground-truth answers during training, limiting relevance where correctness labels are difficult or expensive to obtain.The authors suggest unsupervised signals and future semi-supervised or unsupervised approaches.
  • Conflating the model’s chain-of-thought with legible solutions: Training chain-of-thought directly for legibility may impose an overly pessimistic accuracy–legibility tradeoff compared with translating scratch-work into human-readable justifications.The authors do not know a principled early-stopping method for legibility.
  • Dataset diversity and difficulty: The experiments use one relatively easy, standardized GSM dataset, motivating evaluation on harder mathematics, coding, and fuzzier preference domains.The method is described as general when final answer labels form a finite set.
  • Heterogeneous experiment set-ups: The study uses heterogeneous stopping criteria and incompletely tuned hyperparameters, which could make some training schemes appear worse in robustness or legibility.
  • Future work: Future work should study interactive multi-turn prover games and more systematic human assistance, since the paper mainly measures legibility to smaller models.More verifier–prover interaction may improve sample efficiency, while broader human studies would test the ultimate target more directly.

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

The proof establishes that a verifier-leading Stackelberg equilibrium is equivalent to completeness and soundness under the paper’s stated assumptions and reward conditions.

  • Assumptions: The formal setup treats inputs as discrete, uses deterministic prover mappings, and assumes every input has at least one correct and one incorrect solution.The verifier outputs a value in [0,1], while correctness is represented by a binary indicator.
  • Reward conditions: The prover reward combines verifier scores with correctness for the helpful prover and incorrectness for the sneaky prover, while requiring higher verifier scores to yield higher reward for the same target label.The loss function is minimized when verifier output matches correctness.
  • Theorem statement: Under the stated assumptions, the existence of a verifier-leading Stackelberg equilibrium is necessary and sufficient for completeness and soundness.The proof constructs an arbitrary incorrect sneaky solution and then shows violations of either property contradict equilibrium.
  • Contradiction argument: If completeness or soundness fails, changing the corresponding prover output increases prover utility or verifier performance, contradicting the equilibrium conditions.Thus equilibrium rules out rejected correct helpful solutions and accepted incorrect adversarial solutions.

B SAMPLES FROM SEVERAL EXPERIMENTS

Correctness-only training can produce strong performance while reducing legibility, including incorrect solutions that receive high verifier scores.

  • Correctness-only training is compared at early and late stages, highlighting changes over training.
  • Strong performance can coexist with poor legibility after learning from a binary grader.
  • Incorrect solutions can receive high verifier scores at multiple points during training.

C SEPARATION MIGHT INHIBIT PROGRESSION OF CHECKABILITY TRAINING

Verifier training can exploit easy differences between helpful and sneaky provers rather than learning general correctness, limiting progress in checkability training.

  • A verifier may predict correctness from correlated, easier-to-detect solution attributes instead of learning a general correctness algorithm.
  • Training data makes correctness strongly correlated with whether the helpful or sneaky prover produced a solution.
  • Early in checkability training, helpful and sneaky solutions are easily separable using features learnable by a very small discriminator.
  • When provers separate through easily learned surface features, they may not improve verifier robustness, so game design must avoid encouraging early separation.

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

Checkability training is inhibited when the verifier is badly sized: very small verifiers destabilize training, while verifier-sized models fail to gain robustness.

  • Very small verifiers produce unstable training dynamics and degenerate solutions.
  • A verifier as large as the prover does not become more robust across rounds and also produces degenerate solutions.
  • The large-verifier evaluation also tracks human contractor accuracy on helpful-prover solutions across checkability-training rounds.

E ADDITIONAL EVALUATIONS FOR THE GOODHARTING BASELINE

Additional goodharting evaluations examine human accuracy, attacker training difficulty, and balanced best-of-n samples under small-verifier settings.

  • After three rounds of goodharting training, test samples show no significant increase in human trainer accuracy across R0-2.
  • Iterative goodharting is evaluated with verifier relative sizes 10^-3 and 3 × 10^-3, using attacker steps to reach a high verifier score while remaining 95% incorrect.
  • Balanced best-of-n evaluation uses current-round last-checkpoint prover samples with equal proportions of correct and incorrect solutions.

F VALIDATION WITH PROVERS WITH NO MATH-SPECIFIC PRETRAINING.

Supplementary validation repeats the proposed checkability training with LLMs lacking math-specific fine-tuning and reports qualitatively unchanged dynamics. The supplementary materials also document the prover prompts and initialization procedure.

  • Checkability-training dynamics remain qualitatively unchanged when repeated with LLMs not fine-tuned on math-specific text.
  • The honest and sneaky provers receive a system prompt before each grade-school math problem, with a dishonest-mode template used for the sneaky prover.
  • Solutions are sampled from the prover initialization using a few-shot prompt.

I DETAILS ON THE HUMAN LEGIBILITY EVALUATION CAMPAIGN

The human legibility evaluation samples prover and baseline solutions for time-limited correctness judgments. An earlier pilot used a different timing and presentation procedure and may be affected by learning or fatigue.

  • The main evaluation samples last-checkpoint helpful-prover solutions, correctness-only baseline checkpoints, and the few-shot initialization for GSM test problems.The experiment collects up to one correct and one incorrect sample from each prover and problem when possible.
  • An earlier pilot gave 10 trainers one minute per task and included sneaky solutions and Iterative Goodharting samples.The pilot used a 1-minute limit rather than 45 seconds.
  • The pilot presented samples in round order over one month, creating suspected learning or fatigue effects in its data.
  • Supplementary materials include the instructions shown to human trainers and an example human-evaluation task.
Loading 2407.13692v2…