Depate and interactive proof

2025-01-17 — 2026-02-13

Wherein neural nets are represented as prover‑verifier games, and neural interactive proofs are shown to capture PSPACE and NEXP decision procedures, with zero‑knowledge variants obtained for certain protocols.

compsci
machine learning
making things
neural nets
Figure 1: Bob hides his proof from Alice.

Placeholder. Various notes on interactive proofs, debate, and related protocols.

1 Computational cost of explaining complex reasoning

Intuitively, something might be, should be difficult, computationally about explaining the reasoning of a large neural network. Surely simpler things cannot explain more complex things?

As an extreme example, we might run into incompleteness results. (Prove the consistency of the following system of axioms…) I can believe such extreme esoterica would not be relevant in practice, but could problems close to those arise in practice? TBC.

2 Neural interactive proofs

Neural Interactive Proofs (Hammond and Adam-Day 2025):

The main theoretical challenges are to: i) represent a given protocol in the form of a prover-verifier game (Kirchner et al. 2024); and ii) train the models to approximate the right equilibria of this game. While the first challenge is reasonably straightforward, the power of different protocols can vary greatly depending on several subtle details such as the number of messages the agents can send to each other, their ability to randomise, and whether messages can be sent privately to different agents. By taking these subtleties into account, we can show an equivalence between the equilibria of the game and valid proof systems for a range of different protocols.

Table 1: (from Hammond and Adam-Day (2025)) A comparison of the various proof protocols we discuss in our work. The “Complexity” column denotes the corresponding complexity class of decision problems that can be solved when represented as a (generalised) prover-verifier game played between unbounded provers and probabilistic polynomial time verifiers.
Model Rounds Complexity Zero-knowledge
adp 2 NP ❌
debate $T$ PSPACE ❌
mac 2 MA ❌
nip $T$ PSPACE ❌
mnip $T$ NEXP ❌
zk-nip $T$ PSPACE ✅
zk-mnip $T$ NEXP ✅

The second theoretical challenge arises because the equilibria that form this equivalence are (approximate) Stackelberg equilibria over the worst-case loss, which are difficult to optimise for using conventional machine learning algorithms. We discuss several approaches to overcoming this challenge, including the use of Stackelberg policy gradient and opponent-shaping algorithms to approximate Stackelberg equilibria, and the efficacy of average-case optimisation and adversarial training when it comes to minimising worst-case losses.

3 Prover-Estimator games

TBD

4 References

Abbaszadeh, Pappas, Katz, et al. 2024. “Zero-Knowledge Proofs of Training for Deep Neural Networks.”
Allen-Zhu, and Xu. 2025. “DOGE: Reforming AI Conferences and Towards a Future Civilization of Fairness and Justice.” SSRN Scholarly Paper.
Barnes. 2020. “Debate Update: Obfuscated Arguments Problem.”
Barnes, and Christiano. 2020. “Writeup: Progress on AI Safety via Debate.”
Brown-Cohen, Irving, and Piliouras. 2025. “Avoiding Obfuscation with Prover-Estimator Debate.”
Hammond, and Adam-Day. 2025. “Neural Interactive Proofs.” In.
Irving, Christiano, and Amodei. 2018. “AI Safety via Debate.”
Kirchner, Chen, Edwards, et al. 2024. “Prover-Verifier Games Improve Legibility of LLM Outputs.”
Lang, Huang, and Li. 2025. “Debate Helps Weak-to-Strong Generalization.”
Michael, Mahdi, Rein, et al. 2023. “Debate Helps Supervise Unreliable Experts.”
Navajas, Niella, Garbulsky, et al. 2018. “Aggregated Knowledge from a Small Number of Debates Outperforms the Wisdom of Large Crowds.” Nature Human Behaviour.
Zakershahrak, and Ghodratnama. 2024. “Explanation, Debate, Align: A Weak-to-Strong Framework for Language Model Generalization.”