Table of Contents
Fetching ...

Learning to Give Checkable Answers with Prover-Verifier Games

Cem Anil, Guodong Zhang, Yuhuai Wu, Roger Grosse

TL;DR

The paper introduces Prover-Verifier Games (PVG) to induce verifiable decision protocols between a trusted verifier and an untrusted prover. It analyzes which game formulations yield complete and sound proof-verification equilibria and demonstrates, via gradient-based optimization, that robust verification strategies can emerge in practice. Through simulations on the Binary Erasure Channel and a FindThePlus task, PVG-trained verifiers exhibit strong robustness to adversarial prover behavior and even maintain performance when the verifier is frozen. The work provides both theoretical guidance on which PVG formulations are desirable and empirical evidence that learnable verification protocols can improve reliability in decision problems. This framework offers a principled route to deploy high-stakes machine decisions with measurable, checkable justification protocols.

Abstract

Our ability to know when to trust the decisions made by machine learning systems has not kept up with the staggering improvements in their performance, limiting their applicability in high-stakes domains. We introduce Prover-Verifier Games (PVGs), a game-theoretic framework to encourage learning agents to solve decision problems in a verifiable manner. The PVG consists of two learners with competing objectives: a trusted verifier network tries to choose the correct answer, and a more powerful but untrusted prover network attempts to persuade the verifier of a particular answer, regardless of its correctness. The goal is for a reliable justification protocol to emerge from this game. We analyze variants of the framework, including simultaneous and sequential games, and narrow the space down to a subset of games which provably have the desired equilibria. We develop instantiations of the PVG for two algorithmic tasks, and show that in practice, the verifier learns a robust decision rule that is able to receive useful and reliable information from an untrusted prover. Importantly, the protocol still works even when the verifier is frozen and the prover's messages are directly optimized to convince the verifier.

Learning to Give Checkable Answers with Prover-Verifier Games

TL;DR

The paper introduces Prover-Verifier Games (PVG) to induce verifiable decision protocols between a trusted verifier and an untrusted prover. It analyzes which game formulations yield complete and sound proof-verification equilibria and demonstrates, via gradient-based optimization, that robust verification strategies can emerge in practice. Through simulations on the Binary Erasure Channel and a FindThePlus task, PVG-trained verifiers exhibit strong robustness to adversarial prover behavior and even maintain performance when the verifier is frozen. The work provides both theoretical guidance on which PVG formulations are desirable and empirical evidence that learnable verification protocols can improve reliability in decision problems. This framework offers a principled route to deploy high-stakes machine decisions with measurable, checkable justification protocols.

Abstract

Our ability to know when to trust the decisions made by machine learning systems has not kept up with the staggering improvements in their performance, limiting their applicability in high-stakes domains. We introduce Prover-Verifier Games (PVGs), a game-theoretic framework to encourage learning agents to solve decision problems in a verifiable manner. The PVG consists of two learners with competing objectives: a trusted verifier network tries to choose the correct answer, and a more powerful but untrusted prover network attempts to persuade the verifier of a particular answer, regardless of its correctness. The goal is for a reliable justification protocol to emerge from this game. We analyze variants of the framework, including simultaneous and sequential games, and narrow the space down to a subset of games which provably have the desired equilibria. We develop instantiations of the PVG for two algorithmic tasks, and show that in practice, the verifier learns a robust decision rule that is able to receive useful and reliable information from an untrusted prover. Importantly, the protocol still works even when the verifier is frozen and the prover's messages are directly optimized to convince the verifier.

Paper Structure

This paper contains 23 sections, 13 theorems, 14 equations, 3 figures, 3 tables.

Key Result

Proposition 1

Any PVG formulation in which the verifier is given the problem instance before it selects its strategy has bad equilibria --- that is, having converged to an equilibrium is neither necessary nor sufficient for having found a complete and sound proof verification protocol.

Figures (3)

  • Figure 1: Depiction of a proof-verification protocol learned via Prover-Verifier Training. When trained on the task of detecting whether there's a blue plus pattern (\ref{['fig:plus']}) in the input image, Prover-Verifier Training discovers a coordinate-based verification protocol. If there's a plus in the image (\ref{['fig:positive_ex']}), the prover sends its coordinate, and the verifier accepts this certificate. If there's not a plus in the image (\ref{['fig:negative_ex']}), then the prover sends the coordinates of a maximally convincing image patch, but the verifier rejects this certificate.
  • Figure 2: BEC training dynamics: The evolution of the logits, per input-output pair, of the prover (top) and verifier (middle), accompanied by the accuracy of the verifier (bottom). The verifier quickly picks the correct verification protocol, which drives the whole system into the desired equilibrium.
  • Figure 4: Visualizing Verifier's Gaze: We visualized where each of the verifier's $4$ Spatial Transformer heads learn to look at. The top row displays the inputs. The left three inputs contain a blue plus in them (what the prover is defending). Each subsequent row corresponds to a different verifier head. We observe that the first head consistently contain blue plusses at consistent locations, indicating that the prover is communicating the coordinate of the plus to the verifier. If there's not a blue plus in the image, the prover sends the coordinate of a convincing image patch.

Theorems & Definitions (25)

  • Definition 1: Completeness and Soundness
  • Definition 2: Nash Equilibrium neumann1944theory
  • Definition 3: Stackelberg Equilibrium fiez2019convergence
  • Definition 4: Abstract Decision Problem
  • Proposition 1
  • Theorem 1
  • Theorem 2
  • Theorem 3
  • Corollary 1
  • Definition 5
  • ...and 15 more