Prover-Verifier Games improve legibility of language model outputs

To improve legibility, we optimize chain-of-thoughts on grade-school math problems to be verifiable by weaker models and study whether this makes them more legible to humans. This training procedure is inspired by the Prover-Verifier Game(opens in a new window), a game-theoretic framework to encourage learning agents to solve decision problems in a verifiable manner. Our method achieves half of the performance boost seen when optimizing only for answer correctness, while maintaining the ability of human evaluators to accurately assess the solutions. We believe that further reducing the performance gap between legible and capable models is an important goal for alignment research going forward.

To incentivize a strong model, the prover, to produce text that is legible to humans, we use a training scheme where we require the strong model to produce solutions that a much weaker model, the verifier, can easily verify. In particular, we use large and small models from the GPT-4 family with ~3 orders of magnitude difference in pretraining compute, that have undergone a small amount of supervised training on human-written math derivations, but no extensive post-training.

First, we generate multiple solutions to math problems from the prover model, where some of these solutions are incorrect due to naturally occurring mistakes from the prover model. We then alternate for multiple rounds between two phases:

• Verifier Training. We train the weak verifier model to predict the correctness of solutions generated by the prover.

• Prover Training. We instruct the strong prover model to play either a "helpful" or a "sneaky" role. 

  • In the helpful role, we reward correct solutions that score highly according to the verifier. 

  • In the sneaky role, we instead reward incorrect solutions that score highly according to the verifier.

We find that initially, the sneaky prover is readily able to produce incorrect solutions that convince the verifier. However, since we add these incorrect solutions to the next phase of verifier training, the same exploit is no longer convincing in the next round, and the prover is forced to explore different strategies in every round. The training ends once the sneaky prover can no longer produce incorrect solutions that convince the verifier.

1. Performance vs. Legibility Trade-Off:

• A model with only supervised finetuning on human-written derivations achieved high legibility but poor accuracy.

• Optimizing solely for correctness led to high accuracy but poor legibility.

• Our checkability game method balanced both, retaining high legibility with moderate accuracy.

2. Three Useful Models:

• Robust Verifier: Effectively distinguishes correct from incorrect solutions, even when the solution is designed to be misleading.

• Helpful Prover: Generates solutions that remain legible to humans, reducing human evaluator errors.

• Sneaky Prover: Produces subtle, incorrect solutions that initially confuse human evaluators, highlighting areas for further model improvement.

As large language models (LLMs) are increasingly used in critical domains and complex applications, it becomes essential to know whether their outputs are trustworthy. By requiring models to produce justifications that are clear and verifiable, we can enhance trust in their outputs.

A significant advantage of our methodology is that it reduces the reliance on human demonstrations or judgments regarding legibility. This autonomy is particularly relevant to the alignment of future superintelligent AI systems, where the goal is to reliably align AI systems with human values and expectations without direct human oversight.

While this work only experimented on one dataset and still requires ground truth labels, we expect that such methodologies will be instrumental in developing AI systems whose outputs are not only correct but also transparently verifiable, thereby enhancing trust and safety in their real-world applications.