Neural Interactive Proofs

We seek to provide a comprehensive treatment of neural interactive proofs spanning both theory and practice. In particular, we provide the following contributions:

1. (i)

   a unifying game-theoretic framework that generalises existing neural IP protocols;

2. (ii)

   several new neural IP protocols, including those that allow for zero-knowledge proofs;

3. (iii)

   a theoretical and empirical comparison of both new and existing protocols; and

4. (iv)

   an extensible codebase for testing different protocols in different domains.²²2The codebase will be provided in a later version of the paper.

In so doing, we hope to create a foundation for future work on neural interactive proofs and their application in building safer ML systems.

In order to aid the reader’s intuition for the concepts we introduce, we provide an example scenario to which all neural IP protocols can be applied, and refer back to this throughout the paper.

Formally, this example is a decision problem where the input is a specification and a piece of code. In a neural IP, the agents learn to interact to decide whether the code satisfies the specification.

The most closely related work to ours was – until recently – that of Anil et al. (2021), who introduce prover-verifier games played between neural networks, which we generalise and build on. While an important first step, this work is limited by the formal strength of the proof systems that result from their specific protocol (as we show), and by its application only to small models and problem instances. Similar to prover-verifier games are the works of Irving et al. (2018) and Wäldchen et al. (2022), whose proof systems make use of two provers in competition with one another and are stronger from a theoretical perspective, but are again only applied to very simple problems.

More recently, three papers (concurrent with our own and with each other) have sought to overcome some of the practical limitations of these earlier works by evaluating protocols using LM agents. Kenton et al. (2024) moves beyond earlier efforts (Michael et al., 2023; Khan et al., 2024) by considering several tasks aside from question answering, and also computational (instead of merely informational) asymmetries between the provers and verifiers. They find that multi-prover ‘debate’ protocols outperform single-prover ‘consultancy’ protocols but that there is a relatively limited benefit to debate compared to the verifier baseline performance. The authors hypothesise that one reason for this is that they do not train their models using the protocol (which is the focus of our work). Kirchner et al. (2024) do train their agents to play prover-verifier games using multiple rounds of expert iteration Anthony et al. (2017), but only on the protocol introduced by Anil et al. (2021), which we show has important theoretical limitations. They find that the helpful prover’s accuracy and the verifier’s robustness to adversarial attacks increase over the course of training, though their primary focus is on the legibility of solutions to humans. Finally, and most recently, Arnesen et al. (2024) combine several of the strengths of these two investigations by comparing multiple protocols and training the provers using a novel variant of Direct Preference Optimisation (Rafailov et al., 2023), though they restrict their attention to question-answering. Mirroring Kenton et al. (2024), they find that optimising the provers leads to higher verifier accuracy in debate but not consultancy, and that debate training introduces stronger argumentation (as measured by the use of quotations).

Unlike these recent works, our investigation is not only empirical but aims to further understand the theoretical implications of different protocols. In the same spirit, Brown-Cohen et al. (2023) study doubly efficient debate, where the provers run in polynomial time and the verifiers are more efficient still (Goldwasser et al., 2008). They prove that under appropriate assumptions, any polynomial-time computation can be verified using only a constant number of queries to the black-box representing human judgement (and in time linear in the size of a single query). Other closely related research includes work on interactive proofs for PAC verification (Goldwasser et al., 2020), where the verifier’s task is to assess whether the prover has produced a near-optimal hypothesis, and – concurrent with, and most similar to, our own work – on self-proving models (Amit et al., 2024), where the authors devise a method for training provers to demonstrate the correctness of their outputs to a fixed verifier. Both of these latter works, however, focus on hand-crafted rather than learnt proof systems. In contrast, we take inspiration from Gowal et al. (2019) and hypothesise that such ideas can best be scaled to real-world ML systems if the verifier can learn the protocol.

Interactive proofs are standardly defined with respect to a decision problem $(X,S)$, where $X$ is the set of problem instances and $S\subseteq X$ is the set of ‘positive’ instances. In Example 1, $X$ is the set of all specification-code pairs produced by the prover, and $S$ is the set of pairs where the code satisfies the specification. The prover and verifier exchange messages from their message spaces $M^{p}$ and $M^{v}$ respectively. In our example, these could be the space of all text strings under a certain length.

While validity can be viewed as a property of the verifier, being zero-knowledge can be viewed as a property of the prover. Intuitively, $\langle p,v\rangle$ is zero-knowledge if the verifier learns only whether $x\in S$ and nothing else, i.e. $v^{\prime}$ does not gain any additional power through their interaction with $p$ (represented by the fact that $z\in V$).

In this work, we study $n$-player games $\mathcal{G}=(N,\Sigma,\mathcal{L})$ where $N=\{1,\ldots,n\}$ are the agents, $\Sigma\coloneqq\bigtimes_{i\in N}\Sigma^{i}$ is a product strategy space and $\mathcal{L}$ contains loss functions $\mathcal{L}^{i}:\Sigma\to\mathbb{R}$ for $i\in N$. Each agent $i$ selects a strategy $\sigma^{i}\in\Sigma^{i}$ in an attempt to minimise their loss $\mathcal{L}^{i}(\sigma)$. More specifically, we focus our attention on what we term ‘messaging games’, which centre around rounds of communication between the different agents via multiple channels. In Example 1, for instance, the verifier might cross-reference portions of the code or the prover’s answers by sending them to a second, independent prover via a separate channel.

We use $\mathcal{G}(\sigma^{i})$ to denote the $(n-1)$-player game induced when agent $i$ plays strategy $\sigma^{i}$ in $\mathcal{G}$, but where the remaining $n-1$ agents have not yet chosen their strategies. In practice, we assume that each agent’s strategy space $\Sigma^{i}$ is defined by some finite number of parameters $\bm{\Theta}^{i}$, and will often refer to $\bm{\theta}^{i}\in\bm{\Theta}^{i}$ instead of $\sigma^{i}$. Within these games, we make use of two standard equilibrium concepts, which can be defined both locally and globally.

The simplest approach to minimising the worst-case loss using finitely many data $\mathcal{D}$ generated from $\operatorname{\mathbb{P}}$ is to ignore the worst-case performance and simply return some $\bm{\sigma}^{\text{ER}}_{\mathcal{D}}$. The question then becomes: when is minimising the empirical risk with respect to $\mathcal{D}$ sufficient for minimising the worst-case risk with respect to $X$? The following result shows that we can break this down into two properties (defined formally in Section B.2): (a) the empirical worst-case loss being similar to the actual worst-case loss; and (b) for a given $\mathcal{D}$, the empirical worst-case loss of $\bm{\sigma}^{\text{ER}}_{\mathcal{D}}$ being similar to that of $\bm{\sigma}^{\text{WC}}_{\mathcal{D}}$. These conditions do not always hold, but can do when the decision problem is sufficiently ‘regular’.

propositionworstcaseloss If $\Sigma$ has the worst-case uniform convergence property (a) and the worst-case robustness property (b) then there is some $f^{\text{WCUC}}:(0,1)^{2}\to\mathbb{N}$ such that for every $\epsilon,\delta\in(0,1)$, if $|\mathcal{D}|\geqslant m^{\text{WC}}(\epsilon,\delta)$ then $\mathcal{L}^{\text{WC}}(\bm{\sigma}^{\text{ER}}_{\mathcal{D}})-\mathcal{L}^{\text{WC}}(\bm{\sigma}^{\text{WC}})\leqslant\epsilon$ with probability $1-\delta$.

Alternatively, we can introduce an adversary, $a$, whose strategy space is $S\times X\setminus S$ and whose loss function is $\mathcal{L}^{a}(\bm{\sigma},(s,x))=-\ell(\bm{\sigma},s)-\ell(\bm{\sigma},x)$. We then replace the terms $\mathcal{L}^{\text{WC}}(\bm{\sigma}\mid y=i)$ in the original loss functions for the prover and verifier with $\ell(\bm{\sigma},s)-\ell(\bm{\sigma},x)$ and $\ell(\bm{\sigma},s)+\ell(\bm{\sigma},x)$ respectively. The verifier-leading Stackelberg equilibria of the original nip game are then identical to the verifier-prover-leading Stackelberg equilibria in this new three-player game, denoted $G^{a}$. Unlike the classical learning-theoretic approach above in which we assumed we were given a fixed dataset $\mathcal{D}$ of $(x,y)$ pairs, we are here assuming access to an adversary capable of outputting any $x\in X$. This stronger assumption may not always hold, but when it does, learning can be more efficient (Goldman & Kearns, 1995).

propositionadversarialstackelberg Let $(X,S,\operatorname{\mathbb{P}})$ be a probabilistic decision problem and $\mathcal{G}$ a nip game. Then $(\sigma^{p},\sigma^{v})$ is an approximate verifier-leading SE ($\bm{e}\textup{-SE}_{v}$) of $\mathcal{G}$ if and only if there is some $\sigma^{a}$ such that $(\sigma^{p},\sigma^{v},\sigma^{a})$ is an approximate verifier-prover SE ($\bm{e}\textup{-SE}_{v,p}$) of $G^{a}$ (the adversarial version of $\mathcal{G}$).

Computing Stackelberg equilibria can be naturally modelled as a bi-level optimisation problem. A standard solution to such problems using gradient-based methods is to employ a timescale separation (Borkar, 2008). In particular, we take the sequential nature of the problem setting into account by explicitly modelling the dependence of $\bm{\theta}^{p}$ on $\bm{\theta}^{v}$ and updating $\bm{\theta}^{p}$ more quickly as part of an ‘inner loop’. Fiez et al. (2020) show that if $\alpha^{v}=o(\alpha^{p})$ then with high probability the following dynamics will converge locally to the neighbourhood of a $\textup{LSE}_{v}$:

where we drop the dependence on $\bm{\theta}$ from our notation and write $\nabla_{v}$ and $\nabla_{p}$ for $\nabla_{\bm{\theta}^{v}}$ and $\nabla_{\bm{\theta}^{p}}$, respectively. These updates require computing an inverse Hessian vector product, which is intractable when $\bm{\theta}^{p}$ is large. Replacing the term $\Big{(}\nabla^{2}_{p}\mathcal{L}^{p}\Big{)}^{-1}$ with $\alpha^{p}(t+1)$ leads to the LOLA (Learning with Opponent Learning Awareness) update (Foerster et al., 2018), which aims to actively influence the future policy updates of its opponents. While LOLA may fail to converge, interpolating between the LOLA update and LookAhead (Zhang & Lesser, 2010) leads to local convergence to stable fixed points in differentiable games under self-play (Letcher et al., 2019).

Multi-prover interactive proofs (MIPs) are a natural generalisation of classical IPs (Ben-Or et al., 1988), whose additional power results from the fact that while the two provers may correlate their strategies, they are prevented from communicating with one another during their interactions with the verifier (Babai et al., 1991). This allows the verifier to ‘cross-examine’ the provers.

We define the mnip protocol identically to the nip protocol, but now with two provers, $p_{1}$ and $p_{2}$, each of which has the same loss. Valid MIP systems are defined as in Definition 1, with the soundness condition altered such that $v$ must be robust to any choice of $p^{\prime}_{1},p^{\prime}_{2}$. Using a similar proof to that of Section 4, it can be shown that the equilibria of the mnip PVG correspond to valid MIP systems. The only subtlety is that due to the provers’ ability to coordinate on a joint strategy and shared random signal beforehand, we must consider correlated equilibria (defined in Section B.1).

theoremmnipstackelberg Let $(X,S,\operatorname{\mathbb{P}})$ be a probabilistic decision problem that has a valid proof system and $\mathcal{G}$ a mnip game. Then $\bm{\sigma}$ is a valid MIP system if and only if it is an approximate verifier-leading correlated Stackelberg equilibrium of $\mathcal{G}$.

We now consider whether the prover can prevent the verifier from learning any more than to solve the task at hand. We formalise this question as whether the resulting proof system is zero-knowledge (ZK). Far from a theoretical curiosity, this may have important practical implications, such as for the prevention of model cloning/stealing via black-box access (Orekondy et al., 2019).

Recall from Definition 2 that $\langle p,v\rangle$ is ZK if for any $v^{\prime}$ and any $x$ such that $y=1$, there is another weak agent $z\in V$ capable of generating approximately the same distribution over message sequences as $\langle v^{\prime},p\rangle(x)$, without interacting with $p$. While it is possible to introduce a precise analogue of this condition, we wish to investigate whether the verifier can gain knowledge regardless of the value of $y$.

We therefore provide a slightly stronger condition that requires statistical closeness between $\langle v^{\prime},p\rangle(x,y)$ and $z(x,y)$ for any $x$. In other words, short of the answer $y$, there is nothing else that $v^{\prime}$ can learn by interacting with $p$. We can implement this protocol using a PVG by introducing an additional verifier agent $v_{2}=v^{\prime}$ and a simulator $v_{3}=z$, whose objectives $\mathcal{L}^{v_{2}}$ and $\mathcal{L}^{v_{3}}\coloneqq-\mathcal{L}^{v_{2}}$ are defined via:

and by adding the term $\mathcal{L}^{v_{3}}$ to the prover’s loss $\mathcal{L}^{p}$. We refer to the resulting protocol as zk-nip, and show that the equilibria of this game correspond to ZK proof systems. {restatable}theoremzknipstackelberg Let $(X,S,\operatorname{\mathbb{P}})$ be a probabilistic decision problem that has a valid $\epsilon_{\text{k}}$-statistically zero-knowledge system and $\mathcal{G}$ a zk-nip game. Then $\bm{\sigma}$ is a valid $\epsilon_{\text{k}}$-zero-knowledge IP system if it is an approximate verifier-prover-leading Stackelberg equilibrium ($\bm{e}\textup{-SE}_{v_{1},p}$) of $\mathcal{G}$. We note that in this protocol the equilibria contain a Stackelberg hierarchy with more than two levels. Namely, the prover $p$ commits to their strategy before agents $v_{2}$ and $v_{3}$. Technically, $v_{2}$ should also be viewed as committing before $v_{3}$, but $\mathcal{G}(\sigma^{v_{1}},\sigma^{p})$ is a zero-sum game and so reaching an NE is sufficient.

As a warm-up exercise, we consider the problem of testing for graph isomorphism using a synthetic dataset of 10,000 graphs (each with approximately ten vertices) generated via the Erdős-Rényi model. The verifiers and provers are implemented using a graph neural network (GNN) and transformer body, with standard feedforward heads used for sending messages and estimating the value of each state. Agents are trained using independent PPO (Schulman et al., 2017; Schroeder de Witt et al., 2020) and evaluated on a held-out test set. This simple setting has the benefit that by varying the number of GNN layers we can precisely calibrate the capability of the agents to distinguish between isomorphic and non-isomorphic graphs. By controlling the number of rounds of the Weisfeiler-Leman test (Weisfeiler & Leman, 1968) needed to distinguish non-isomorphic graph pairs in the dataset, we ensure a theoretical limit on the accuracy attainable by the verifier alone.

We begin by directly comparing the adp, debate, nip, and mnip protocols, shown in Figure 2(a) (plots of the accuracy and mean episode length over training are shown in Section D.1). While we see that nip performs favourably, with verifiers learning to near-perfectly classify valid instances when interacting with the prover, other protocols do not see an increase in performance. This, however, is mainly due to the problem setting, in which there is a relatively simple algorithm for testing for isomorphic graphs: the verifier selects a random node from one graph, and if the prover can return a similar node in the second graph, then they are likely isomorphic. This algorithm is not possible under adp as the verifier does not send any messages to the prover, and is harder to learn in the presence of multiple provers (as in debate and mnip).

Rather, the graph isomorphism task is useful because it allows us to assess how the verifier’s performance changes with its computational abilities. More precisely, we vary both the verifier’s network width and the its number of layers. We show results for the nip protocol in Figure 2(b). We observe that – as expected – larger models are able to solve the task whereas smaller models are not, and that by interacting with a (non-random) prover, verifiers gain capability in comparison with interacting with a random prover. Notably, this gap is most pronounced for verifiers that are incapable of solving the task by themselves, but are capable of doing so after learning to interact with the prover.

We also investigate the zk-nip protocol by varying the coefficient of the $\mathcal{L}^{v_{3}}$ term in the prover’s loss, which controls the strength of the prover’s incentive to minimise the simulator’s loss. In Figure 2(c), we plot the mean difference between $\operatorname{\mathbb{P}}\big{(}\langle\sigma^{p},\sigma^{v_{2}}\rangle(x,y)=\bm{m}\big{)}$ and $\operatorname{\mathbb{P}}\big{(}\sigma^{v_{3}}(x,y)=\bm{m}\big{)}$ against the $\mathcal{L}^{v_{3}}$ coefficient. We observe a roughly negative correlation, suggesting that the training converges on an equilibrium with lower information leakage as the prover coefficient increases.

Our second experiment involves a much more complex problem: checking that a given Python program satisfies a natural language specification. In particular, we make use of the Automated Programming Progress Standard (APPS) dataset (Hendrycks et al., 2021), which consists of Python coding challenges with ground-truth solutions written by humans, as well as test cases for checking the solutions. We create a new dataset by drawing two solutions for each problem, one of which we insert a subtle bug into using GPT-4o-mini (OpenAI, 2024), checking that the result is still valid Python code but that it fails on at least one of the test cases. An example is given in Section C.2.1, and the median (Levenshtein) edit distance when inserting a bug is seven. We use GPT-4o as the provers and GPT-4o-mini as the verifiers, fine-tuning both using eight rounds of expert iteration (Anthony et al., 2017). In each iteration, we fine-tune the models from scratch using all previous rollouts, following Kirchner et al. (2024). The models are then evaluated on a held-out test set.

We test each of the protocols introduced above, and in all cases we observe a modest improvement in final test accuracy over the baseline of a verifier trained in isolation (Figure 3(a)). The nip and mnip protocols see the greatest improvements in accuracy (around 11%). A key differentiator between the protocols is presented in Figure 3(b). In line with Section 4, an IP system corresponds to minimising the worst-case loss. To measure the extent to which worst-case performance is optimised, we sample rollouts from the trained agents 10 times for each test data point, and record the percentage of these where the verifier always guesses incorrectly. As shown in Figure 3(b), most protocols perform significantly better than the solo verifier baseline, with mnip performing the best. Figure 3(c) refines the accuracy metric by plotting the final precision and recall of each protocol. We see that the nip and mnip protocols perform well by obtaining a lower false negative rate than the other protocols, while maintaining a high true positive rate.

We observed that both debate and the solo verifier have a high precision-to-recall ratio. Further analysis reveals that expert iteration exacerbates an initial low acceptance rate in both cases, because only rollouts where the verifier guesses correctly are included in the fine-tuning data. To remedy this, we introduce a new training scheme (‘stabilised’ expert iteration) where in an annealed proportion of the rollouts, the verifier’s guess is replaced with the true label. Figure 4(a) shows that this greatly reduces the ‘mode collapse’ dynamics seen with vanilla expert iteration. In Figure 4(b) we see that replacing the verifier guess also allows the solo verifier to obtain much higher mean accuracy, which we hypothesise is due to the training scheme being closer to standard supervised fine-tuning. Using this scheme has a small effect on the mean accuracy of each interaction protocol, improving some and worsening others. However, Figure 4(c) shows that the worst-case performance of every protocol is improved by this training scheme, with the debate protocol performing particularly well.