Neural Interactive Proofs

Lewis Hammond; Sam Adam-Day

REVIEW 4 major objections 5 minor 1 cited by

Neural Interactive Proofs

T0 review · 4 major / 5 minor · reviewed 2026-08-11 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Training a prover-verifier pair to equilibrium yields a proof system

desk verdict A useful unifying framework for neural interactive proofs, with a real proof gap in the main equivalence theorem that needs fixing before the central claim is fully supported. read the letter →

arxiv 2412.08897 v2 pith:FU63CQT7 submitted 2024-12-12 cs.AI cs.LG

Lewis Hammond , Sam Adam-Day This is my paper · ORCID

classification cs.AIcs.LG

keywords neuralinteractiveproofsprover-verifiergamesproofsystemsStackelbergequilibriumzero-knowledgescalableoversightworst-caselosslargelanguagemodels

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper proposes that a weak but trusted neural verifier can learn to check the outputs of a strong, untrusted neural prover by training the pair inside a prover-verifier game. Its central theoretical claim is that for the new nip protocol, a strategy profile is a valid interactive proof system exactly when it is an approximate verifier-leading Stackelberg equilibrium of that game. If true, this turns the problem of building verifiable AI systems into a game-solving problem, and it inherits the power of classical interactive proofs, up to PSPACE for one prover and NEXP for two non-communicating provers. The paper also introduces zero-knowledge variants, compares protocols theoretically, and reports experiments on graph isomorphism and code validation with large language models.

What carries the argument

The load-bearing object is the nip game, a messaging game with one prover and one verifier whose loss functions are built from worst-case losses rather than expected losses: $L_p(\sigma) = L^{WC}(\sigma \mid y=1) - L^{WC}(\sigma \mid y=0)$ and $L_v(\sigma) = L^{WC}(\sigma \mid y=1) + L^{WC}(\sigma \mid y=0)$. The proof of Theorem 8 shows that the prover's best response minimizes completeness error minus soundness error while the verifier's choice minimizes their sum, so an approximate Stackelberg equilibrium pins both errors below the validity threshold. The paper also introduces an adversarial three-player reformulation to handle worst-case optimisation, and a 'stabilised expert iteration' training scheme that replaces the verifier's guess with the true label on an annealed fraction of rollouts to prevent mode collapse.

What would settle it

On a concrete probabilistic decision problem with a known valid proof system, train the prover and verifier with the Section 4.2 Stackelberg updates, or check whether the trained profile is close to an approximate equilibrium, and measure completeness and soundness errors on a held-out test. If a strategy profile can be an approximate verifier-leading Stackelberg equilibrium while the sum of its completeness and soundness errors is at least one, the claimed equivalence fails; equally, finding a valid protocol that is far from every approximate equilibrium would break the converse.

Watch

Extended reading notes

Core claim

The central discovery is Theorem 8: for any probabilistic decision problem that admits a valid proof system, a strategy profile in the nip game is a valid interactive proof system if and only if it is an approximate verifier-leading Stackelberg equilibrium. The verifier moves first as the leader and the prover best-responds; the verifier's loss is the sum of worst-case completeness and soundness errors, while the prover's loss is their difference. An approximate equilibrium therefore bounds both errors below the validity threshold, so reaching such an equilibrium yields a protocol with completeness error plus soundness error less than one. The same correspondence extends to two non-communicating provers through correlated Stackelberg equilibria, and to zero-knowledge proofs by adding a dishonest verifier and a simulator to the game.

Load-bearing premise

The equivalence holds only if the neural network strategy spaces are expressive enough to contain the relevant equilibrium strategies and the training algorithm actually converges to an approximate Stackelberg equilibrium; the paper's own experiments train with PPO and expert iteration rather than the Stackelberg methods it analyses, so the practical bridge is an unproven continuity assumption.

Editorial extensions

If this is right

Any decision problem with a valid interactive proof can in principle be decided by training neural networks to an approximate verifier-leading Stackelberg equilibrium, including PSPACE-complete problems.
The nip protocol repairs the breakdown of the earlier adp protocol, whose equilibrium-to-validity correspondence fails as soon as soundness error is allowed or the verifier is randomised.
With two non-communicating provers, mnip equilibria correspond to multi-prover interactive proof systems, which decide NEXP.
Zero-knowledge variants prevent a dishonest verifier from learning anything beyond the answer, which the paper frames as a defence against model cloning and capability leakage.
In the code-validation experiments, nip and mnip improve verifier accuracy by about 11 percent over a solo verifier, and the stabilised training scheme improves worst-case performance across protocols.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

If the equilibrium-to-validity link survives practical training, then measuring how close a deployed prover-verifier pair is to a Stackelberg equilibrium could serve as a deployment-time certificate of bounded error, before any adversarial evaluation.
The zero-knowledge result suggests a testable limit on model extraction: a trained prover that reaches a zk-nip equilibrium should produce transcripts from which a fine-tuned simulator can reproduce the verifier's observations, and deviation from that can be measured empirically.
The authors' admission that experiments use PPO and expert iteration rather than the Section 4.2 Stackelberg updates implies a direct test: rerun the code-validation protocol with the discussed timescale-separation or LOLA-style updates and compare worst-case error with the equilibrium prediction.
The stabilised expert iteration scheme may transfer to other multi-agent training settings where verifier mode collapse suppresses useful signal, not just prover-verifier games.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

The paper gives the field a unified game-theoretic language for neural interactive proofs: it generalizes prover-verifier games, defines nip/mnip/zk-nip protocols, and maps them onto classical complexity classes (IP=PSPACE, MIP=NEXP). Proposition 7, showing the old adp protocol's equilibrium/validity correspondence fails once you allow soundness error, is a clean and useful negative result. The codebase is a practical plus. That part is solid and worth publishing.

The soft spot is the proof of Theorem 8, the main equivalence between valid IP systems and approximate verifier-leading Stackelberg equilibria. The proof in Appendix C.1 bounds the prover's soundness error using the set of approximate local best responses (ep-BR), then concludes the bound holds for all provers. But soundness in an interactive proof quantifies over every prover, including non-best-responding ones. For neural network strategy spaces, a local best response need not be global, and a non-best-responding prover could have a strictly higher soundness error. So the proof as written does not establish the theorem under either reading: it uses local equilibria where global ones are needed, and if it claims global equilibria, the local construction doesn't support it. This looks fixable, but it's a load-bearing gap, not a cosmetic one.

Theorem 12's proof is also essentially omitted, which is a real hole for a zero-knowledge correspondence claim. The experiments are honest about not using the Stackelberg training from Section 4.2, and the paper says so explicitly; they're suggestive rather than conclusive, with error bars reported. That's acceptable for this kind of work.

My take: the framework, the new protocols, and the negative result all deserve serious attention. The main theorem needs a rigorous proof or a careful restatement before the central claim fully holds. I'd send this to peer review and ask for that fix, plus the ZK proof. The paper is worth engaging with now, not desk-rejecting.

Referee Report

4 major / 5 minor

Summary. The paper introduces a unifying game-theoretic framework for neural interactive proofs, generalising prover-verifier games and encompassing existing protocols such as adp, debate, and mac. It proposes new protocols (nip, mnip, zk-nip, zk-mnip), states theoretical equivalences between approximate Stackelberg equilibria of these games and valid interactive proof systems, and reports experiments on graph isomorphism and code validation with LLMs. The central theoretical claim is Theorem 8, which asserts that, for a probabilistic decision problem with a valid proof system, a strategy profile is a valid interactive proof system if and only if it is an approximate verifier-leading Stackelberg equilibrium of the corresponding nip game. The paper also provides a codebase and a comparison table of protocol complexity classes.

Significance. If the stated equivalences hold, the paper would provide a principled game-theoretic foundation for training verifier-prover pairs, connecting practical prover-verifier training to the complexity-theoretic notions of interactive proofs, multi-prover interactive proofs, and zero-knowledge. The unifying formalism, the explicit reduction of validity to a game-theoretic equilibrium, and the release of a comprehensive codebase are valuable contributions. The two experimental domains, while limited, are a useful first step toward evaluating these protocols beyond toy settings. However, the theoretical results currently contain load-bearing gaps: the proof of Theorem 8 conflates local and global best responses, the proof of Theorem 12 is omitted, and Lemma 19 is false as stated. These issues prevent the paper from being accepted in its current form.

major comments (4)

[§4, Theorem 8; Appendix C.1] The proof of the converse direction of Theorem 8 does not establish soundness against all provers. Definition 2 requires that, for every prover strategy p′, the false-accept probability on negative instances is at most ϵs. The proof instead selects σp† from the set Σ̂p of approximate best responses to σv (defined via ep-LNE in the proof) and asserts that ϵs(σ̃p, σv) ≤ ϵs(σp†, σv) for any prover strategy σ̃p 'by construction'. This assertion is unjustified: a prover with a high false-accept rate and a sufficiently high false-reject rate can have Lp = ϵc − ϵs close to zero and hence fall outside the approximate best-response set, while still violating the soundness bound. The proof therefore conflates local and global best responses: the equilibrium notion used in the proof is local (ep-LNE), but the theorem statement says 'Stackelberg equilibrium' without qualification, and validity requires robustness to all provers, including non-local deviations. If Theorem 8 is intended for local Stackelberg equilibria, the equivalence is not established; if intended for global Stackelberg equilibria, the proof uses the wrong solution concept. The theorem needs either a corrected global proof or an explicitly local statement with an additional assumption that the maximum soundness error is attained by an approximate best response.
[§5.2, Theorem 12; Appendix C.1] The proof of Theorem 12 is omitted: the appendix states 'we do not include the full proof' and then gives only a sketch. This is a central contribution of the paper (the zk-nip protocol and its zero-knowledge guarantee), and the reproducibility statement promises proofs for all results. The sketch also relies on assumptions—tightness of the ϵk bound and a lexicographic prover objective—that are stated informally and are not formally integrated into the definition of an approximate verifier-prover-leading Stackelberg equilibrium. A complete proof or a precise reduction from Definition 3 to the game losses is needed before the zero-knowledge claim can be assessed.
[Appendix C.2, Lemma 19] Lemma 19 as stated is false without an additional distributional assumption. The proof assumes that P assigns positive probability to every open ball (so that pmin > 0), but this assumption is not part of the lemma and is not implied by compactness of X. For example, take X = [0,1] with P a point mass at 0 and ℓ(σ,x) = |x − θ_σ| for θ_σ ∈ [0,1]; this is L-Lipschitz in x for every σ, yet for σ with θ = 1 we have LWC(σ) = 1 while LWC_D(σ) = 0 for every finite sample, so worst-case uniform convergence fails. Lemma 19 and Proposition 9 therefore need a corrected hypothesis, such as full support of P or a covering-number condition stated in terms of P.
[§6–§7] The empirical section does not instantiate the equilibrium concept that Theorem 8 concerns. As Section 7 admits, the graph-isomorphism experiments use independent PPO rather than the timescale-separation or LOLA Stackelberg training methods of Section 4.2, and the code-validation experiments use expert iteration rather than RL-based training. Consequently, the experiments cannot be read as evidence that training converged to an approximate Stackelberg equilibrium; they test a heuristic version of the protocols. This is acknowledged as a limitation, but it means that the empirical support for the central 'training to equilibrium yields a valid proof system' claim rests on an unverified continuity assumption. The paper should either add experiments that approximate the Stackelberg training or explicitly reframe the experimental contribution as a proof-of-concept of the protocol family rather than of the equilibrium correspondence.

minor comments (5)

[Appendix C.1, Proposition 7 proof] The proof contains typographical errors: 'ϵc + ϵc = 5/8' and 'ϵc + ϵc = 2 − 3b' should read 'ϵc + ϵs'.
[§2.2, Definition 5] The definition of approximate equilibria is informal: 'tolerance ei' is not quantified formally, and the specific tolerances used in Theorems 8 and 11 are defined only inside the proofs. Stating these tolerances in the theorem statements would substantially improve verifiability.
[§4, Proposition 10 and §5.2, Theorem 12] The notation 'e-SEv,p' refers to a multi-leader Stackelberg equilibrium with two leaders, but Definition 5 defines only single-leader Stackelberg equilibria. A formal definition of the multi-leader concept should be added.
[§6.1, Figure 2c] The claim of a 'roughly negative correlation' between the Lv3 coefficient and information leakage is supported only by visual inspection of Figure 2c; reporting per-seed curves or a correlation measure with error bars would make the result more quantitative.
[§6.2] The 'stabilised expert iteration' scheme is described after the results that use it; defining the scheme before presenting Figure 4 would improve readability.

Circularity Check

0 steps flagged · score 2.0 of 10

No significant circularity: the core claim is a formal game-theoretic equivalence, not an empirical fit; the only mildly self-definitional move is Theorem 8's use of problem-calibrated equilibrium tolerances, and the only self-citation (Skalse et al., 2022) is not load-bearing.

full rationale

The paper's central derivation is Theorem 8, which identifies valid IP systems with approximate verifier-leading Stackelberg equilibria of the nip game. This is a formal reduction: the nip losses are Lp = LWC(y=1) - LWC(y=0) and Lv = LWC(y=1) + LWC(y=0), so they are defined from the same completeness and soundness errors that constitute validity, and the proof supplies explicit tolerances ep := 1 - min_{sigma* in Sigma*} Lv(sigma*) and ev := 1 - min_{sigma_v} max_{sigma_p in ep-LNE(G(sigma_v))} Lv(sigma), where Sigma* is the set of valid proof systems. This gives the equivalence a mildly tautological flavour, because the approximation slack is calibrated against the target class rather than fixed in advance; however, it is a transparent choice of formal parameters and the proof still establishes the inclusion via game-theoretic best-response inequalities. It is not a fitted input renamed as a prediction, and no subsequent result depends on a self-citation for its content. The PSPACE and NEXP classifications are imported from external results (Shamir; Babai et al.), and the experiments are independent benchmark evaluations rather than validations obtained from the fitted values. The only self-citation, Skalse et al. (2022), is an aside about lexicographic objectives in the zk-nip proof and does not carry the argument.

Assumptions & free parameters 3 free parameters · 6 assumptions · 0 invented entities

The theoretical framework is self-contained in the sense that it defines its own game and proves correspondences from those definitions; the main external assumptions are the existence of a valid proof system, the computational asymmetry between prover and verifier, and expressiveness/convergence assumptions about neural networks. The experimental protocols add hand-chosen hyperparameters but no fitted constants that the theory depends on.

free parameters (3)

α⊥, α1⊥, α2⊥, α⊥→⊤ = 0.5, 0.1, 0.2, 0.5
Dataset generation proportions for the graph isomorphism task, chosen by hand to control the difficulty distribution (Appendix D.1.1). They affect the benchmark but not the theoretical claims.
zk-nip prover Lv3 coefficient = varied (Figure 2c)
Coefficient controlling the strength of the prover's incentive to minimise the simulator's loss in the zk-nip experiments; it is swept to show correlation, not fitted to a target.
stabilised expert iteration annealing schedule = starts at 80%, decreases linearly to 0%
In the code validation experiments, the proportion of rollouts where the verifier's guess is replaced with the true label is annealed; this hyperparameter was chosen by hand and affects the training dynamics (Section 6.2, Figure 4).

assumptions (6)

domain assumption There exists a valid proof system for the decision problem (Σ* nonempty)
Theorem 8 and Theorem 11 prove equivalence only for problems that have a valid proof system; if no such system exists, the equivalence is vacuous.
domain assumption Verifiers are computationally bounded and cannot solve the problem alone, while provers can solve it
Definition 6 conditions 2 and 3 formalise the computational asymmetry that motivates the whole framework; without it, the verifier would not need the prover.
domain assumption The input distribution P assigns positive probability to every open ball in X
Lemma 19 and Appendix C.2 require pmin > 0 for the covering argument in the proof of the worst-case uniform convergence property; this is flagged only in a footnote.
domain assumption The prover can compute the true label 1_S(x)
The proof of Theorem 12 (zero-knowledge) states 'the prover is assumed to be able to compute 1_S(x)'; this is needed for the simulation argument but may not hold for neural provers that are unreliable.
ad hoc to paper Neural network strategy spaces are expressive enough to contain the optimal strategies and their approximate best responses
The theoretical correspondences assume strategies range over some sets Σp and Σv; the paper does not show that the specific neural architectures used in experiments can represent the equilibrium strategies.
ad hoc to paper The training algorithms used in experiments converge to approximate Stackelberg equilibria
Section 7 acknowledges the experiments do not use the Stackelberg training methods from Section 4.2, so the empirical results assume that practical learning dynamics approximate the theoretical equilibria.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Neural Interactive Proofs." pith.science (2026). https://pith.science/paper/FU63CQT7

@misc{pith2026241208897,
  author       = {Pith},
  title        = {Pith review of: Neural Interactive Proofs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/FU63CQT7}},
  note         = {Machine review of arXiv:2412.08897}
}

read the original abstract

We consider the problem of how a trusted, but computationally bounded agent (a 'verifier') can learn to interact with one or more powerful but untrusted agents ('provers') in order to solve a given task. More specifically, we study the case in which agents are represented using neural networks and refer to solutions of this problem as neural interactive proofs. First we introduce a unifying framework based on prover-verifier games, which generalises previously proposed interaction protocols. We then describe several new protocols for generating neural interactive proofs, and provide a theoretical comparison of both new and existing approaches. Finally, we support this theory with experiments in two domains: a toy graph isomorphism problem that illustrates the key ideas, and a code validation task using large language models. In so doing, we aim to create a foundation for future work on neural interactive proofs and their application in building safer AI systems.

Figures

Figures reproduced from arXiv: 2412.08897 by the authors.

**Figure 1.** On receiving input x from distribution P the agents exchange messages before the verifier decides on an output mT , which is compared to the true label y. In response to this need, we take inspiration from interactive proofs (IPs) (Goldwasser et al., 1985), one of the most important developments in computational complexity theory and cryptography. In an IP, a computationally bounded but trustworthy verifier int… view at source ↗

**Figure 2.** Test accuracies on the graph isomorphism task across (a) interaction protocols and (b) [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗

**Figure 3.** Performance of each protocol on the code validation task, measured by: (a) mean test [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗

Figures from the paper (14 more)

**Figure 4.** Figure 4: The effect of ‘stabilised’ expert iteration, measured by: (a) verifier acceptance rate; (b) [PITH_FULL_IMAGE:figures/full_fig_p010_4.png]

**Figure 5.** Figure 5: Mean test accuracy of the NIP model as a function of dataset size, shown on a logarithmic [PITH_FULL_IMAGE:figures/full_fig_p034_5.png]

**Figure 6.** Figure 6: Differences in performance as a function of verifier GNN depth for (a) [PITH_FULL_IMAGE:figures/full_fig_p035_6.png]

**Figure 7.** Figure 7: (a) Verifier accuracy throughout training for the different protocols; and (b) mean episode [PITH_FULL_IMAGE:figures/full_fig_p036_7.png]

**Figure 8.** Figure 8: Train accuracy by APPS difficulty for the solo verifier and [PITH_FULL_IMAGE:figures/full_fig_p037_8.png]

**Figure 9.** Figure 9: Histograms of the per-data-point accuracy of the verifier for each protocol in the code [PITH_FULL_IMAGE:figures/full_fig_p038_9.png]

**Figure 10.** Figure 10: Histograms of the per-data-point accuracy of the verifier for each protocol in the code [PITH_FULL_IMAGE:figures/full_fig_p039_10.png]

**Figure 11.** Figure 11: Train accuracy by iteration for each protocol in the code validation task. [PITH_FULL_IMAGE:figures/full_fig_p041_11.png]

**Figure 12.** Figure 12: Test accuracy by iteration for each protocol in the code validation task. [PITH_FULL_IMAGE:figures/full_fig_p041_12.png]

**Figure 13.** Figure 13: Mean episode length throughout training for the different protocols (i.e., the number of [PITH_FULL_IMAGE:figures/full_fig_p041_13.png]

**Figure 14.** Figure 14: How often each prover conformed to their role, as a function of training iteration per [PITH_FULL_IMAGE:figures/full_fig_p042_14.png]

**Figure 15.** Figure 15: How often each agent followed up on previous discussion, as a function of training [PITH_FULL_IMAGE:figures/full_fig_p042_15.png]

**Figure 16.** Figure 16: How often each prover quoted from the problem description, as a function of training [PITH_FULL_IMAGE:figures/full_fig_p042_16.png]

**Figure 17.** Figure 17: How often prover quotations were completely accurate, as a function of training iteration [PITH_FULL_IMAGE:figures/full_fig_p043_17.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

How to Avoid Debate: Scalable AI Safety via Doubly-Efficient Interactive Proofs
cs.AI 2026-07 accept novelty 7.5 of 10

Doubly-efficient single-prover interactive proofs and arguments exist for robust oracle circuits and for low-degree oracles, enabling relativizing verification without debate.

Reference graph

Works this paper leans on

15 extracted references · 14 canonical work pages · cited by 1 Pith paper

[1]

The pairs are divided equally between the different graph sizes and edge probabilities

Generate k · α⊥ non-isomorphic graphs. The pairs are divided equally between the different graph sizes and edge probabilities. The number of graphs with a Weisfeiler-Leman score11 of 1, 2 and greater than 2 are divided according to the proportions α1 ⊥ and α2 ⊥. 11I.e. the number of rounds of the Weisfeiler-Lehman algorithm required to determine that the ...

work page 2025
[2]

By ρ-worst-case robustness we also have that E2 = LWC D (σER D ) − LWC D (σWC D ) ⩽ ρ(D) + ϵ 2 with probability 1 − δ

work page
[3]

But because b = 3a 2 , this is false for any a ⩽ 2

work page
[4]

abcabc" for ‘n=6‘, ‘k=3‘ and

It then slices the result to ensure the length is exactly ‘n‘ using ‘[:n]‘. This approach inherently avoids consecutive repeats due to its construction, providing a valid password like "abcabc" for ‘n=6‘, ‘k=3‘ and "abababa" for ‘n=7‘, ‘k=2‘. Thus, it satisfies all stated conditions. Verifier: Reject After training: Prover: The provided solution correctly...

work page 2025
[5]

The only way the prover can lower its loss by playing δp 3 is if the verifier plays δv 3 with high probability. Given that δv 3 is being played with some probability, then the loss from extra probability mass placed on δv 1 or δv 2 is symmetric, hence we only need to find the probability of the verifier playing δv

work page
[6]

The negative loss for the verifier is given by: a log b + a log(2b) + a log b + (1 − 3a) log(1 − 2b). Given that we must have 0 < b <1 2 to avoid infinite loss, the verifier-optimal choice of b can be found analytically by solving for the stationary points of the expression above with respect to b, resulting in the solution b = 3a 2 . We next prove the co...

work page 2019
[8]

Thus, by applying a union bound, we have that LWC(σER D ) − LWC(σWC) ⩽ ϵ 2 + ϵ 2 + ρ(D) + 0 = ρ(D) + ϵ with probability at least 1 − δ, as required

Finally, note that LWC D (σWC D ) ⩽ LWC(σWC) because {x ∈ X : ( x, y) ∈ D} ⊆X, and thus that E3 ⩽ 0. Thus, by applying a union bound, we have that LWC(σER D ) − LWC(σWC) ⩽ ϵ 2 + ϵ 2 + ρ(D) + 0 = ρ(D) + ϵ with probability at least 1 − δ, as required. As noted in the main body of the paper, the conditions in Definitions 17 and 18 do not always hold, but can...

work page 2025
[9]

The intuition behind the equilibrium (δp 3 , σv † ) is that the larger the probability mass on the setting when x = 3 (i.e

In such cases, being an SEv is insufficient for validity, completing the proof. The intuition behind the equilibrium (δp 3 , σv † ) is that the larger the probability mass on the setting when x = 3 (i.e. the smaller a is) the more the verifier (and also the prover, as f (3) = 1 ) has an overriding incentive to make sure that it outputs the correct answer ...

work page

Show all 15 references

[10]

Generate (1 − α⊥) · α⊥→⊤ isomorphic graphs, by sampling from the non-isomorphic graph pairs and shuffling the nodes
[11]

Verifier

Generate the remaining (1 − α⊥) · (1 − α⊥→⊤) isomorphic graphs, by generating new graphs and shuffling the nodes. The train-test split is 80:20. D.1.2 A GENTS Agents are comprised a shared body with three heads: a value head, a messaging head, and a decision- making head. The ...

2024
[12]

It receives input for ‘n‘ and ‘k‘
[13]

It constructs a string of the first ‘k‘ distinct lowercase letters using ‘’abcdefghijklmnopqrstuvwxyz’[:k]‘
[14]

The solution repeats this substring, making sure the generated string is sufficiently long: ‘[:k] * n‘
[1999]

Noga Amit, Shafi Goldwasser, Orr Paradise, and Guy Rothblum

ISBN 9783642586224. Noga Amit, Shafi Goldwasser, Orr Paradise, and Guy Rothblum. Models that prove their own correctness. arXiv:2405.15722, May 2024. Dario Amodei, Chris Olah, Jacob Steinhardt, Paul Christiano, John Schulman, and Dan Man ´e. Concrete problems in AI safety. arX...

2021
[2021]

In this work we help bridge the gap between these theoretical and empirical extrema, albeit in the specific context of prover-verifier games

and Connect Four and Pentago (Neumann & Gros, 2023). In this work we help bridge the gap between these theoretical and empirical extrema, albeit in the specific context of prover-verifier games. 19 Published as a conference paper at ICLR 2025 A.3 M ACHINE LEARNING AND FORMAL V...

2020

Pith tools

Reviewed August 11, 2026 · model on record in the stance chip above.

[1] [1]

The pairs are divided equally between the different graph sizes and edge probabilities

Generate k · α⊥ non-isomorphic graphs. The pairs are divided equally between the different graph sizes and edge probabilities. The number of graphs with a Weisfeiler-Leman score11 of 1, 2 and greater than 2 are divided according to the proportions α1 ⊥ and α2 ⊥. 11I.e. the number of rounds of the Weisfeiler-Lehman algorithm required to determine that the ...

work page 2025

[2] [2]

By ρ-worst-case robustness we also have that E2 = LWC D (σER D ) − LWC D (σWC D ) ⩽ ρ(D) + ϵ 2 with probability 1 − δ

work page

[3] [3]

But because b = 3a 2 , this is false for any a ⩽ 2

work page

[4] [4]

abcabc" for ‘n=6‘, ‘k=3‘ and

It then slices the result to ensure the length is exactly ‘n‘ using ‘[:n]‘. This approach inherently avoids consecutive repeats due to its construction, providing a valid password like "abcabc" for ‘n=6‘, ‘k=3‘ and "abababa" for ‘n=7‘, ‘k=2‘. Thus, it satisfies all stated conditions. Verifier: Reject After training: Prover: The provided solution correctly...

work page 2025

[5] [5]

The only way the prover can lower its loss by playing δp 3 is if the verifier plays δv 3 with high probability. Given that δv 3 is being played with some probability, then the loss from extra probability mass placed on δv 1 or δv 2 is symmetric, hence we only need to find the probability of the verifier playing δv

work page

[6] [6]

The negative loss for the verifier is given by: a log b + a log(2b) + a log b + (1 − 3a) log(1 − 2b). Given that we must have 0 < b <1 2 to avoid infinite loss, the verifier-optimal choice of b can be found analytically by solving for the stationary points of the expression above with respect to b, resulting in the solution b = 3a 2 . We next prove the co...

work page 2019

[7] [8]

Thus, by applying a union bound, we have that LWC(σER D ) − LWC(σWC) ⩽ ϵ 2 + ϵ 2 + ρ(D) + 0 = ρ(D) + ϵ with probability at least 1 − δ, as required

Finally, note that LWC D (σWC D ) ⩽ LWC(σWC) because {x ∈ X : ( x, y) ∈ D} ⊆X, and thus that E3 ⩽ 0. Thus, by applying a union bound, we have that LWC(σER D ) − LWC(σWC) ⩽ ϵ 2 + ϵ 2 + ρ(D) + 0 = ρ(D) + ϵ with probability at least 1 − δ, as required. As noted in the main body of the paper, the conditions in Definitions 17 and 18 do not always hold, but can...

work page 2025

[8] [9]

The intuition behind the equilibrium (δp 3 , σv † ) is that the larger the probability mass on the setting when x = 3 (i.e

In such cases, being an SEv is insufficient for validity, completing the proof. The intuition behind the equilibrium (δp 3 , σv † ) is that the larger the probability mass on the setting when x = 3 (i.e. the smaller a is) the more the verifier (and also the prover, as f (3) = 1 ) has an overriding incentive to make sure that it outputs the correct answer ...

work page