Neural Interactive Proofs

“Simple experiments”

While the reviewer is correct that the Graph Isomorphism experiments are deliberately simple (as this allows us benchmark our empirical results against theoretical bounds, and to more easily assess the influence of key variables such as the network size and amount of training data), we respectfully disagree that the Code Validation experiments are simple. The underlying APPS dataset (Hendrycks et al., 2021) contains coding problems ranging from “introductory” to “competition”. We do not agree that competition-level programming challenges are “simple”, nor that detecting subtle bugs in proposed solutions to such challenges is. Indeed, our results show that even a (near-)state-of-the-art model such as GPT-4o fails to do much better than chance on such a problem, indicating that it is in fact highly non-trivial. With that said, both our theory and our codebase support applications to many other domains, and we believe that this is a promising avenue for future research.

Questions

As requested by the reviewer, we have responded to their comments under the “Weaknesses” section. Following their suggestion, we have also added experimental results regarding zero-knowledge protocols and further discussion to our paper (described further in the update summary above).

We thank the reviewer for their careful reading and commentary on our paper. In what follows, we address the weaknesses and questions raised by the reviewer, in light of our updates to the paper described in the official comment further above. In particular, we have expanded our empirical results and linked them more closely to our theoretical contributions (the latter of which we also explain and justify further below). We also seek to address what we view to be some misunderstandings of our work in the reviewer’s commentary. To the extent that these replies address the reviewer’s concerns, we kindly request that they consider the impact this might have on their assigned scores; to the extent that they fail to address the reviewer’s concerns, we warmly welcome any further questions or comments.

Weaknesses

“It is unclear on the zero-knowledge aspect”

We agree with the reviewer that the original version of the paper was too brief in motivating our discussion of zero-knowledge protocols. The idea here is that while prover-verifier games may describe a training setup (in today’s current ML paradigm where there is a training-deployment dichotomy), in the future we will likely have large numbers of AI systems and services interacting with one another in order to solve tasks. While we may want such systems to be able to query one another, we may not wish for agents to gain additional knowledge from doing so (perhaps because it represents private information, or could imbue the agent with new, potentially dangerous capabilities).

While this risk is not novel, the concept of zero-knowledge interactions between such agents provides a firm theoretical foundation for addressing such problems. On the other hand (from the verifier’s perspective instead of the prover’s), it also suggests a fundamental limit to the amount that might be learnt from interacting with another, more powerful agent. Thus, while using zero-knowledge protocols is certainly not “necessary”, it may provide additional information security. To support this hypothesis, we have now also included some preliminary experimental results validating our zero-knowledge training scheme.

Worst-Case Optimisation and Stackelberg Equilibria

Regarding the reviewer’s confusion about the paragraph under Proposition 2, we kindly request that they point out the specific notation that is unclear, so that we correct or further explain this if necessary. Regarding the use of bi-level optimisation to solve the Stackelberg game, we believe the reviewer may have misunderstood the motivation behind this approach. We do not introduce the idea of a Stackelberg equilibrium in order to motivate bi-level optimisation; rather, it is Stackelberg equilibria of the prover-verifier games that correspond to valid proof systems (see Theorems 1-3), and seeking the latter in turn motivates using bi-level optimisation. Thus, the idea of Stackelberg equilibria is in fact crucial to the correspondence between prover-verifier games and proof protocols, whereas bi-level optimisation is not.

Unimplemented developments

We agree with the reviewer that a weakness of the original version of our paper was that we did not include experimental results for the zero-knowledge protocols and some of the other protocols in the paper. This shortcoming has now been rectified, and the additional results are described further in the update summary above. We have also implemented methods for adversarial training and algorithms for Stackelberg Policy Gradient (Fiez et al., 2020), Learning with Opponent-Learning Awareness (Foerster et al., 2018), and Stable Opponent Shaping (Letcher et al., 2019) in our codebase.

Typos

We respectfully disagree with the reviewer that the paper has “many” typos, or that the existence of extremely minor typos (such as "a node a similar node the second graph") means that the paper requires significant development before it can be published. We will of course make sure that we rigorously check for any remaining small typos before the full paper is published, and if the reviewer has identified any more typos beyond the single instance they included in their original review, we kindly request that they make these known to us so that they can be fixed.

Given that the discussion period is due to end in around 48 hours, we wish to offer a brief reminder of the changes we have made in response to the reviewer’s comments and the answers to their questions, as we have not yet received any reply to our response. In particular, we have:

• Clarified the motivation behind, and importance of, zero-knowledge neural interactive proofs;
• Clarified the significance of Stackelberg equilibria and the connection to bi-level optimisation;
• Conducted additional experiments that connect more closely to our theoretical contributions;
• Corrected the typo pointed out by the reviewer;
• Explained how the code validation task is in fact non-trivial for state-of-the-art LLMs and thus why we do not believe the experiment is too “simple”.

To the extent that these updates and replies address the reviewer’s concerns, we kindly request that they consider the impact this might have on their assigned scores; to the extent that they fail to address the reviewer’s concerns, we warmly welcome any further questions or comments, and will do our best to address them in the remaining time permitted.

We thank the reviewer for their reply to our response, and we are glad that our explanations seem to have alleviated some of their concerns. We address the remaining concerns in their reply in turn.

Zero-Knowledge

First, as we highlight in our original response, we do not expect that the verifier and prover “need to satisfy zero-knowledge” (emphasis ours), only that it may be useful in some cases. Moreover, we would like to emphasise that our paper is not specifically about zero-knowledge proofs. Indeed, the reviewer will note that they are described in Section 5.1, with the title of Section 5 being “Extensions”. We summarise what we view to be our core contributions further below.

With that said, to try to explain the usefulness of zero-knowledge protocols further, let us consider three examples in which a user employs a weak (trusted) verifier agent to interact with a strong (untrusted) prover agent that is provided by some model provider via an API. The key idea of zero-knowledge protocols is for the prover (controlled by the model provider) to adopt a strategy that prevents the verifier (controlled by the user) from extracting additional knowledge from their interactions, while still being able to solve the task at hand.

1. First and foremost, recent work has highlighted the risk of “model stealing” via black-box queries (Oliynyk et al., 2023). In other words, merely by interacting with the prover, a verifier can distill the model representing the prover to gain more knowledge than is required to merely solve the task at hand.
2. Another concern is that the verifier might be able to query the prover in a way that allows them to develop dangerous capabilities (Phuong et al., 2024; Jones et al., 2024). For example, a prover being queried about a chemistry problem might inadvertently leak information that enables the verifier to synthesise dangerous chemicals.
3. Finally, proprietary models serving as provers may have learnt private information (either deliberately via instruction from the model provider or unintentionally because of the information being in the pre-training dataset). It is important that we develop techniques to prevent the extraction of this data via black-box model access (Carlini et al., 2020).

While we certainly do not claim to have directly solved these problems in our paper (as they are not the main focus of our work), we do suggest that the concept of zero-knowledge interactions between such agents provides a firm theoretical foundation for addressing such problems. On the other hand (from the verifier’s perspective instead of the prover’s), it also suggests a fundamental limit to the amount that might be learnt from interacting with another, more powerful agent.

Stackelberg Equilibria

We fully agree with the reviewer that using bi-level optimisation to solve for Stackelberg equilibrium is not a novel contribution of this paper, and indeed we do not claim it to be. In fact, only a mere 18 lines (3.3%) out of the 539 in the main body of our paper are dedicated to discussing this point, and we explicitly cite several prior works when explaining how these ideas are relevant to solving the problems we are interested in. Rather, the novel contributions of our paper are:

1. A unifying game-theoretic framework that generalises existing neural IP protocols;
2. Several new neural IP protocols, including those that allow for zero-knowledge proofs;
3. A theoretical and empirical comparison of both new and existing protocols;
4. An extensible codebase for testing different protocols in different domains.

The reason that we briefly discuss solving for Stackelberg equilibria using multi-agent reinforcement learning is that some readers may not be as familiar as the reviewer with the standard techniques used for doing this, or how they can be tractably approximated using various different learning updates. We stress that we do not wish to claim this brief discussion as a novel contribution of our work, and we hope this alleviates the reviewer’s concerns.

Regarding Definition 5:

• Line 223-225: We apologise for the typo. The reviewer is correct that it should have been written $m_T$, not $m^T$. It is indeed the same $m_T$ as in L140. We use $T$ to denote the index of the final timestep of a trajectory. Finally, the reviewer is also correct that $1_S$ is the indicator function on membership in $S$ (which is defined at the beginning of Section 2).
• Line 223-225: We apologise for the typo. The inequality should indeed be the other way round (i.e., a higher chance of success corresponds to a lower loss).
• Line 228—230: We apologise for the typo. We should have written $\mu(c^\dagger, 1) = \{p\}$ instead of $\mu(0, c^\dagger) = \{p\}$. In other words, the game proceeds by an input $x$ being sampled at time 0, before being immediately terminated after a single message is sent by a prover p in the channel $c^\dagger$ at timestep 1. The reviewer is quite correct that in the PVG model we assume that $c^\dagger = \{v\}$ for some $v \in N^v$. Criterion 3 represents a counterfactual scenario: if it were the case that we instead had $c^\dagger = \{p\}$ for some $p \in N^p$, then it would be the case that $\min_{\sigma^p} \Ell^v(\sigma^p, \sigma^{-p}_u) \approx l^v_\star$. This counterfactual scenario is consistent with the reviewer’s correct observation that there is no overlap between provers and verifiers. We have now highlighted explicitly that this criterion is a counterfactual.

Questions

Questions

• In effect, yes, we can view the application of a deterministic loss function to stochastic strategies as being calculated given a random seed that is fixed ahead of time.
• Yes, the union $N = N_p \cup N_v$ is indeed disjoint in line 218. We have updated the notation to $\sqcup$ to reflect this – thank you for the suggestion. In addition, as the reviewer notes in their “minor comments”, our use of subscripts here is inconsistent with our use of superscripts elsewhere, and we have also fixed this typo.

Minor comments

• Thank you for pointing out the typo regarding the inconsistent use of $\top$ ($\bot$) and 1 (0). We have now removed all earlier usages of the former and replaced them with the latter.
• We apologise for this typo. The correct usage is that $\langle p, v \rangle(x)$ denotes an entire sequence of messages ($\mathbf{m}$). We have now updated Definition 1 to reflect this.
• The reviewer is correct that the “assumption” in line 179 is really more of a requirement about the structure of the game. We have updated the wording to reflect this, as suggested.
• We have now corrected the typo on line 228-229 (as also noted further above).
• The reviewer is correct that the use of subscripts in $N_p$ and $N_v$ (instead of superscripts) is indeed a typo, and one that we have now fixed.

• Regarding the reviewer’s final question, we are not entirely sure we have fully understood everything, but we attempt to provide further clarity regardless, and we welcome any additional questions or corrections to our potential misunderstandings.
  • Firstly, we point out that in the code validation experiments, it is empirically the case that interactivity (i.e. using NIP instead of ADP) allows a verifier of the same computational capabilities to achieve higher accuracy, though we are unsure if the reviewer would view this example as sufficient. Nonetheless, it suggests that Example 1 is in fact realistic and not hyperbolic. From a theoretical perspective, while this takes us further from our domain of expertise as researchers, it is possible to combine probabilistically checkable proofs (PCPs) with IPs in order to obtain the benefits of both: requiring the verifier to only query small portions of the proof, while using interaction to handle more complex problems (Kalai & Raz, 2008).
  • Secondly, regarding the interplay between interactivity and generalisation from examples, one key intuition behind this that representing the game between prover(s) and verifier in ‘extensive-form’ (i.e. with multiple rounds of interaction) is that, assuming the verifier has perfect recall, their strategy can be encoded more compactly using a behavioural representation, meaning that effectively they only need to consider their local state when making a decision. In other words, the tree-like space of interactions introduces additional structure to the problem, factoring the verifier’s strategy space, which can in turn make learning easier.

Finally, in response to the reviewer’s suggestion, we have now added analysis detailing how performance degrades as the complexity of verification tasks increases (see Figure 8).

“The notation is not fully explained and the constraints in one of the central definitions (5) are contradictory”

We are extremely grateful to the reviewer for pointing out some of the minor issues with the notation and definitions. We agree with the reviewer that despite this, “the ideas are sound and the definitions are repairable” and in our updated manuscript (described further in the update summary) we have now repaired all of the flaws pointed out by the reviewer.

Regarding Definition 3:

• Line 173: $\Delta(X)$ refers to the set of all distributions over a set X and is defined at the beginning of Section 2.
• Line 174-175: We apologise for the typo. We meant $C(i) = \{ c \in C : i \in c\}$, where $c \subseteq N$. In other words, a channel $c \in C$ contains a set of players, and $C(i) \subseteq C$ denotes the set of all channels to which player $i$ belongs.
• Line 174: Given the meaning of $\Delta(X)$ and the type signature $\mu : C \times \mathbb{N} \to \Delta(2^N)$ in Definition 3 we hope it is now clear that $\mu$ can be stochastic.
• Line 176: We use the (standard) notation $\sim$ in $i \in N’ \sim \mu(t, c)$ to indicate that $N’$ is sampled from $\mu(t, c)$.
• Line 178: $\rho$ denotes the distribution that governs the drawing of random messages, which occurs when the protocol does not select any agent to move – it has no other special characteristics or functions, we simply used the letter $\rho$ to represent “random”.
• Line 178: A random message $m^0_{c,t}$ is sent to channel $c$ at timestep $t$ whenever we have $\varnothing \sim \mu(c,t)$ (i.e., the protocol does not select any agent to play in channel $c$ at timestep $t$). Thus, it is possible that a random message may be sent in one channel at a given timestep, but not in another. In other words, the distributions $\mu(c,t)$ over subsets of players needn’t be correlated between channels $c$ (or timesteps $t$, for that matter).

We thank the reviewer for their careful reading and commentary on our paper. In what follows, we address the weaknesses and questions raised by the reviewer, in light of our updates to the paper described in the official comment further above. In particular, we have now fixed all mathematical/notational typos, and added further detail (see also below) that we hope clarifies the scope, motivation, and impact of NIP.

Weaknesses

“The scope, motivation, and impact of NIP are not made clear”

We concede that given the wide range of background material and length limitations, there is inevitably a reasonably large degree of context needed to easily interpret some aspects of the paper. With that said, we have tried to ensure that the key messages of the paper are digestible, and we hope that our answers below and updates to the paper have improved it in this regard. In what follows, we respond to the three specific points raised by the reviewer.

• The reviewer is correct that in a sense the verifier itself represents the formal specification, though we would still defend the claim that (unfortunately!) it is not yet the case that large neural networks are amenable to analysis using “standard formal verification tools”.
  • The concurrent work of Gross et al. (2024) is closely related to our paper in that they are also focused on using small, learnt components to verify the performance of larger models. While they are able to obtain stronger guarantees using white box access (whereas we only assume query access), their approach does not yet scale to the kinds of problems and models we consider, for example, in our second experiment. A direction or future work that we are especially excited about is the combination of neural interactive proofs with other tools such as white-box access or the ability to simulate a model.
  • Finally, the reviewer is correct that our emphasis is on problems where “any system which is powerful enough to (non-interactively) verify the solution is larger or more complicated than what we’d be willing to trust as part of our specification”, and we found this rephrasing to be especially crisp and helpful. As a final additional subtlety, in practice we will be interested not in “any [sufficiently powerful] system” but in those powerful systems that we have available to us. I.e., perhaps there is nothing in theory to prevent the construction of a trusted, powerful agent to solve a task, but we do not in fact have such an agent or know how to construct it.
• We agree with the reviewer that the construction of the counterexample in the proof of Proposition 1 is rather contrived (though this of course does not make it any less correct). We furthermore agree that the key idea here is about the computational limitations of the agents. We would argue, however, that our proof is an attempt to highlight the importance of realistic assumptions, rather than eschew them.
  • Concretely, Anil et al. (2021) prove their correspondence result by limiting the verifier to be deterministic (which will not be a reasonable model of most AI systems, despite the fact that deep down they are essentially deterministic), and by assuming that perfect soundness is possible (which is also not realistic). Our claim in Proposition 1 is to show that relaxing these conditions means their correspondence no longer holds. This issue is averted (as shown in Theorem 1) by considering approximate equilibria and by not blurring the distinction between soundness and completeness when considering worst-case outcomes.
  • Separately, both the theory of interactive proofs and our experimental results suggest that greater interactivity (i.e. NIP over ADP) leads to improved performance (see also our further reply on this point below).
  • Finally, zooming back out to the broader point: in this work we model the computational limitations of agents by circumscribing their strategy spaces (as in Definition 5, but see also Figure 2b), though empirically we also consider the impact of limited access to training data in Figure 5. While not unreasonable, this is clearly not a perfect model for all purposes, as it does not capture, for example, the difficulty in searching over a larger strategy space. As we note in our introduction, we view our paper as falling between one extreme (modelling these limitations using Turing machines) and another (using different kinds of neural networks). We are excited about the possibility of future research that attempts to further bridge this divide in order to enable powerful theoretical results to improve the safety of real-world systems.

Thank you for the edits to the paper and for your detailed responses. I haven't yet fully digested them, but I want to make sure there's as much time as possible before the end of the reviewing period to address the specific points that might raise my score, so I'm going to follow up with some additional questions (in the “The scope, motivation, and impact of NIP are not made clear” category) now, after having read the responses only once.

(I will note in passing that the point "We would argue, however, that our proof [in the counterexample of Proposition 1] is an attempt to highlight the importance of realistic assumptions, rather than eschew them." is well-made, and also that I have not yet managed to digest

Secondly, regarding the interplay between interactivity and generalisation from examples, one key intuition behind this that representing the game between prover(s) and verifier in ‘extensive-form’ (i.e. with multiple rounds of interaction) is that, assuming the verifier has perfect recall, their strategy can be encoded more compactly using a behavioural representation, meaning that effectively they only need to consider their local state when making a decision. In other words, the tree-like space of interactions introduces additional structure to the problem, factoring the verifier’s strategy space, which can in turn make learning easier.

)

It seems to me that an interesting application of NIP requires the following properties:

1. We are trying to establish some property $\mathcal P$ (e.g., code is good) of some object $o$ (e.g., the code).
2. We have some property $\mathcal H$ (e.g., there is no bug on this line of code) of some other sort of object $p$ (e.g., one line of code), such that:
   1. For a typical $o$, if $\mathcal H$ holds on all choices of $p$, then we would believe $\mathcal P(o)$ is true
   2. For most (or all) $o$ for which $\mathcal P(o)$ is false, it is easy to chose a $p$ (perhaps at random) such that $\mathcal H(p)$ is false
   3. It is easy to trust (the small model that performs) the choice of $p$ and the correlated check of $\mathcal H$
   4. It is infeasible to check $\mathcal H$ across all choices of $p$.

In the interactive proofs I've seen (which is alas not that many), the power comes from having a vast computational gap between "for all" ("holds on all choices" in 2.1) and "there exists" ("it is easy to chose a" in 2.2). But this sort of computational gap seems to me to be of a different kind than what I'd expect to see in powerful LLMs. What is an example of a task where we have the following three things?

1. there's a property $\mathcal H$ that is simultaneously hard enough to check that we'd need an LLM, but one that is easy enough to check that we expect we could trust the LLM to check it
2. spot-checks of this property are enough to flag most bad examples
3. exhaustive checking of this property is infeasible

Note that the code checking example seems to fail at (2) and/or (3) -- I expect that either the small models will not be good enough at finding the suspicious places to inspect that can trust that they will be able to find all (or even most) suspicious blocks of code, or else the small models will be good enough that they can do a more-or-less complete exhaustive check for suspiciousness.

Perhaps another way of saying this is that the power of IP seems to come from being able to hide information about how a choice was made, and it is not clear to me that this extends to NIP.

I expect that if I become convinced otherwise (either by examples of NIP being expected to shine from the above sort of power, or by being given another frame on what makes IP powerful that suggests that the extension to NIP will benefit from the same power), I'd be happy to update my score to a 10; I expect that without this, I'll keep my score at an 8.

I'll post a follow-up comment with some background on my understanding of IP / NIP that led to the above property list, which I hope may be useful if the above seems incorrect to you. I'll also aim to respond to the other comments before the deadline.

I think it's definitely worth adding a sentence or two to the discussion / future work (or even a whole appendix section, if there's time) about how essential amplification techniques are; it now seems to me that the two things we'd need to trust / prove about the smaller model / verifier are that it does a good job of checking, and that the amplification technique it is using is sufficient. Of these, it seems like establishing that the amplification technique is sufficient to catch rare and subtle failures is going to be trickier by far, especially if we have to establish that it is possible to learn sufficiently good amplification techniques without necessarily being able to establish what the amplification technique is.

In light of my this discussion, I will be increasing my score from 8 to 10 -- I now believe this paper lays solid groundwork for a substantial new field of investigation that may prove important to steering AI systems.

However, I will be keeping my confidence level at 2 -- the existing literature in Interactive Proofs is still quite new to me, and I am not confident in my ability to judge how this paper fits in amongst existing work.

I'd also like to thank the authors for their detailed and friendly engagement with my questions and concerns.

Thank you for this suggestion! In short, we completely agree. Amplification via repetition is one of the key ways in which classical interactive proofs gain their power and we are cautiously optimistic to see that this at least tentatively seems to be the case for neural interactive proofs as well, though of course this clearly demands a more detailed investigation than we were able to provide within the scope of the present work. Indeed, as the reviewer suggests, there may also be other ways in which inference-time compute can be used to boost the effectiveness of scalable oversight. We are in the process of analysing our results further in this regard and plan to conduct additional experiments along these lines. If we are satisfied that these further results are sufficiently robust we will at least include them in the appendix as a post-acceptance change (if, indeed, our paper is accepted!) and in any case will consider this further as part of ongoing follow-up work. Thanks again!

We thank the reviewer for their careful reading and commentary on our paper. In what follows, we address the weaknesses and questions raised by the reviewer, in light of our updates to the paper described in the official comment further above. In particular, we have expanded our empirical results and linked them more closely to our theoretical contributions (the latter of which we also justify further below). To the extent that these replies address the reviewer’s concerns, we kindly request that they consider the impact this might have on their assigned scores; to the extent that they fail to address the reviewer’s concerns, we warmly welcome any further questions or comments.

Weaknesses

“The theoretical results aren't very important”

While we understand that this may not have been that reviewer’s primary contention, we would defend the importance of theoretical results in “construct[ing] better protocols or … analyz[ing] the safety of protocols”. Indeed, many ideas in scalable oversight (including debate, for example), have been directly inspired by deep results in computational complexity theory that give us hope that a weak verifier may be able to oversee a strong prover. More than this, however, we believe that such results can be practically useful, informing us, for example that:

• Optimising for Nash equilibrium is not sufficient for finding a valid protocol (Anil et al., 2021)
• Several subtle aspects of the interaction protocol can have a significant impact on its resulting efficacy, such as:
  • The ability of the verifier to randomise (Proposition 1)
  • Separate communication channels for the provers (Theorem 2; see also Barnes & Christiano, (2020))

Regarding our results about worst-case performance, we agree that this setting is inherently intractable for extremely complex, real-world scenarios. Our aim with Proposition 2 is to gesture at the high-level conditions of a problem that imply that despite this difficulty it can be enough to minimise the empirical risk. As more advanced techniques and theory become available for targeting worst-case optimisation (see, e.g. Shalev-Shwartz & Wexler (2016), Tang et al. (2019), Gu et al. (2023), etc.), satisfying these conditions may become available by other means. Our aim with Proposition 3 is merely to formalise the intuitive idea that the introduction of an adversary is a natural example of one such technique and mirrors, for instance, the use of an adversary in the debate protocol. To complement these theoretical results, we have also now included empirical results regarding the worst-case performance of different protocols (see Figures 3b and 4c), which indicate that progress can indeed be made in this direction.

Regarding the motivation behind our discussion of zero-knowledge protocols, the idea is that while prover-verifier games may describe a training setup (in today’s current ML paradigm where there is a training-deployment dichotomy), in the future we will likely have large numbers of AI systems and services interacting with one another in order to solve tasks (see, e.g., Drexler, (2019) for one vision of this scenario). While we may want such systems to be able to query one another we may not wish for agents to gain additional knowledge from doing so (perhaps because it represents private information, or could imbue the agent with new, potentially dangerous capabilities). While this risk is not novel, the concept of zero-knowledge interactions between such agents provides a firm theoretical foundation for addressing such problems. On the other hand (from the verifier’s perspective instead of the prover’s), it also suggests a fundamental limit to the amount that might be learnt from interacting with another, more powerful agent.

Presentation: 1

We note that the reviewer rated the presentation of the paper as “poor” (1), but apart from their remarks on missing error bars in Figure 3 (now added) and some lack of clarity regarding Figure 8 (now fixed, see below), they do not mention any other issues about presentation in their review. If there are other aspects of the presentation that the reviewer suggests we improve, we kindly ask them to communicate these so that we can do so; otherwise, we hope they will update their score regarding our paper’s presentation.

Questions

How is Figure 3, which shows (nip > adp > solo verifier > debate), consistent with Figure 8, which appears to show that at the end of training that (solo verifier = nip > adp > debate)?

To clarify, Figure 8 was plotted so as to represent our training process, which, following Kirchner et al. (2024), uses Expert Iteration on partitions of the data at each iteration. We have now also included a plot of the test accuracy by iteration (Figure 12), which more closely aligns with the final test accuracy.

Can we get error bars in Figure 3, please?

Thank you for this suggestion. We have added error bars to the figure.

What future research directions are enabled by the theoretical contributions of this paper, and why are they important?

Thank you for the excellent question. While many of our theoretical contributions serve primarily to ground and motivate our subsequent discussion, we believe that the generalised PVG model we introduce and our preliminary theoretical results also provide fertile ground for future research directions, such as:

• Comparing and creating new protocols using the generalised PVG formalism, which crisply captures the roles of features such as randomness (of agent strategies or of the protocol itself), hidden information (as in the use of separate communication channels), multiple agents (such as in debate or MNIP), and the solution concepts corresponding to valid outcomes of the protocols. While several protocols have been suggested at this point, it is far from clear that an “optimal” protocol has been discovered, and indeed a major motivation of our work is in comparing and creating protocols. By providing an explicit formalism we may also combine it with other formalisms, such as “open-source games” or “program games” (where at least one agent’s strategy is partially transparent to the other – in ML this could be enabled by providing white-box access to the model), and derive the guiding principles that we should employ if/when implementing new, more exotic protocols.
• Developing and evaluating new algorithms for training agents in PVGs, such as those that aim to find different solution concepts (e.g. Stackelberg equilibria), or those place more emphasis on worst-case performance instead of average-case performance (e.g. by introducing additional adversaries). At the moment it remains an open question when it comes to the viability and impact of such algorithms, but our preliminary results (and codebase implementations) provide a foundation for additional investigations in this area.
• Pursuing a theoretically principled investigation into the prevention of model extraction/stealing via black-box interactions (based on the idea of zero-knowledge interactions). While this direction is certainly more speculative than the others, we believe (as described further above) that the underlying problem is an important one, and one that may benefit from an alternative lens (namely, zero-knowledge interactions) when it comes to inspiring new solutions.
• Developing a rigorous understanding of strategic interactions between agents of different computational abilities. In a future teeming with different AI agents, their capability asymmetries may be important not only for problems of scalable oversight but for problems relating to cooperation and exploitation (Dafoe et al., 2019). PVGs provide one example of settings in which a weak agent can solve a problem via interaction with a strong agent despite not being fully aligned with the strong agent, but understanding the more general conditions under which weak agents can be robust to exploitation by computationally stronger agents (and the corresponding “scaling laws”) is very much an open problem and is the subject of some of our research that builds on this paper.

“The theoretical results aren't crucially related to the empirical results”

We agree that this was a shortcoming of our original presentation, and have now included preliminary results for the zero-knowledge protocols in the graph isomorphism setting, validating our zero-knowledge training scheme (described further in the update summary). We have additionally implemented methods for adversarial training and algorithms for Stackelberg Policy Gradient (Fiez et al., 2020), Learning with Opponent-Learning Awareness (Foerster et al., 2018), and Stable Opponent Shaping (Letcher et al., 2019) in our codebase. Finally, in the new experiments that we include in the revised paper we have specifically sought to further study the worst-case performance, showing empirically how different protocols (see Figure 3b) and training regimes (see Figure 4c) affect this metric. As noted above, while optimising the true worst-case loss is intractable in practice, we argue both that this represents the gold standard for developing safe, advanced AI systems, and that progress can be made vis-a-vis this standard.

“The empirical results aren't very detailed/strong”

We agree with the reviewer that the point of the Graph Isomorphism experiment is as a validation tool. However, the highly structured and theoretically crisp nature of the resulting learning problem additionally allows us to validate the effects of different model sizes (Figure 2b) and amount of data (Figure 5) on the efficacy of the resulting protocol.

We thank the reviewer for their compliments on the APPS setting. In response to their concerns we have added additional experiment analysis (described further in the update summary). In particular, further investigate the impact of problem difficulty, the distribution of protocol accuracies across problems, and the precision and recall of the different protocols. This helps point out a key reason that NIP and MNIP outperform debate which is that using standard expert iteration leads to the verifier rejecting very often under the debate setting. Our leading hypothesis is that this stems from the presence of a prover arguing for rejection, not just acceptance, combined with the fact that for code correctness there is a certain kind of asymmetry where arguing for the presence of a single flaw that undermines the correctness of a program is intuitively easier than arguing for correctness of the entire program. Another way to phrase this is that the debater arguing for rejection need only make an existential claim (“there is a line with a bug”), whereas the debater arguing for acceptance must make a universal claim (“all lines are bug-free”). Combined with the fact that solo verifier is also reluctant to accept any potentially buggy code (even after extensive prompt tuning to prevent this behaviour), this helps to explain the biassed and thus lower performance of debate relative to NIP and NMIP. When this bias is removed using stabilised experience replay, debate’s performance improves (see Figure 4b), though our ongoing and future work that tests additional learning algorithms and problem domains is likely to add further clarity here.

AI Control and Prover-Verifier Games

While we believe that the AI Control setting (Greenblatt et al., 2023) is an extremely important one and worthy of much greater attention, we would argue that this setting is importantly different from that of prover-verifier games (PVGs). The emphasis in AI Control is on detecting a malicious agent during pre-deployment testing. This has important implications that are both theoretical and practical. For example, the fact that the agent (the red team) is effectively in “simulation” means it must be modelled as memoryless. As an aside, the reviewer may be interested in concurrent work that formalises the AI Control setting (Griffin et al., 2024).

While one can enforce such restrictions upon PVGs, they are a more general model, subsuming, for example, debate (Irving et al., 2018) as well as other protocols (see, e.g., Hubinger (2020) for others). The emphasis in PVGs, however, is on training (or using) agents in a way that is robust to (potentially) partially misaligned agents, as opposed to being robust in the worst-case setting of a maximally misaligned, deceptive agent. In practice, these approaches are complementary: we might train an agent using a protocol (such as NIP) represented as a PVG before running pre-deployment tests as in AI Control, or we might want to test an agent using the AI Control methodology before using it with a PVG protocol (such as debate) once we know it is sufficiently safe to do so.

We thank the reviewer for their time in continuing to engage and further spell out their concerns with the paper. We address their key points in turn.

Conceptual Arguments

Zero-Knowledge

Regarding the relevance of zero-knowledge, we agree with the reviewer that this point is somewhat speculative. To further clarify the reviewer’s concern, we wish to ask whether it is primarily about:

1. The usefulness of having zero-knowledge protocols for model interactions at all;
2. Whether our proposed formalism is a reasonable way to characterise or learn zero-knowledge protocols for model interactions.

If the reviewer’s concern is regarding the first point, we argue that being able to ensure zero-knowledge interactions would, if feasible, be useful. In particular, let us consider three toy examples in which an individual employs a weak (trusted) verifier agent to interact with a strong (untrusted) prover agent that is provided by some model provider via an API:

• First and foremost, recent work has highlighted the risk of “model stealing” via black-box queries (Oliynyk et al., 2023). In other words, merely by interacting with the prover, a verifier can distill the model representing the prover (to gain more knowledge than is required to merely solve the task at hand).
• Another concern is that the verifier might be able to query the prover in a way that allows them to develop dangerous capabilities (Phuong et al., 2024; Jones et al., 2024). For example, a prover being queried about a chemistry problem might inadvertently leak information that enables the verifier to synthesise dangerous chemicals.
• Finally, proprietary models serving as provers may have learnt private information (either deliberately via instruction from the model provider or unintentionally because the information is in the pre-training dataset). It is important that we develop techniques to prevent the extraction of this data via query access (Carlini et al., 2020).

If the reviewer’s concern is regarding the second point, our justification for our proposed model is that it is (more or less) the closest possible analogue to the theoretical definition of zero-knowledge (as proved formally in Theorem 3). While it may be possible to approximate this and/or use a different model, we view this as a reasonable first step in establishing a principled theoretical foundation for future applied work.

If the reviewer’s concern about the relevance of zero-knowledge is regarding neither the first nor the second point, we kindly welcome them to further clarify their concern so that we can better understand its nature.

AI Control

Regarding control, we apologise for any lack of clarity here. In our original reply, we were referring to control evaluations specifically, which is listed by Greenblatt et al., (2023) as their primary contribution (“We describe a methodology to evaluate protocols that try to ensure safety despite intentional subversion”). We also note that as the third contribution listed in their paper, however, that they also introduce novel “[s]afety protocols and attack policies”.

The reason we referred to control evaluations specifically was that we took this to be the “formalism” that the reviewer was referring to. The point of these evaluations (as with virtually all dangerous capability evaluations) is that they take place before deployment (though this, of course, does not diminish the importance of additional run-time monitoring and oversight post-deployment). This is indeed evidenced by quotes from Greenblatt et al., (2023), e.g.:

• “During the [control] evaluation, we aren’t trying to get the model to do actual useful work, and so the model doesn’t need to have access to dangerous affordances. So it should be possible to run the [control] evaluations in a much more secure and safe environment than the model will be run in during deployment.”
• “Running the control evaluation needs to be much cheaper than running through all of deployment while still handling untrusted model strategies that involve rarely doing bad actions.”

AI Control

While we agree with the reviewer that the AI Control paper does spell out the nature of each interaction protocol, we do wish to stress that formally modelling such settings (as we do in our paper) can still be important. For example, Griffin et al. (2024) (the authors of which overlap with the original paper on AI control) formally model control evaluations as a partially observable stochastic game and use this model to introduce Pareto-improvements to the protocols originally studied by Greenblatt et al. (2023).

We also agree with the reviewer that the main difference between our paper and the works on AI control is that “the control evaluation methodology explicitly models some models as behaving adversarially with respect to the utility of the protocol designer, while [our] formalism assumes the models just myopically optimize reward”, and that the latter is “an interesting and important setting to study”. We advance previous work by making the following contributions:

1. A unifying game-theoretic framework that generalises existing neural IP protocols;
2. Several new neural IP protocols, including those that allow for zero-knowledge proofs;
3. A theoretical and empirical comparison of both new and existing protocols;
4. An extensible codebase for testing different protocols in different domains.

We would argue that the concurrent related works of Kenton et al. (2024), Khan et al. (2024), Kirchner et al. (2024), and Arnesen et al. (2024) complement but by no means obsolete or significantly diminish these contributions.

Empirical Results

We agree with the reviewer that a reasonable way to trade off precision and recall would be applying a nonlinear function to the original output of the protocol. Though to the extent that the precision and recall between different protocols differed so widely in our experiments and that – to the best of our knowledge – the breakdown into precision and recall has not been studied by other works that use these protocols, we still view it as worthwhile to bring this point to the attention of other researchers, as this implies that such subtleties might also apply to prior work. We hope that future work on various proof protocols will also watch out for this and take it into account more directly, as the reviewer suggests.

Thanks once again!

We thank the reviewer for their continued engagement as the discussion period draws to a close. Due to the deadline, this will be our last chance to reply. We hope that even if the reviewer does not believe that every single issue with the paper has been resolved, that our responses further above and below have convinced them that all things considered, our paper still makes sufficient contributions to meet the bar for acceptance. If so, we kindly ask them to consider updating their score.

Zero Knowledge

Thank you for the further clarification regarding your concern (and thanks also to Reviewer ZrkB for chiming in here!). We will try to better illustrate why we think the use of zero-knowledge protocols may be helpful in addressing the problems we identified by describing one of our examples in slightly more depth. First, recall that the key properties of a zero-knowledge interactive proof are as follows:

• Validity: Roughly, a trusted verifier $v$ can interact with an untrusted prover $p$ in order to (with high probability) solve a specific task $T$. In the classical setting, $T$ is typically formalised as a decision problem, where we must classify instances $x$ as positive or negative, but this can be generalised to other kinds of problems.
• Zero-Knowledge: For a given instance $x$, $v$ only learns the classification of $x$ when interacting with $p$, not any other information. In the classical setting, this is (roughly) formalised by saying that there is no adversarial verifier $v’$ that can interact with $p$ in order to solve tasks beyond what they ($v’$) could solve with an oracle for $T$.

Now, let us connect this to our examples. For the sake of illustration, we consider the second example, but similar analogies can be made in the other two cases. Suppose that we have the following:

• $p$ is a powerful proprietary model developed by a major AI company to serve as a general purpose scientific assistant.
• $v$ is a weaker personal software assistant used by an individual that can interact with $p$ via an API. (We also think that Reviewer ZrkB’s suggestion of an external auditing agent could be used here.)
• $T$ involves classifying different chemical compounds based on complex features of their underlying structure. For example, $T$ could involve classifying chemicals based on what colour dye they will produce when combined with another chemical. (We apologise if this example is a little naive – we are not chemists – but we hope that the reviewer can at least imagine a similar kind of benign task.)

Ideally, we would like $v$ to only be able to perform task $T$ by interacting with $p$. We would not, for instance, like them to be able to repeatedly query $p$ in order to learn how to synthesise dangerous novel chemicals (assuming that simply being able to solve $T$ would not otherwise allow them to do this). In other words, we would like $p$ to adopt a strategy that makes the protocol for solving task $T$ zero-knowledge.

A few remarks are in order:

• First, we note that this is clearly a large oversimplification of the risk we are truly concerned with, and that the zero-knowledge property is somewhat conservative in this context (as there are presumably other kinds of benign information that we wouldn’t mind if $v’$ extracted). At the same time, we think it would be beneficial to have a principled, theoretical foundation for future work that at at least attempts (as the concept of zero-knowledge does) to answer questions such as:
  • What does it mean for one model to gain knowledge from another?
  • How would we measure this knowledge gain?
  • What sorts of training regimes might, in principle, reduce this knowledge gain to its minimal level while still enabling the solving of a particular task?
• Second, we note that the “threat model” here is slightly different to the main topic of study in our paper, where the risk is the untrusted prover misleading the trusted verifier, not the possibility of an adversarial verifier extracting extra information from the prover (whether that prover is trustworthy or not). We apologise if this was unclear and will be sure to update our paper to mention this. Still, as pointed out by Reviewer ZrkB and as is hopefully made clear by our examples, we expect this threat model to be a significant one in the years to come, and one that can be neatly captured using prover-verifier games.
• Third, as we emphasised in our original reply, we do not mean to suggest that the precise training setup we provided in order to learn zero-knowledge neural interactive proofs completely solves these problems. Rather, we hope this idea provides a novel lens on an important problem, and that it might help to inspire new solutions. This is consistent with Reviewer ZrkB’s remarks that our initial suggestions in this paper could be complemented in future work by learning-theoretic bounds, for example, as well as further practical exploration and experimentation.