Learning to Give Checkable Answers with Prover-Verifier Games
Authors: Cem Anil
Guodong Zhang
Yuhuai Wu
Roger Baker Grosse
Venue: ICLR 2022 Submitted (2022)
Keywords: AI Safety
verifiable learning
robustness
adversarial learning
proof systems

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 applications. We propose Prover-Verifier Games (PVGs),  a game-theoretic framework to encourage neural networks 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 several variants of the basic framework, including both simultaneous and sequential games, and narrow the space down to a subset of games which provably have the desired equilibria. We then develop practical instantiations of the PVG for several algorithmic tasks, and show that in practice, the verifier 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 message is directly optimized to convince the verifier.

Under review as a conference paper at ICIR 2022
LEARNING TO GIVE CHECKABLE ANSWERS WITH PROVER- VERIFIER GAMES
Anonymous authors Paper under double-blind review
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), game-theoretic framework to encourage learning agents to solve de- cision problems in a verifiable manner. The PVG consists of two learners with competing objectives: trusted verifier network tries choose the correct answer, and 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 frame- work, including simultaneous and sequential games, and narrow the space down to a subset of games which provably have the desired equilibria. To complement our novel learning problem, we propose rigorous methodology for evaluating the robustness of the learned protocol. We develop instantiations of the PVG for two algorithmic tasks, and provide empirical evidence that the verifier robust decision rule that able 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.
in fact learns
INTRODUCTION
The astonishing performance of today's 's dominant learning paradigm optimizing powerful differ- entiable function approximators to minimize suitable loss functions often comes at the cost of poor robustness and reliability. It is common for powerful deep learning systems to be vulnerable adversarial attacks (Goodfellow al., 2015), display erratic behaviour on out-of-distribution data and be very confident of wrong predictions (Che et al., 2021). How can we train our learning algorithms to produce outputs that can be checked by humans or by learning algorithms that are cheaper or better understood?
Over the past decades, the field of computational complexity has greatly expanded our notion of proof to include formalisms such interactive, coowldnweedge, and probabilistically checkable proofs (Goldreich, 2008). Most of these notions can be thought in terms of game between a powerful but untrusted prover and a computationally limited but trusted verifier. Taking inspiration from this, we propose the Prover- Verifier Game (PVG), where two learning agents play the role of prover and verifier, and are allowed converse. The verifier aims to determine the correct answer a decision problem, and the prover aims to convince the verifier of particular answer (regardless its correctness). Since the prover is untrustworthy, the verifier will only find its messages useful to the extent that it can independently verify the information. If all goes well, then the game dynamics will lead to proof protocol which, if not mathematcallly sound, is at least sufficient for the whole system to achieve more reliable predictions than the verifier can achieve unaided.
We analyze the desirability the game equilibria implied by several variants of the Prover- Verifier Game concept and narrow the space down to a subset of games that theoretically have the desired equilibria. Picking the right game equilibrium concept turns out to be essential: we prove that formulating the PVG as sequential game in which the prover agent plays first leads to dysfunctional solutions. On the other hand, the simultancous (connected to Nash equilibria) and verifier-firs first sequential formulations (connected to verifier-leading Stackelberg equilibria) have desirable equilibria. We formally show, on illustrative problem, that gradient based differentiable game optimizers can find desirable proof-verifie verification protocols.

---

Under review as a conference paper at ICIR 2022
Do reliable justification protocols emerge in practice if we let artificial agents play the Prover- Verifier Game? To complement our novel game formulation, we develop rigorous evaluation methodology whereby the verifier is frozen and the prover (or the message) is optimized to convince the verifier. We then run simulations on two algorithmic tasks using a practical instantiation of the PVG concept. As predicted by our theory. PVG-trained verifiers learn to receive useful and reliable information from untrusted provers by following sensible verification protocols, whereas those trained alongside fully collaborative provers are easily deceived.
BACKGROUND
2.1 INTERACTIVE PROOF SYSTEMS (IPS)
Interactive proof systems generalize the notion of mathematical proof dialogue between two agents a prover and a verifier - to solve a decision problem (Arora & Barak, 2009; Thaler, 2019). The verifier agent, who is trustworthy but computationally constrained, is tasked with producing a correct answer to the decision problem. It can exchange messages with computationally unbounded, yet potentially adversarial prover agent. The communication protocol between the prover and verifier constitutes an interactive proof system if and only if it sound and complete:
Definition (Completeness and Soundness), The verifier of an interactive proof system is complete iff there exists a prover that can always convince the verifier that the answer is "yes", the correct answer is "yes". It is sound iff there doesn't I exist prover thut can trick the verifier into answering "yes" if the correct answer is "no".
2.2 DIFFERENTIABLE GAME OPTIMIZATION
A two-player differentiable game consists of two agents whose strategies are parametrized by w (W1. w2) E R2d that take turns minimize their differentiable loss functions (C1, L2) : Rd - R. An equilibriun concept determines which strategies will be adopted by the players. Nash equilibrium is achieved when no player can unilaterally improve its objective function.
Definition 2 (Nash Equilibrium (Von Neumann & Morgenstern, 2007)). The strategies parametrized by (wi, w2) constitute Nash equilibrium' of the two-player sequential differentiable game with loss functions L2) Rd -> R if they minimize their loss functions keeping the other player's 's parameters fixed:
w arg min Li (W1, w
W arg min
(1)
The notion of equilibrium considered by Generative Adversarial Networks (Goodfellow et al., 2014)
an example a Nash Equilibrium. Stackelberg equilibriam differs from the Nash equilibrium that one of the players is deemed the "leader" and the other the "follower" (Wang* et al., 2020). It is assumed that the follower always picks the optimal strategy for given leader strategy. In response, the leader modifies its strategy by factoring in how the follower agent will respond to the modification.
Definition (Stackelberg Equilibrium (Fiez et al., 2020)). Let W parametrize the strategy of the "leader agent" and wa parametrize that of the "follower agens". The loss functions the agents are L and La respectively. The strategies parametrized by (W1, wz) constitute a Stackelberg equilibrium and only (1) the follower's strategy is optimal given the leader's strategy, and (2) the leader's 's strategy optimal taking into consideration how the follower will respond to modifications.
wi= arg min Li (W1, wi(w))), w2(W1) = arg min L2(Wi, w2)
Wi
3 PROVER- VERIFIER GAME
The Veveer-erifeer Game aims to learn decision rules with a reliable internal verification step. We describe what we mean for verification protocol to be reliable, then outline the game formulation.
3.1 DESIDERATA AND PROVER-VERRE VERIFIER INCENTIVES
Desiderata: Designing the right prover-verifier game requires precisely defining what desirable outcome/equilbrrumm of the game looks like. With the "completeness" and "soundness" definitions mind (Section 2.1), we list the properties we seek in a desirable verifier protocol:
We assume uniqueness of equilibria for simplicity.
2

---

Under review as a conference paper at ICTR 2022
Prover
Prover
Message
Message
Verifier
Verifier
(a) Pattern to detect.
(b) When the pattern exists.
(c) When the pattern doesn't exist.
Depiction of mroof-verificttion protocol learned via Prover- Verifier Training. When trained on the task of detecting whether there's 's blue plus pattern (la) in the imput image, Prover- Verifier Training discovers a coordinate-based verification protocol. If there's 's a plus (lb), the prover sends its coordinate, and the verifier accepts this certificate. If there's not a plus in the image (Ic), then the prover sends the coordinates of maximally convincing image patch, but the verifier rejects this certificate.
Figure 1:
image
There should exist a prover that can help the verifier achieve perfect recall - the ratio of true positive predictions to all positive examples.
Possibility of Perfect Recall:
Guarantee of Perfect Precision: There shouldn't exist any prover which can trick the verifier into achieving non-perfect precision the ratio of true positive predictions to all positive predictions.
"Possibility perfect recall" connected completeness, and implics that with right proofs, the verifier can achieve zero false negative rate. "Guarantee of perfect precision" is related to soundness and implies that the verifier always has zero false positive rate regardless of which proof is used.
Picking the right prover-verifier incentives: We propose to set up the prover-verifier game with the following incentive structure: the verifier is incentivized to always give the correct answer given decision problem, and the prover is incentivized to get verifier answer "yes" to the decision problem, regardless the correct answer. This structure encourages collaborative dynamics when the correct answer to the decision problem is "yes" (which is linked to recall) and encourages adversarial dynamics if the correct answer is "no" (which is linked to precision). As we will prove formally in Section 3.3, this incentive structure, when embedded in the right game setup with the right loss functions, can lead to a verificveiiiiation protocol that meets the desiderata.
3.2 DIFFERENT PROVER- VERIFIER GAME FORMULATIONS
Notation Let Px Px(x), Pr (v) and y' ~ (y-( random variables where have E IR= y {0, 1..,,... K) and 10. K). Let their joint distribution be Pn-
) be the input, verifier label and prover label
The prover agent Pw,, parametrized by w, R outputs conditional probability distribution (r(x(z) over real valued "message" vectors z E I conditioned on inputs. The verifier agent W parametrized by w, E R"= represents the conditional probability distribution P. 20 2) over the predicted labels E (0, 1, .... K) conditioned the inputs and messages
Loss Functions: We pick the following loss functions for the verifier and prover:
C. (x.. ampp(aa)) -- log =)]
(3)
C, E ((aaa/)))p. e (xpp))))) log =)]
(4)
Since we wish for the verifier agent to try and solve the problem to the best of its ability, we set Py to be the correct label distribution. Since we wish to incentivize the prover to try and defend
3

---

Under review as a conference paper at ICTR 2022
particular answer regardless of its correctness, we set (t' = where of E {0, 1,...: K} is the output that the prover is defending. In a decision problem, yf will be one of 0 or 1. One can consider variations on these loss functions by replacing the negative log with other functions that are convex and monotonically increasing. We prefer the aforementioned loss functions when the verifier agent represents a softmax policy over its outputs. This guarantees that the gradients vanish iff the agents fulfill their incentives (see Appendix A).
Suitable Equilibrium concepts: There are three obvious ways to set up the order in which the agents play (i.e. pick their strategies parametrized by w and w.. the Prover- Verifier Game: 1) The prover and verifier play simultaneously. 2) The prover plays first, 3) The verifier plays first. The simultaneous setup leads to picking Nash equilibrium as the equilibrium concept. The latter two lead to picking Stackelberg equilibrium, where prover or verifier is the leader and can therefore reason about how the opponent will respond to given strategy. Interestingly, as we show in Section 3.3, not all of these formulations lead to equilibria that satisty our desiderata.
When Instances Revealed: We can also arrive at different game formulation depending on whether the problem instances (i.e., the input and prover-veritee veriffre labels) are revealed the agents before or after they pick their strategics (i.c. weights). This leads to eight different game formulations: two from the simultaneous setup (before or after the simultaneous moves) and six from the sequential setup (before, in- betbeween and after the moves, for each of the two sequential formulations).
The design space of how the prover and verifier interact with each other large. We only consider the single-step, no feedback formulation throughout the paper and leave the analysis of other formulations as future work. Note that the single-step, no feedback formulation is related to NP proof systems and include sophisticated proof-verification protocols. We can also derive numerous PVG formulations by modifying the communication channel between the prover and verifier. Various decisions regarding the channel include: 1) If the channel stochastic or deterministic (and what kind noise there is) 2) Whether prover's 's messages are real valued vectors, or discrete tokens 3) Whether the prover and verifier use an already constructed communication protocol, such as natural language.
How the Prover and Verifier Interact:
3.3 PVG FORMULATIONS WITH DESIRABLE EQUILIBRIA
We list in Table 1 all possible game instantiations obtained by varying the 1) player order and 2) when the problem instance is revealed. Our goal is to find which - if any - of these formulations have desirable equilibria. We consider the following abstract decision problem formulation to compare and contrast different PVG formulations:
Definition 4 (Abstract Decision Problem). Let X. M. (0,1) and - = (0,1) be the (discrete) sets of all imputs. prover messages, and labels, respectively. Let Px represent the input distribution. Assume the label is a deterministic function of the input, y = f(x), and the prover is always arguing for the label y = 1. The prover agent can choose a policy E P. where P is a set of mappings X + -M. Let V denote set of base verifiers, which are mappings X x M + {0, 1}. The verifier chooses policy U which computes a convex combination of elements of V. (The verifier's ouput can be interpreted as the probability it assigns to the label being 1). The verifier and prover try to minimize the loss functions defined in Equations? 3 and 4 respectively. We assume that both P and V include every constant mapping (i.e. ones which don't 't depend the input).
Assume that there exists a deterministic verifier policy 8² V such that:
7p E Cp:: Vv E X:: x² (II, = f(z) (completeness)
(5)
Yp E Cp:: Vz E X:: o" ((x)) =
f(x) = (soundness)
(6)
For instance, to represent decision problem from complexity theory, we could take X' and M to be sets of binary strings, P to be set of all mappings - M (the prover typically computatioually unrestricted), and V the set of mappings implementable by boolean circuits with some maximum size. However, we keep the formalism general because our main results don't depend on the details of boolean circuits complexity theoretic assumptions.
The conclusions of our thcoretical analysis displayed in Table 1. Proper proof-verification protocols constitute equilibria of only three of the eight game formulations: the simultancous setup where the problem instance is presented after the agents' moves, and the two verifier-fiss sequential setups where the problem instances are revealed after the verifier's 's move. We justify these claims through the following thcorems. The proofs are presented in Appendix B.
4

---

Under review as a conference paper at ICTR 2022
Table I: The summary of our theoretical results on the desirability of equilibria different PVG Tormulations. The "ordering" column illustrates in which order the prover and verifier pick their strategies (weights) and the problem instance (the input and labels) are revealed. The "necessity" and "sufficiency" columns show whether having converged to an equilibrium is necessary and/or sufficient for having discovered and complete and sound proof- verification protocol. The "failure mode" column describe in what way some of the setups lead to undesirable equilibria. The "convergence" column specifies if gradient descent converges to the eqilibrium on the Binary Erasure Channel Task. (*)We've ve only shown local convergence for the perifier-leading equilibria.
Ordering
Necessity Sufficiency
Failure Mode
Convergence
(Prover, Verifier). Instance Instance, [Prover, Verifier)
X
coordination problem trivial verifier
x
X
Verifier, Prover, Instance Verifier, Instance, Prover Instance. Verifier, Prover Prover, Verifier, Instance Prover, Instance, Verifier Instance, Prover, Verifier
/
V
none
/
V
none
/
X
X
trivial verifier
X
X
X
flood-the-zone
X
X
trivial verifier
X
X
trivial verifier X
X
Proposition 1. Any PVG formulation in which the verifier is given the problem instance before it selects its strategy has bad equilibria that having converged an equilibrium is neither necessary nor sufficient for having found a complete and sound proof verification protocol.
the instance is known when the verifier chooses policy, then the verifier can simply choose the constant policy which returns fz)) We dub this the "trivial verifier" failure mode.
Theorem 1. Consider all prover-leading sequential PVG formulations. Having reached a (prover leading Stackelberg) equilibrium is neither necessary nor sufficient for huving found complete and sound proof verification protocol.
The intuition behind this result is follows: matter what strategy the prover picks as the leader, the verifier can always find a strategy whose outputs match the label marginals (i.e. at least 50% accuracy if the labels are balanced). Due to the algehraic form of the prover loss function, the hest the prover can do is to avoid giving the verifier any information about the information whatsoever about the label. This defective incentive prevents the learning of proper proof-verification protocols. failure made, in reference the media disinformation strategies
We dub this the "food--the-nnn that pollute the information ecosystem to prevent people from knowing what's 's true Illing (2020).
Theorem 2. Consider all priifie-leaddng sequential PVG formulations in which the problem instance is revealed after the verifier picks its strategy. Having reached a (verifier leading Stackelberg) equilibrium is both necessary and sufficient for having found a desirable verifiitii protocol.
Necessary is easy to argue: given complete and sound protocol, neither player has incentive deviate. Sufficiency can be shown using a "proof by contrapositive" argument: If the protocol represented by prover and verifier is not complete and sound, then they cannot possibly represent a verifier-leading Stackelberg equilibrium, because the verifier can do strictly better by switching to the complete and sound verification system (as the prover will react by producing correct proofs).
Theorem 3. Consider the sinultaneous PVG formulation where the problem instance is revealed after the agents pick their strategies. Having converged to a (Nash) equilibrium necessary for having found a complete and sound proof-verificatti protocol.
the prover and verifier already represent complete and sound proo-verification protocol, the verifier's loss function is already minimized, hence the verifier won't 't change its strategy. Because the prover can already convince the verifier when it's acting collaboratively (due to completeness) and cannot fool when it's acting adversarially (due soundness), it also won't 't have the incentive to change its strategy. Therefore, the prover-verifee strategies constitute Nash equilibria. This also implies that all Stackelberg equilibria of the proof-verification game are also Nash equilibria: Corollary 1. All verifierleadding Stackelberg equilibria are Nash equilibria of PVG.
There might exist Nash equilibria that don't 't correspond to complete and sound protocols. For instance, the case in which the verifier completely ignores the prover constitutes a Nash equilibrium. We call this the "coordination problem" failure mode: no player can adopt protocol unilaterally.
5

---

Under review as a conference paper at ICIR 2022
3.4 FINDING PROOF- VERIFICATION STRATEGIES USING GRADIENT- OPTIMIZERS
Section 3.3 establishes that there exist PVG formulations whose equilibria, if found, will constitute complete and sound proof-verification protocols. Is there hope in finding these equilibria using gradient based differentiable game optimizers? We thereon use the phrase "Prover- refer to the general method of using gradient-based optimizers to solve for PVG equilibria.
Training"
To address the question above, we turn to simpler problem we call "Binary Frasure Channel" (BEC) which admits detailed analysis. The BEC problem is defined as follows:
We have prover-verifier system. The prover takes in input z E {0, I and attempts to convince the verifier to output 1 all the time whatever the input is. The verifier aims predicting the input correctly only based on the message from the prover. The prover defines a stochastic function
Definition 5.
f: [0.1] + {0, 1..... K} & M and is parameterized by probability vectors p" [P .... Pkg] and p² Int. ..... Pic] while the verifier defines g -M- - {0, 1] and is parameterized by q E R -g with
9: representing the probability of predicting when receives token i E .M.
We impose some further restrictions: the prover cannot send the message 1 when x 0 and cannot send 0 when 1. With this restriction, the communication channel between the prover and verifier resemble the hinary erasure channel Cover (I (1999) with the tokens ( K}} representing multiple erasure tokens. This setup is simplification of the more general assumption that there exists a complete and sound verification protocol that is realizable by the prover and verifier. In this setting (given loss functions in Eq. equation 3 and equation 4). the joint strategy of prover sending the right proof with pl 1 and verifier proceeding with @1 1 but q: 0 for all & 1 is Nash equilibrium.
Moreover, we add entropy regularization (i.e.. label smoothing) to the verifier loss avoid degenerate cases in training. We can show that running standard gradient descent converges to the ideal joint strategy under the simultaneous game formulation. In more detail, we have the following theorem.
Theorem 4. Starting from any initialization with v. > 0.p. > fofor all i E .M. running gradient descent on both prover and verifier with reasonable learning rates, the prover would converge only sending message when x = while the verifier would predict only if it receives mexsage 1 from
the prover. To put it differently, pi = 1 when converge while qı = 1 - C and qo = 92
QK c
with a small constant depending on the strength of entropy regularization.
Formulating the PVG as sequential game in which the prover agent plays first leads to undesirable solutions. We summarize the the result below.
Theorem 5. Starting from any initialization with ye > 0.p; > for all i E M, rumning gradient descent on both prover and verifier with any learning rates, prover would converge to only sending message 2 to K no matter what the input is.
4 RELATED WORK
Computational Complexity: Much of computational complexity theory is centered around various notions of proofs, from the hasic definition of NP to more modern notions of proof such as interactive, zero-knowledge, and probabilisticalyy checkable proofs (Goldreich, 2008). These various notions of proof can be understood in terms of a game between a prover and verifier somewhat analogous to ours. Our game is most directly analogous to the vanilla notion of proof used to define NP. But given the right architecture, our game would allow the prover's message to encode the weights a network that answers the verifier's 's questions, thereby more closely resembling an interactive proof.
Interpretabillity: Selective rationalization is the task of highlighting input features that are useful for classification. A number of game theoretic selective rationalization methods have been proposed (Lei al., 2016; Yu et al., 2019; Chang al., 2019). With text applications in mind, Lei et al. (2016) propose two player, collaborative game where a generator network selects relevant features from the input text, and a predictor network does classification using those features. Chang et al. (2019) propose a six player game where the 4 generators select factual or counterfactual rationales, and the 2 discriminators aim to distinguish factual and counterfactual rationales. In practice, only 3 players are instantiated (two generators that only take negative or positive examples and a discriminator). Game theoretic approaches have also been used for interpretable fact-checking on knowledge graphs. Hildebrandt et al. (2020) propose solving the triplet classification task (deciding whether a subject- predicate-object triple is contained in knowledge graph) using debate dynamics. Two reinforcement
6

---

Under review as a conference paper at ICIR 2022
learning agents learn to generale arguments (paths a knowledge graph) that either support or go against a fact (a triple). These are then fed to classifier trained to ascertain the truth value of the fact.
Verifying correctness and functional properties of models: There's a growing body of literature aimed at verifying both the correctness and/or functional properties of learned models. Goldwasser al. (2021) investigate interactive proof systems to verify correctness. They show cases where PACº verification of hypotheses are significantly more sample efficient, even when using a single-round protocol. Works that aim to verify functional properties of models (such as robustness to adversarial perturbations) can be categorized under three groups (Kohli et al., 2019): those that test consistency with specifications (Ruderman et al., 2018; Uesato al., 2018), those that train specification consistent models (Raghunathan al., 2018; Wong el al., 2018: Mirman et al., 2018: Dvijotham al., 2018) and those that formally verify adherence to specifications (Katz et al., 2017: Dvijotham et al., 2018; Singh et al., 2018). These works are orthogonal our notion of verification differs from that of the software analysis/verifiaaiion community that is concerned with showing models/picces of code meet specifications for all inputs as we aim learn proof mrof-verifiiation protocols to solve a given task.
Being able to verify the correctness of the outputs produced by powerful but potentially ad- versarial or brittle learning systems is a top objective of the Al Safety community. Irving et al. (2018) propose a two player debate game where two agents communicate (space-con conseeconstrained) statements to convince the judge of the correctness of opposing statements, Our approach is different in that it uses only single debater (prover). We also differ significantly in our focus: while Irving et (2018) believed the presence of adversarial debaters would itself lend robustness, we are more interested using the system to discover proof protocols. We believe the latter philosophy captures the spirit of the adversarial debate game from the rationalist community (Barnes & Christiano, 2020), which is intended determine which forms of (human) argumentation lead most reliably to true conclusions. Che et al. (2021) I) propose Deep Verifier Networks, which uses a conditional variational autoencoder detect "unreliable inputs or predictions." Unlike our approach, this approach hard-codes the structure of the verification algorithm, and considers out-of ofstiribibtttionnnnnnooooo detection applications.
Al Safety:
5 SIMULATIONS
5.1 PRACTICAL DESIGN DECISIONS
We elaborate on some design decisions we made for running prover-verifier training in practice.
Practical Constraints on the Verifier: If the verifier agent is instantiated using neural networks, then one can constrain the verifier by varying the architecture and/or reducing the size and depth of the network. While picking a suitable verifier constraint on toy problems might be tricky, we argue that this no longer remains an issue if the decision problem is inherently difficult to solve. For example, it is easy to find verifier architecture that cannot solve problems that have large search spaces (such as subset sum, SAT problems, or problems in NP in general), yet can check the proofs.
Picking the Differentiable Game Optimizer: We use standard gradient based optimizers (such Adam (Kingma& & Ba. 2014)) with alternating updates to find the equilibria of the prover-verife game, since it was shown by Zhang et al. (2021) I) that simple alternating gradient descent-ascent is on par with more sophisticated algorithms for adversarial games. We suspect that some advances in the optimization of generative adversarial networks could help, and leave this as future work.
Since computing the response gradients required to solve for Stack- elberg equilibria is often computationally challenging, we opt solve for Nash equilibria our simulations. Since all Stackelberg equilibria of the proo--erification game are also Nash equilibria, it is a viable strategy to find Nash equilibrium then check whether it also corresponds to verifier- lcading Stackelberg equilibrium. Also, the convergence properties of the simultaneous setup are favourible, as suggested by Theorem
Solving for Nash Equilibria:
Training Heuristies:
We list heuristics that improve speed and stability of training in Appendix D.
5.2 EVALUATING SUCCESS
The aim of the PVG is to produce proof system which is both sound and complete. If this is the case, then we can expect the verifier to achieve high accuracy. However, the verifier's accuracy
'Probably Approximately Correct (Valiant, 1984)
7

---

Under review as a conference paper at ICIR 2022
Table 2: (Precision and Recall on Binary Erasure Channel Task:) We froze the verifier networks obtained via. Prover-Verifier Training and collaborative training and evaluated their precision and recall against both optimized prover and directly optimized messages. The PVG-trained verifier achieved perfect specificity, whereas the collaborative-traieed verifier achieved exactly specificity.
Frozen Verifier Recall
Frozen Verifier Precision
PVG
Collaborative
PVG
Collaborative
Against Optimized Prover 1.0
1.0
1.0
0.0
Against Optimized Messages
1.0
1.0
1.0
0.0
during training does not constitute good yardstick for evaluating success, since a high accuracy for the verifier could instead reflect problematic game dynamies. For example, high accuracy be explained by the verifier detecting the prover's "tell" (spurious features in prover messages that correlate with the lahels) rather than checking the proof. Also, we would like the proof protocol to generalize upwards to provers that are more capable than the one seen at training time.
Therefore, we propose to stress-test the robustness of the verifier by freezing it and giving a lot more resources to the prover. We did this in two different ways: First, we would freeze the verifier and continue train the prover. Second, would initialize messages the prover's 'ss output and directly optimize the messages (to maximize the verifier's s acceptance logit) using powerful optimizers, such as L-BFGS. Both of these techniques remove the verifier's ability to recogmize the prover's 's tell, and also provide degree of confidence in the robustness of the proof system. (It remains possible that there exist incorrect proofs which the verifier would accept but which difficult to find.) We report the precision and recall of the frozen verifier against the two methods augmenting the prover.
The stress-tests outlined above can be seen as a way of checking the verifier represents a verifier- leading Stackelberg equilibrium. Optimizing the prover corresponds to the setup where the problem instance is presented after agents pick their strategies. Optimizing the prover messages links to the setup where the instance is known to the prover (see Table 1).
We emphasize that proposed evaluation methodology is essential to measuring progress on this problem: early on in our investigations, we were fooled into thinking the networks had learned a correct protocol because the verifier achieved high accuracy during training. However, we later determined that this high accuracy simply reflected the verifier learning the prover's 's "tell" faster than the prover learned to hide it. Since prior work aiming at similar goals to ours (Irving et al., 2018; Perez et al., 2019) reported only final accuracy during training, we consider our frozen verifier evaluation methodology an important contribution.
5.3 RESULTS
Binary Erasure Channel Experiments: We used the binary erasure channel (BEC) task described in Section 3.4 Definition as a test bed to check whether our theoretical results on the desirability of equilibria are matched in practice. We parametrized the prover as a small fully connected network that takes mn--hot-encoded input bits [1, O] or [0. 1] as inputs and outputs logits over the K = 16 communication tokens. The verifier was instantiated as a small network that takes in the one-hot encoded communication tokens inputs and outputs logits that are used to compute the probability the verifier assigns to the labels O and We sampled the input bits uniformly, which means the labels were balanced. We used the Adam optimizer (Kingma & Ba, 2014) with its PyTorch defaults (Paszke et al., 2019), batch size of 2000 and learning rate of 0. 0.0033. We updated the verifier 5 times for every prover update. Details about training setup are described in Appendix E.
To assess completeness and soundness, we computed the frozen verifier precision and recall against 1) a fully optimized prover and 2) fully L-BFGS optimized message vectors. The details for how we optimized the prover and message vectors are given in the Appendix E. We compared these results with those obtained using prover and verifier agents trained fully collaboratively (i.e. prover's 's labels always matches with the verifiers). The results, shown in Table 2, reaffirm our hypothesis that the PVG-trained frozen verifier achieved perfect precision and recall both against the optimized prover and optimized messages. The collaboratively trained verifier had zero precision, hence is not robust.
In Figure 2, we visualize how the outputs (i.e. logits) of the prover and verifier networks for each different input evolve over time, accompanied by the accuracy of the verifier. We highlight - with bolded blue and orange curves how the prover and verifier treat the special "0" and "1" tokens. The
8

---

Under review as a conference paper at ICLR 2022
Table 3: (Precision and Recall on Thnd-The-Plus Task:) We froze the verifier networks obtained via Prover- Training and collaborative training and evaluated their specificity and recall against hoth optimized prover and directly optimized prover messages. The PVG-trained verifier achieved near-perfect specificity against the optimized prover and optimized messages. The specificity of the baseline was zero in all cases.
Frozen Verifier Recall
Frozen Verifier Precision
PVG
Collaborative
PVG
Collaborative
Against Optimized Prover
1.0
1.0
1.0
0.0
Against Optimized Messages
1.0
1.0
0.99
0.0
verifier quickly picks up on the fact that receiving "0" is indicative of the label being "0", Shortly thereafter (around iteration 400) the verifier learns the desired verification protocol.
FindTThePlus Experiments: We tested the efficacy of prover-verifier games on visual search task we call "FindThePllus. As in Figure the dataset consists of binary x bluc-red images that contain single 3 x plus pattern in them. Labels are determined by the color of the plus: images with red plus are assigned to class 1 and images with blue plus are assigned to class 0. The verifier is constrained to only process a portion of the prover advise it "where to look" (advice which parametrized the prover as a convolutional net followed by a fully connected layer. We parametrized the verifier with Spatial Transformer Network- like (Jaderberg et al., 2015) architecture with multiple heads.
Prover-Verifiee Verifier Training Dynamics on Binary Erasure Task
Provrr Loyks
MARL abbut cyts
the input image, so it depends
Velial
whold
free to ignore).
11
The training details are provided in Appendix E,2. The frozen verifier precision and recall corresponding Prover- Prover-Verifier training, well as collaborative training are shown Table 3. We optimized the prover and the messages using the same setup we used in the Binary Erasure Channel experiments. As before, the verifier trained under the prover- verifier game dynamics achieves perfect pre- cision against the optimized prover, while the verifier trained under the standard, collabo- rative learning dynamies achieves exactly precision. The frozen verifier precision was 0.99 if we directly optimized the proof vec- tors. We visualized where the Prover- Prover-Verifier trained verifier looks using the proof vectors from the prover. An example is displayed in Figure I (more in Appendix E.2). These vi- sualizations indicate that not only does the prover send the coordinate of the blue plus whenever it exists, it also sends the coordinates of maximally convincing patches if there's not blue plus in the image.
100
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.
6 CONCLUSION
We proposed Prover- Veriffrr Games (PVG), game-theoretic framework to encourage neural networks solve decision problems in verifiable manner. We provided a space, and eliminated game formulations that have undesirable equilibria. Using a rigorous evaluation framework, we demonstrated both theoretically and empirically that there exist PVG formulations that can learn robust proof- vroff-veriiiiation protocols in practice.
thorough analysis the problem
9

---

Under review as a conference paper at ICLR 2022
REFERENCES
Sanjeev Arora and Boaz Barak. Computational complexity; a modern approach. Cambridge Univer- sity Press, 2009.
Jimmy Lei Ba, Jamie Ryan Kiros, and Geoffrey E Hinton. Layer normalization. arXiv preprint
1607 06450. 2016.
Beth Barnes and Paul Christiano. Writeup: Progress on Al safety via. debate. LESSWRONG, 2020.
URL https://wwet http://wwwwsswwwggggg.. http://pttp/////////a/eeee/////e
Shiyu Chang, Yang Zhang, Mo Yu, and Tommi Jaakkola. game theoretic approach class-wise selective rationalization. Advances Neural Information Processing Systems, 12:10055-10065, 2019.
Tong Che, Xiaofeng Liu, Site Li, Yubin Ge, Ruixiang Zhang, Caiming Xiong, and Yoshua Bengio. Deep verifier networks: Verification of deep discriminative models with deep generative models. In AAAI, 2021.
Thomas M Cover. Elements of information theory. John Wiley & Sons, 1999.
Krishnamurthy Dvijotham, Sven Gowal, Robert Stanforth. Relja Arandjelovic, Brendan O' D'onoghue, Jonathan Uesato, and Pushmeet Kohli. Training verified learners with learned verifiers. arXiv preprint arXiv:1805. 10265, 2018.
Tanner Fiez, Benjamin Chasnov, and Lillian Ratliff. Implicit learning dynamics in Stackelberg games: Equilibria characterization, convergence analysis. and empirical study. In Proceedings of the 37th International Conference on Machine Learning, 2020.
Oded Goldreich. Prohabilistic proof systems: A primer. Now Publishers Inc, 2008.
Shafi Goldwasser, Guy N Rothblum, Jonathan Shafer, and Amir Ychudayoff. Interactive proofs for verifying machine learning. In 12th Innovations Theoretical Computer Science Conference (ITCS 2021). Schloss BegstuuhlL-cbbnii-7eettm für Informatik, 2021.
Ian Goodfellow, Jean Pouget-Abadie, Mehdi Mirza, Bing Xu, David Warde-Farley, Sherjil Ozair, Aaron Courville, and Yoshua Bengio. Generative adversarial nets. In Advances in neural information processing systems, pp. 2672-2680, 2014.
Ian J. Goodfellow, Jonathon Shlens, and Christian Szegedy. Explaining and harnessing adversarial examples. In 3rd International Conference on Learning Representations, 2015.
Marcel Hildehrandt, Jorge Andres Quintero Serna, Yunpu Ma, Martin Ringsquandl, Mitchell Joblin, and Volker Tresp. Reasoning on knowledge graphs with debate dynamics. In Proceedings of the AAAI Conference Artificial Intelligence, volume 34, pp. 4123-4131, 2020.
Sean Illing. "flood the zone with shit": How misinformation overwhelmed our democracy. Vox, 2020. URL https: /www, vox . wwtpc//ccpppccccoooo wappooyyyyyyaaaaaea and wtt.liiicc////oo/// 20991816/ wwwpacchent-trriiie wtttee-trrritttu---b--eee-e
Geoffrey Irving, Paul Christiano, and Dario Amodei. 1xXiv:1805.00899 2018
safety via debate. arXiv preprint
Max Jaderberg, Karen Simonyan, Andrew Zisserman, et al. Spatial transformer networks. Advances in neural information processing systems, 28:2507-20225, 2015.
Guy Katz, Clark Barrett, David I. Dill, Kyle Julian, and Mykel Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. In International Conference on Computer Aided Verification, pp. 97-117. Springer, 2017.
Diederik P Kingma and Jimmy Ba. Adam: A method for stochastic optimization. arXiv preprint arXiv:1413 1482.6980,..1 2014.
10

---

Under review as a conference paper at ICTR 2022
Kohli, Gowal, Dvijotham, and Uesato. Towards robust and verified AI: Specification testing, robust training, and formal verification. DeepMind. Medium, 2019.
Tao Lei. Regina Barzilay, and Tommi S. Jaakkola. Rationalizing neural predictions. In Proceedings of the 2016 Conference on Empirical Methods Natural Language Processing, EMNLP 2016. Austin, Texas, USA, November 1-4, 2016, pp. 107-117. The Association for Computational
Linguistics, 2016.
Andrew L Maas, Awni Y Hamnun, and Andrew Y Ng. Rectifier nonlinearities improve neural network acoustic models. International Conference on Machine Learning, 2013.
C Maddison, A Mnih, and Y Teh. The concrete distrihution: A continuous relaxation of discrete random variables. In Proceedings of the international conference on learning Representations, 2017.
Matthew Mirman, Timon Gehr, and Martin Vechev. Differentiable abstract interpretation for provably robust neural networks. In International Conference on Machine Learning, pp. 2018.
PMLR,
Rafael Müller, Simon Kornblith, and Geoffrey E. Hinton. When does label smoothing help? Advances in Neural Information Processing Systems, 32:4694-4703, 2019.
Jorge Nocedal and Stephen Wright. Numerical optimization. Springer Science & Business Media, 2006.
Vardan Papyan, XY Han, and David L Donoho. Prevalence of neural collapse during the terminal phase of deep learning training. Proceedings of the National Academy of Sciences, 117(40): 24652-24663, 2020.
Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, et al. PyTorch: An imperative style, high-performance deep learning library. Advances in neural information processing systems, 32: 8026-8037, 2019.
Ethan Perez, Siddharth Karamcheti, Rob Fergus, Jason Weston, Douwe Kiela, and Kyunghyun Cho. Finding generalizable evidence by learning to convince Q&A models. arXiv preprint arXiv:1999.0586. 2019.
Aditi Raghunathan, Jacob Steinhardt, and Percy Liang. Certified defenses against adversarial examples. In International Conference on Learning Representations, 2018.
Avraham Ruderman, Richard Everett, Bristy Sikder, Hubert Soyer, Jonathan Uesato, Ananya Kumar, Charlie Beattie, and Pushmeet Kohli. Uncovering surprising behaviors reinforcement learning via worst-case analysis. 2018.
Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. Fast and effective robustness certification. Advances in Neural Information Processing Systems, 31: 10802-10813, 2018
Justin Thaler. Interactive proofs (part i). 2019. URL httpst yout cttp:ee.oowwwtttttaeo v=2XroadirvwAst==22
Jonathan Uesato, Ananya Kumar, Csaba Szepesvari, Tom Erez, Avraham Ruderman, Keith Anderson, Krishnamurthy Dj Dvijotham, Nicolas Heess, and Pushmeet Kohli. Rigorous agent evaluation: An adversarial approach to uncover catastrophic failures. In International Conference on Learning Representations, 2018.
Leslie Valiant. A theory of the leamable. Communications of the ACM, 27(11):113411142 1984,
John Von Neumann and Oskar Morgenstem. Theory of games and economic behavior. Princeton university press, 2007.
Yuanhao Wang", Guodong Zhang*. and Jimmy Ba. On solving minimax optimization locally: follow-the-ridge approach. In International Conference on Learning Representations, 2020. URL https://opente net net/forumiddd-ik'" 1rkwS..

---

Under review as a conference paper at ICTR 2022
Nicholas Watters, Loic Mathee, Christopher Burgess, and Alexander Lerchner. Spatial broadcast decoder: A simple architecture for learning disentangled representations in vaes. arXiv preprint 1oXiv:990..00111 2019.
Eric Wong, Frank R Schmidt, Jan Hendrik Metzen, and Zico Kolter. Scaling provable adversarial defenses. In Proceedings of the 32nd International Conference on Neural Information Processing Systems, pp. 8410 8419, 2018.
Mo Yu, Shiyu Chang, Yang Zhang, and Tommi Jaakkola. Rethinking cooperative rationalization: Introspective extraction and complement control. In Proceedings of the 2019 Conference on Empirical Methods Natural Language Processing and the 9th International Joint Conference on Natural Language Processing (EMNL.-IICNILP), pp. 4094-4103, 2019.
Guodong Zhang, Yuanhao Wang, Laurent Lessard, and Roger Grosse. Don't fix what ain't broke: Near-optimal local convergence of alternating gradient descent-ascent minimax optimization. arXiv preprint arXiv:2102.09468, 2021.
A WHEN LOG-LOSS GRADIENTS VANISH
The gradients of the log-loss (i.c. the loss function used in Equations equation 3 and equation 4) vanish if and only if the agents fulfill their incentives (i.e. classity their labels conrectly). Let
l = (1 p(x)) E Rd be the logits that the verifier network ouiputs for input and prover message
p(x). S: Rd I2d
softmax operation with temperature [S(E)],
o5 We take
Σ e
S(E): to the probability the verifier assigns for the correct label to
Let y be the correct label. The verifier loss and its gradient with respect the logits can be given by:
e
J. = - log
Σ,
c
0J.
-11 E, c
(8)
O
54
the verifier assigns high probability to class y, then Σ, vanish. Otherwise, the gradient won't vanish. The derivation is identical for prover's loss.
will approach 1 the gradients will
PROOFS OF EQUILIBRIUM THEOREMS
Theorem 1. Consider all prover-leading sequential PVG formulations. Having reached a (prover leading Stackelberg) equilibrium is neither necessary nor sufficient for having found complete and sound verificaitnnnnnon protocol.
Proof. It suffices prove that the prover-leading Stackelberg equilibrium neither necessary nor sufficient for having found a complete and sound proof- verification protocol on the following decision problem:
Definition 6 (Simplified Binary Erasure Channel Problem), Let = = - {0,1} and M (0, 1, 2). Let the input distribution Fx be the uniform distribution over X, and let the label generating function be defined as y (x), That is. the label is identical to the imput. The prover is arguing for label y = 1.
The prover can choose between two policies Pı and Pz
0 r
[2 r
r
2 T T=1
The verifier can pick between three policies Un 02 and defined as follows:
12

---

Under review as a conference paper at ICIR 2022
0 m = 0
0 m = 0
1 m = 0
U1
1 m
02
0 m 1
V/
1 m =1
0
m 2
0 m 2
m=
Note that the mappings available to the verifier ignore the imput. Also note that the prover-veriiee pair (pi, v.) satisfy Equations 5 and 6.
Lack of Necessity: To show lack of necessity, it suffices to show that the complete and sound prover- verifier pair (Pı, 81) don't 't constitute a prover- prover-leading Stackelberg equilibrium. the prover picks pi. the verifier can attain exactly loss by assigning weight of to vn and a weight of to at and ag. In this scenario, the prover's loss will be infinity:
1 log 02(x = 0, p(x) = 0) log u2(a 1(x()) = 1) = +00
Jp = 2
2
On the other hand, if the prover picks policy P2, then its messages have exactly 0 mutual information with the imput. In this scenario. the best the verifier equal probability both outputs and 1. It can do this by assigning weight to ej and weights 0.5 to di and Vg., The prover's loss in this scenario is:
do to minimize its loss function is to assign
Jp
log 0.5 + 2 1.5
when X=0
when x=1
Since the prover can do better by picking P2 over Pl. the pair (p1, v1) doesn't constitute a prover- leading Stackelberg equilibrium.
Lack of Sufficiency: Consider the scenario discussed above where the prover picks pa, and the verifier responds by assigning 0.5 weight to 1/ and V3. This is Stackelberg equilibrium despite not corresponding to a complete and sound decision rule. This is because 1) p1 achieves the best prover loss given that the verifier
O
Theorem Consider all verifier-leading sequential PVG formulations which the problem instance revealed after the verifier picks its strategy. Having reached a (verifier leading Stackelberg) equilibrium is both necessary and sufficient for having found
found a desirable verfffieiiin protocol.
Proof. We first prove necessity, then sufficiency.
Necessity: By the problem definition, there exists a prover-verifier pair (p1,01) v1) that satisfy Equations 5 and 6, therefore constitute complete and sound proo--verficaaion protocol. Consider the scenario where the prover's 's policy is Pt. and the verifier assigns weight of to policy V1- These prover-verifier strategies constitute a (Stackelberg) equilibrium of the lerifier-leading sequential game formulation. This is because (1) p1 already achieves the smallest prover loss for the given verifier strategy (2) the verifier already achieves 0 loss and therefore has no incentive to change its strategy. To see (1), note that the verifier
never be fooled if the correct label is 0, so the prover cannot possibly lower its loss by changing to a different strategy. the correct label I, then the prover achieves loss by following P1. Therefore, the prover has no incentive to change its strategy.
Sufficiency:
To show that having reached a verifier-leading Stackelberg equilibrium implies a complete and sounds proof- veriiieiiiinntoon protocol, we follow a "proof by contrapositive" argument and prove, instead, that if the verifier is not representing complete and sound proof-verification protocol, it cannot possibly be a Stackelberg equilibrium.
Assume that the verifier assigns non-zero weight to a verification policy s" that neither complete and/nor sound. If it's not complete, then for v" there exists a label-1 input x such that there doesn't 't exists a prover policy that can convince the verifier that the correct label is 1. This will cause the verifier's 's loss to be nonzero. If it's not sound, then there exists a label-0 input for which there exists a prover policy that can fool the verifier answering 1. This will also cause the verifier's 's loss be nonzer. On the other hand, if the verifier assigns 0 weight to all non-complete nor non-sound verification modules, then it's loss will be exactly O. This implics that the verifier can do strictly better by switching to complete and sound verification protocol.
13

---

Under review as a conference paper at ICLR 2022
Theorem 3.
Consider the simultaneous PVG formulation where the problem instance revealed after the agents pick their strategies. Having converged to a (Nash) equilibrium is necessary for having found complete and sound preffftieii protocol.
Proof. Proving necessity for the simultaneous setup is identical to proving necessity of the verifier- leading Stackelberg setup.
The complete and sound prover-verifier pair (p1, 01) (i.e. the verifier strategy of assigning a weight of to 01) ). whose existence is guaranteed by the problem definition, form a Nash equilibrium.
If we fix the verifier strategy at v1, then the prover has incentive change it's strategy. In the collaborative case (when the input belongs to class 1. the prover already achieves loss. the adversarial case, the verifier is never fooled (by the soundness assumption) so the prover cannot improve its loss by switching to different strategy. Therefore. if we fix the verifier strategy, the prover wouldn't 't move.
If we fix the prover strategy at Pt, then the verifier already achieves 0 loss by following V1. Therefore it doesn't 't have an incentive move.
Therefore, the (pr, 21) pair form a Nash equilibrium.
Corollary 1. All verifter-eadiing Stackelherg equilibria are Nash equilibria of PVG.
Proof. Having reached a verifier-leading Stackelberg equilibria is sufficient for having found a complete and sound proof-verification protocol (by Theorem 2). A sound and complete proof- verification protocol already constitute a Nash equilibrium 3. Therefore, having reached a verifier- leading Stackelbeg equilibrium implies having reached a Nash equilibrium.
C PROOFS FOR EQUILIBRIUM ANALYSIS
Theorem 4. Starting from any initializaaionn with pi > O,P; > for all i E M, rumning gradient descent on both prover and verifier with reasonable learning rates, the prover would converge to only sending message 1 when x = 1 while the verifier would predict 1 only if it receives mexsage from the prover. To put differently, pt when converge while qı 1- and qo = Q2 = QK with c a small constant depending on the strength of entropy regularization.
Proof. First, we assume WLOG that K 2 because all these tokens from K "exactly" same for both prover verifier. So we do not concern about computation time, we can group tokens 2 - K as a single token. In this case, the only parameters for the prover is just p and pl. For notational convenience, we let a P8 and é pl. Further, we assume the learning rates TP & .y.. With two time-scale updates, one can show that the verifier would converge first. Given nondegenerate initialization and entropy regularization on g with coefficient À >> 0 (this is basically label smoothing), have
1 A 91
1-a A(2 a b) (2 - a
40
92
(9)
2X
1 2X
b-b () + 2X)
Recall that the objective of the prover is
L(a, b) = a log 9 log d0
(2 b) kog
(10)
Hence, we have the mean gradients of the prover
0L
1
X(2 b) llog (1 + A)(2
1- b
log q2
log 41 log
11
(11)
Za
b)
1 X(2 b)
0C
1 a + X(2 a b) log
1
log 42 log 900
log
(12)
0b
X(2 a b)
a X(2 a 6)
As long as < 1, b would keep decrease as the gradient w.r.t b in equation 12 is > 0. This further implics that the gradient w.n. is < 0 and hence would keep increasing until 1.
14

---

Under review as a conference paper at ICTR 2022
Further, we show a b < and q laking the values equation are the Nash equilibria of the game. It is easy to see the value are optimal given fixed a, b, so it is impossible to improve unilaterally for the verifier. On the other hand, we know log > log = log 42 if = I and 6 < 1, the prover could not improve either. This completes the proof.
Theorem 5. Starting from any initialization with p. > 0, > for all i E M, running gradient descent both prover and verifier with any learning rates, prover would converge only sending message 2 K matter what the input is.
Proof. From the viewpoint of prover, it is essentially single-objective optimization problem with the loss function in the following form:
1+A + 2A
1 X(2 - a
L(a, b) = a log
blog 1 2X - -(2 (2- a 6) log
(13)
(2 a b)(1 + 2A)
Surprisingly, the Stackelberg game formulation leads to bad joint strategy where the prover may send wrong messages with the input In particular. we have the gradient:
ac
1-b b
1-b b
log
+
(14)
du
+ X(2 a--ah b)
+ X(2 b)
Ac log
1-
(15)
X(2
+ X(2
By the identity log(1 2) < x. we immediately know that > and ac if * 1. Interestingly, this is exactly the opposite of the simultancous game. This immediately implies that b will converge to U. This completes the proof.
D TRAINING HEURISTICS
We find that the following design decisions make learning consistent and help speed up convergence, while not being essential for success:
Different Number of Gradient Steps per Agent:
We find that updating the verifier multi- ple times per single prover update helps. It is especially helpful in preventing the verifier from ignoring the prover's messages early in training. Note that proving Theorem 4 requires setting larger learning rate to the verifier.
Adaptive Prover Step Size: Adaptively increasing the prover-update frequency if the verifier's s accuracy surpasses pre-selected (i.c. 90 percent) value helps speed up the transition from "nearly robust" protocols to fully robust ones at the terminal phase of the training.
Pretraining the prover to solve the decision problem before initiating the prover-verifier game ensures that the first messages the verifier receives from the prover will likely contain features that correlate with the labels and therefore decreases the likeli- hood that the verifier will ignore the prover's 's messages. We do this by appending two extra heads to the prover that are trained to do solve the task at hand, as well as to autocncode the input.
Prover Pretraining:
E EXPERIMENT DETAILS
E.1 BINARY ERASURE CHANNEL EXPERIMENTS
Task Setup and Data Distribution: We picked there to be 16 communication tokens that the prover can communicate to the prover. We sampled the input bits uniformly, which mean the labels were balanced.
15

---

Under review as a conference paper at ICIR 2022
Prover Network: We parametrized the prover as two hidden layer fully connected LeakyReLU network with width 100 and LayerNorm (Ba et al., 2016) layers fully connected network. We used the Gumbel-softman trick (with constant temperature of 1) to sample (one hot encoded) communication tokens. We use the Striigh-Thhroug Gumbel Sofimax Estimator (Maddison et al., 2017) to backpropagate through the discrete sampling step.
one hidden layer, fully connected LeakyReLU neural network with width 100 and LayerNorm layers.
Verifier Network: The verifier was instantiated
Optimization setup: We used the Adam optimizer for updating both the prover and verifier with a learning rate of 01.003 and batch size of 2000. We updated the verifier 5 times for each prover update. We observed that training the prover to solve the classification and autoencoding auxiliary lasks doesn't 't have an impact on training, likely due to the simplicity of this task. We ran optimization until the verifier learned a complete and sound veoff-veriiiattin protocol (or, frozen verifier's precision and recall reached the value of 1)
Evaluation details: To train the prover against the frozen verifier, we use the Adam optimizer with a learning rate of 0.0003 for 500 gradient steps, which we found was enough to reach coverronvere, To optimize the prover messages directly, we use the Py Torch implementation (Paszke et al., 2019) of the LBFGS optimizer (Nocedal & Wright, 2006) with learning rate of I, history size of 300 and "strong Wolfe" line search. We terminate the optimization when either the L.1 norm of the change in iterates becomes less than 10e- 9, or when the LI norm of gradients become less than 10e- 5, or when the number of optimizer steps surpass 300. We found that the the tolerance-based termination criteria are met almost always before the maximum number of optimizer steps is reached.
Hyperparameter Optimization and Tuning: We tuned the following aspects of training 1) Optimizer (Adam SGD). 2) Learning rate (Ie-3, 3e-4, 1e-4), 3) Batch size (500, 2000), 4) Network width (32, 100) 5) verifier number of steps (1, 5, 10, 20, 50).
found that using Adam, the larger batch size of 2000 and a larger width of 100 for the networks were crucial. Setting the learning rate to be Se 4 and verifier number of steps to 5 stabilized training and made it more consistent.
Training hardware: Due to the low computational requirements of the BEC experiments, the experiments were run on an 2019 Modle MacBookPro with 8-Core Intel Core 19 processors.
E.2 FINDTHEPLUS EXPERIMENTS:
Task Setup and Data Distribution: We used 10 x 10 images with exactly one 3 x 3 plus patterns in them. The images were single-channel, and the pixel values were binary (i.e. 0 or 1). The plus patterns were either formed using 0-pixels or 1-pixels, which we refer "red" or "blue" plusses in the original text for additional clarity. The used balanced labels during training.
Prover Network: We parametrized the prover a hidden layer convolutional neural network with 40 hidden channels, kernel size 3. padding of and LeakyRel.U (Maas et al., 2013) nonlinearities followed by Instance Normalization layers. We passed the output of this convolutional neural network through mecan-polinn operation follow by linear projection layer that resulted in the message vectors. The message vectors were 32 dimensional.
We also trained the prover network to both solve the decision problem itself (i.e. classi- fication). as well as autoencode the inputs. did this by tacking "auxiliary heads" that process the output of the convolutional backbone described above and produce their outputs, We used a linear classification auxiliary head. For the autoencoding auxiliary head, we used Spatial Broadcast Decoder (Watters al., 2019) with 3 convolutional layers with 32 channels, kernel size of 3 and LeakyReLLU activations.
We parametrized the verifier with the Spatial Transformer Network- like (Jaderberg et al., 2015) architecture with 4 heads. This architecture lincarly transforms the prover messages into 2 3 matrices that parametrize what kind spatial transformation should be applied to the image. The transformed images are then fed into a final linear classifier that produces the verifier predictions. A schematic diagram of a single head of this architecture is displayed in Figure 3. We constrained the allowed spatial transformations to
Verifier Network:
16

---

Under review as a conference paper at ICT. 2022
Spatial Transform Params,...
Linear
Message
Spatial Transformation
Transformed
Prediction
Image
Linear
Image
Logits
Figure 3: FindTheePlus Verifier Architecture: A schematic diagram of single head of the Spatial Transformer Network-like verifier architecture we used in out FindThePlus experiments.
only include shifts, and hard-coded the rest to zoom in by a factor of 2, and have no rotation and shear. These constraints only serve to improve the clarity plus visualizations and allow inspect training- training still succeeds if remove these constraints. We used zero padding, if the verifier chose shift its gaze outside of the image.
Optimization Setup: We used the Adam optimizer for updating both the prover and verifier with learning rate of 0.0003 and batch size of 2000. We updated the verifier 1 times for each prover update. We observed that pretraining training the prover solve the classification task speeds up training considerably, while the autoencoding head doesn't have a significant impact. We adaptively incremented the prover's number of steps if the verifier's accuracy kept above 75% for 20 consequent game steps, and stopped incrementing when the prover's s number of steps reached 15. We ran pretraining using the optimizer settings, for 100 gradient steps (enough let the prover achieve around 80% accuracy).
We employed bit of Label Smoothing (Müller al., 2019) (with coefficient 0.05) to the verifier loss to regularize training. For pretraining prover classification and autoencod- ing auxiliary heads, we used the cross entropy loss and (pixelwise) mean squared error respectively. We kept training the prover to classify and autoencode throughout training. We report results at the point verifier achieved it's best frozen precision against directly optimized message vectors. Note that the verifier achieves perfect frozen precision against an optimized prover way before this point.
Evaluation Details: We used exactly the same evaluation setup used in the Binary Erasure Channel Experiments. We report the results the training checkpoint with the highest overall frozen verifier accuracy against optimized proofs, as the performance of the verifier tends to fluctuate all throughout training. We also report the best result amongst training runs initialized with four random number generator seeds.
Hyperparameter Optimization and Tuning: We used setup that worked best the Binary Erasure Taks and found that also yielded good results for the Find task. We re-tuned the number of verifier steps and found that updating the verifier less frequently (i.e once per prover step) doen't 't degrade performance, while speeding up convergence. We also tuned duration of prover pretraining.
found that pretraining the prover convergence actually hurts performance. We link this to the Neural Collapse phenomenon elaborated by Papyan et al. (2020) and leave more detailed examination to future works.
Training Hardware: We ran training using single NVIDIA P100 GPU with Intel Xeon
Silver processors.
E.3 ADDITIONAL PLUS VISUALIZATIONS
In Figure 4, we show more visualizations that display where the verifier looks at in the input images.
17

---

Under review as a conference paper at ICTR 2022
Blue Plus
Red Plus
inputs
verifier's gaze
Figure 4: Visualizing Verifier's Gaze: We visualized where each of the verifier's Spatial Trans- former heads learn to look at. The top displays the inputs. The left three inputs contain a blue plus in them (what the prover is defending). Each subsequent row corresponds to 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 convincing image patch.
18


Reviews:
[{"review_id": "unwDEW0K7hg", "reviewer": "Reviewer_uyg3", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 1, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "First of all, I have to admit that I am no expert in this area and hence I do not feel qualified to fully assess the merits of this paper. Also, for this reason, I find the paper really hard to follow. The presentation of the material does not offer a reader any help in this regard. The paper is not self-contained and a reader is supposed to go from one paper to another in hope of grasping what the authors are talking about.\n\nUnfortunately, what is worse is that the paper delivers not a single example of a game that the authors are talking about. I do believe this makes the presentation suffer a lot (granted that I am from a different research area). The notation and the problem being studied aren't exemplified nor well-motivated either (as an example, what is PAC verification?).\n\nHaving said that, the paper seems to offer a rigorous theoretical study with a wealth of propositions, theorems and their proofs (there are several appendices attached). (In this sense, I am inclined to think that another venue might possibly fit this work better than ICLR.) Additionally, theoretical findings are confirmed by experimental analysis performed.", "summary_of_the_paper": "Based on the ideas lying behind interactive proof systems (IPS), this paper proposes a prover-verifier games (PVG) framework, which aims at solving decision problems in a verifiable manner, where two learning agents interact with competing goals: a trusted verifier agent tries to get a correct answer to the problem while an untrusted (but more effective) prover tries to convince the verifier that its answer is correct, regardless of its actual correctness. The paper studies the framework under several (sequential and simultaneous) game scenarios.", "summary_of_the_review": "To summarise, although I personally find the paper close to impossible to follow, I don't really feel in a position to judge it based solely on this fact simply because I am not an expert in the area, and it is unclear to me what presentation is deemed standard here and what level of preliminary descriptions is accepted as adequate.", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "T1_DwxrvMMq", "reviewer": "Reviewer_wJaU", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "Strengths\n- The paper does a good job of formalizing the various PVG settings and relates the effectiveness of the settings in realizing the goal of finding a desirable prover-verifier system. The analysis of the various equilibria in the context of completeness and soundness of the verifier provides good insight into the problem and might help future research.\n- The empirical method of freezing the verifier to allow the prover more time to adjust to the verifier and hide its \"tells\" provides a more compelling case for the system's effectiveness. \n \nWeakness\n- Most of the theoretical analysis of achievable equilibria in the paper only applies to the case of BEC-based example prover-verifier systems. It is not clear if this would transfer well to more complicated settings. Although the theorems stated in the PVG formulation apply to a more general setting, the convergence guarantees for the games seem to need a lot more work.\n- For the empirical evidence justifying the effectiveness of this strategy, I would like to see it applied to a more practical setting. The current approach seems to heavily depend on human intervention to limit the prover and verifier strategy space severely. I would like to see more theoretical work justifying the importance of expert intervention in the game design process or more experimental evidence in the absence of such interventions.", "summary_of_the_paper": "The paper explores the idea of learning a game-theory-inspired prover-verifier system to augment neural networks with verifiable predictions.   In this paper, the authors set up a differentiable prover-verifier game and establish conditions on the formulation of the game to ensure the learned verifier satisfies the soundness and completeness constraints. The paper has the following results:\n- All verifier leading Stackelberg equilibria in a verifier-leading sequential PVG formulation in which the problem instance is revealed after the verifier picks its strategy give a desirable proof-verification protocol.\n- For the BEC-based prover-verifier system, the paper also guarantees that alternate gradient descent ascent converges to equilibrium under suitable learning rates verifier-leading PVG formulations.\n- Empirical evidence from the BEC experiments and the FindThePlus experiments show the effectiveness of the learning scheme in a practical setting.", "summary_of_the_review": "I feel the paper introduces a novel approach for learning prover-verifier systems. Still, I think the theoretical and experimental treatment of the topic in the current version of the paper is not rigorous enough at the moment. I feel the authors need to address the comments above.", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "Er8jcogfgS6", "reviewer": "Reviewer_cqwN", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "**Pros:**\n- Coming up with a way to learn a network such that it is able to justify its answer is very important and useful in the real world\n- It seems like the authors have done a good job analyzing the dynamics of the particular game in Table 1. I don't have a good sense of the significance of the theoretical contribution and would allow the other reviewers who are more familiar with the topic to comment on this point. \n\n**Cons:**\n- The toy examples seem too naive to demonstrate the effectiveness of the framework with respect to interpretability and robustness. Both of these directions are heavily researched, and the authors should be able to find other more realistic settings to convince us of the value of the framework.\n- It is quite difficult for me to identify the practical usage of the framework when reading through the paper, perhaps the authors could have been more concrete with respect to the potential applications?\n\n**Request for clarification:**\n\nI am having some trouble understanding the practical usefulness of the proposed framework, and could really use some clarification from the authors. From my understanding, the main usages of the proposed framework are the **interpretability** and **robustness** of the network's decision. However, I don't think the experiments have demonstrated effectiveness in these two settings. Please correct me if I understand the purpose of the proposed framework incorrectly.\n\nThe authors try to demonstrate the interpretability of the prover's message by examing the gaze of the verifier, which depends on the prover's message. The author claims that the verifier's gaze is interpretable because it always focuses on the region of the image where a blue cross is present. However, the same behavior can be achieved quite easily with other techniques. For example, one can simply look at the saliency map of a naive classifier on the dataset and should be able to identify the cross-region quite easily or one can simply ablate each region of the image and study how the ablation changes the model's prediction.\n\nWith respect to robustness, the author demonstrated the robustness of the verifier's answer with respect to the prover's message, but I am having trouble understanding why being robust to the prover's message is important. For the most part, we care about robustness with respect to changes in the input distribution as machine learning systems are deployed in a different environment, but in what scenario would robustness to an internal prover's message be useful? Does robustness to the prover's message translate to robustness in settings that we care about? \n\n-----updates after rebuttal------\n\nAfter the author's clarification, I am able to understand the theoretical contribution more, and found it to be a valuable contribution. The empirical weakness of the paper remains. However, I have updated my scores to a 6.\n", "summary_of_the_paper": "The authors propose a framework for training networks, such that justification of the answers can automatically emerge from it. Specifically, they propose a training framework where a prover's objective is to persuade the verifier network while the verifier network's objective is answering correctly based on both the original input and the prover's message. The authors analyze when the two-agents training network would converge and identify when the solution derived would become trivial. The authors also applied their framework in two experimental settings: the binary erasure task and the cross detection task, and show that the method would results in robust and interpretable decision rule.", "summary_of_the_review": "The goal of coming up with a neural network that can justify its decision is an important task. The authors have done a thorough job of technically analyzing the proposed framework, but experiments could be strengthened by using more realistic settings.", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "A0Sv_zyVLCO", "reviewer": "Reviewer_RcRe", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "Strengths:\n- the new learning methodology is novel and built on top of solid theoretical foundations, namely, interactive proof systems and game theoretic optimizations;\n- the effectiveness of different instantiations are backed up by both theoretical analyses and empirical studies;\n- the writing is very easy to follow, even though there is quite an amount of theoretical stuff.\n\nWeaknesses:\n- chosen tasks in the evaluation seem fairly simple, so whether there is a great practical potential of the new methodology is not yet clear;\n- the claim of learning in a \"checkable\" or \"verifiable\" manner could be somewhat misleading, as it seems _not_ really verifiable in the sense of classic software analysis and verification (i.e., a piece of code meets its formal specification for all possible executions). The naming might be standard in the theoretical computer science research community, which I am not quite familiar with;\n- the motivation of learning robust protocols is not well-addressed. Basically, why does learning protocols matter in practice? The learned protocol and messages seem to be embedded in neural networks and real-valued vectors, so how could they be interpretable?\n", "summary_of_the_paper": "This paper proposes a new learning methodology for training neural networks based on Prover-Verifier Games (PVGs), which are inspired by interactive proof systems (IPS). PVG consists of two learners, which work in both collaborative and adversarial manners, and the hope is that two learners together could achieve more reliable predictions. This paper studies eight possible game instantiations, depending on player order and when the problem instance is revealed, and the theoretical analysis shows that two instantiations are superior to others, which is also confirmed by an empirical evaluation. This paper also discovers that stress-testing of verifier's robustness is a more meaningful measurement of the learning success in contrast to prediction accuracy during training. ", "summary_of_the_review": "The idea proposed in this paper is novel, and its effectiveness is backed up by theoretical analysis and experimental evaluations. Although no strong practical results have been shown yet, the idea deserves to be published soon. I would like to recommend acceptance for this paper. ", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}]

Author rebuttal:

Meta-review: The reviewers are split about this paper and did not come to a consensus: on one hand they agreed that the paper has valuable theoretical contributions and addresses an important problem in current ML literature, on the other hand they would have liked to see empirical results on a real-world problem setting. After going through the paper and the discussion I have decided to vote to reject for the following reason: I believe the reviewers' concerns about empirical results is not just a request for applying this to more datasets (which is easy to satisfy and I don't think is grounds for rejection), but is actually for a clearer connection for how this work would be used in the machine learning problems described in the introduction and related work sections. What would really help this paper is a real-world running example, in place of the blue plus example, in Figure 1 (I think the blue plus problem is still a useful experimental tool and should be evaluated, but it doesn't clarify the real-world use-cases of this work. This led the reviewers to look to the experimental section for clarification on this, but this wasn't clarified there either. The authors' response to these concerns was an out-of-scope argument: the goal of this paper is to derive/test theoretical results, and there are a number of possible use cases we could apply this to. The authors argue that the current work sends 'a strong signal to the ICLR community that the Prover-Verifier Game is interesting and promising'. I'm sorry but I disagree here: the authors need to do more to convince the ICLR community that this is a framework that will solve outstanding problems in ML. This is solved if the authors (a) run their approach on a real-world dataset in a paper they cite in the related work, (b) they include baselines in this experiment, and (c) if they add this as a running example throughout with a figure that explains this real-world example. With these additions the paper will be a much stronger submission.
Decision: Reject