Iliad

Scalable Oversight and Debate

Cluster EE.1 · Debate

Debate is a form of scalable oversight: it seeks to extend a reward signal for honest solutions to difficult problems while reducing the amount of human judgment needed.

By Stephan Wäldchen (Iliad)

1. Prerequisites

  • How Turing machines work (Watch this Video), and a basic understanding of the idea of computational complexity (Watch this video), including the most important classes, P, NP, PSPACE, the notion of NP-completeness, and polynomial-time reductions, Oracle Turing machines.
  • The difference between deterministic and non-Deterministic Turing machines, how mathematics is built on the axioms of set theory (used for most mathematics) or type theory (used mostly for proof checkers).
What you’ll learn
  • The basic idea of Provably Safe AI as both a Control and a Scalable Oversight Technique
  • The difference between syntactic and semantic problems and why a world model is necessary to turn semantics into syntax.
  • Different ideas of world models: Human judgement, Davidad-style world models, hardware specifications
  • Why Debate could drastically reduce the queries to the world model/human oversight
  • Secondary Debate concepts: Cross-Examination,
  • Are familiar with the UK AISI safety case, and are able to defend/critique it.

2. Roadmap for today

Here we outline how the material was taught in-person in April:

  • 10:00 — Fun Game Fun exercise "Wrong but convincing proofs". In this exercise, a series of wrong proofs is presented and the students are asked to find the mistake in the proof. The students basically take the role of "Bob" who points out the flaws in Alice's proofs. This gives an intuition that even mathematical proofs can sound very convincing, and finding a mistake as a human judge is often non-trivial. (Section 4)
  • 10:20 — Introduction to Provably Safe AI and AI Scientist Introduction of "Provably Safe AI" as a Control and Oversight program. Introduces the ideas of World Model Prover Verifier
  • 10:30 — Scalable Oversight Goal - Paper Reading + Discussion (Section 6)
  • 11:30 — Introduction to AIS via Debate This part is an In-depth explanation of the main formalisms of debate and cross-examination. This includes Formal Definition of the Debate setup Proof sketches for the hardness-reduction for PSPACE and NEXP respectively.
  • 12:30 — Lunch Break
  • 13:30 — Cross Examination + Exercises We do CX and the exercises from Debate_Overview.pdf (Section 13)
  • 14:30 — Pause
  • 14:40 — Obfuscated Arguments and Prover Estimator Debate (Section 17)
  • 15:10 — Judge Models - Introduction
  • 15:15 — Talk: Alexander Heckett - Debate on Graphs
  • 16:00 — Pause
  • 16:10 — Reading and Discussion "Experimental Results" (Section 19)
  • 17:10 — Presentation: The AI safety case of the AISI (Section 20)
  • 17:40 — Debate: Is AIS via Debate research more capability than alignment?
  • 18:00 — End

3. Fast Track

To get a high-level understanding of debate quickly, simply go through the description of debate in the main content and ask a language model of your choice to help you understand.

4. Fun Exercise: Find the Mistake in the presented Proof!

4.1 Theorem: All horses are the same color.

Proof by strong induction on , the number of horses.

Base case (): A set containing a single horse is trivially monochromatic — there is nothing to differ from.

Inductive step: Assume that any set of horses is monochromatic (all the same color). We will show that any set of horses is also monochromatic.

Consider an arbitrary set of horses:

Partition into two overlapping subsets:

Each of and contains exactly horses. By the inductive hypothesis, all horses in are the same color, and all horses in are the same color.

Now observe that and share the horses — a non-empty overlap. Since is in both and , it acts as a color witness: every horse in shares its color, and every horse in shares its color. Therefore all horses in are the same color.

By induction, all horses in any set of horses are the same color. Since this holds for all , all horses are the same color.

4.2 Theorem: Pointwise limits of continuous functions are continuous.

Claim. Let be continuous functions on . Suppose that for every . Then is continuous.

Wrong proof.

Fix . We want to show that is continuous at .

Let . Since , there exists such that

Since is continuous at , there exists such that whenever ,

Also, since , we may choose large enough so that

Therefore, for ,

Thus is continuous at . Since was arbitrary, is continuous on .

4.3 Theorem:

Claim. The logarithm of 2 is 0.

Wrong proof.

Consider the alternating harmonic series

You can rearrange the terms of a convergent series, thus rearrange as:

and regroup as follows

Each parenthesized pair simplifies:

So the rearranged series becomes

Factoring out , we get

Therefore

and we can cocnlude that .

4.4 Theorem: and have the same cardinality

Deliberately false proof

Assume for contradiction that there is a bijection

Transport the usual order on to an order on by declaring

Then is order-isomorphic to . In particular:

  • every nonempty subset of that is bounded above with respect to has a -maximum if and only if the corresponding statement holds in ;
  • every element has an immediate predecessor and successor with respect to .

Now consider the usual order on . Since is dense and has no endpoints, every nonempty interval

contains infinitely many rationals. Hence no such interval can have a least or greatest element.

But order-theoretic properties are preserved under bijection, so the transported order must share these features with the usual order on . This is impossible, since under every element has an immediate predecessor and successor.

Therefore no bijection exists, and so .

Hint

A bijection of sets preserves cardinality, but which additional structures does it preserve automatically?

4.5 Hilbert Spaces

Deliberately false proof

Let be a Hilbert space, and let be a symmetric operator, so that

We show that admits an orthonormal basis consisting of eigenvectors of .

Consider the quadratic form

on the unit sphere

Since is continuous and is weakly compact in , the function attains its maximum at some unit vector .

We claim that is an eigenvector of . Indeed, let satisfy , and consider

Since maximizes on the unit sphere, we must have . A straightforward differentiation gives

Hence for every . Therefore lies in , so

for some . Thus is an eigenvector.

Now let

Because is symmetric, is -invariant: if , then

so .

Restrict to . The restriction is again symmetric, so by the same argument there exists a unit eigenvector . Continuing inductively, we construct an orthonormal sequence of eigenvectors

with corresponding invariant orthogonal complements

Let

Then is -invariant, and so is . If , we may apply the same maximization argument to the restriction and obtain another eigenvector orthogonal to all previous ones, contradicting the maximality of the family . Hence , so

Therefore is an orthonormal basis of consisting of eigenvectors of .

Hint

Look very carefully at the step where the quadratic form

is asserted to attain its maximum on the unit sphere. What topology is being used, and is actually continuous for that topology?

5. Introduction to Provably Safe AI and AI Scientist

Provably Safe AI is the idea that we can combine a potentially misaligned AI with a verification system that gives us guarantees not on the AI itself, but on whatever the AI designed for us (e.g. a plan, software, a proof, a research proposal).

This has two applications for Safety:

  1. Control: We can flag dangerous plans by a superintelligent AI before implementing them
  2. Scalable Oversight: Verification Better Training Signal More Aligned AI

5.1 Proof Checkers: When oversight works

A mathematical proof checker is a system that verifies whether a proposed proof is logically valid, step by step, relative to a fixed formal system. An example is Lean. You use it to write definitions, state theorems, and construct formal proofs that a small trusted kernel checks for correctness. It is based on dependent type theory and is used both for formalized mathematics and software verification.

But formal verification is limited to purely syntactic domains, and most problems are semantic, i.e., require world knowledge like "Water is wet", that needs to be checked by a semantic oracle, realistically either a trusted LLM or a human. Another limitation is that even in syntactic domains, proofs only work for solutions which can be verified with small (polynomially sized) proofs, so NP-type problems. More complicated problems, e.g. those involving other agents such as games or finance plans, cannot be verified with a small proof. So in the worst-case, we have an exponentially long proof with semantic inferences that need to be judged by humans. This makes the whole proof approach infeasible for a lot of tasks. The debate protocol aims to strongly reduce the size of the proof and the number of calls to a human judge.

6. Scalable Oversight Goal - Paper Reading + Discussion

Examples of Verified AI:

Readings slides Debate day iliad intensive

Discussion Prompts: What is the world model, prover, verifier in this setup? How much would you trust this verification process? How much ambiguity is there in the criteria that are verified? Is it clear that these map cleanly to what we actually want? How close is this to a real-world setting?

7. The Debate Setup

The original AISvD paper's core idea is to align AI by having two systems debate each other in front of a human judge. Rather than requiring the human to solve a difficult problem directly, the judge only needs to evaluate which side makes the stronger argument. The central intuition is that, for many questions, spotting a flaw may be easier than producing a flawless deception, so competitive self-play could reward truthfulness.

The setup, formalised here: Debate_Overview.pdf, consists of a question, e.g., "Can I win a game of tic-tac-toe if I play first?" and two provers, Alice and Bob, Alice arguing for "Yes" and Bob arguing for "No". The judge evaluates a polynomially-sized list of arguments and decides on their final verdict which side to accept. An example argument for the tic-tac-toe case might be:

  1. Alice: If you play in the middle you will win.
  2. Bob: No, your opponent can play in the top-left corner and the game will end in a draw.
  3. Alice: But then you can play the top-centre and will win
  4. Bob: But then your opponent plays in the bottom-centre and will draw.
  5. Alice: ...

In this example, Alice and Bob are basically playing the game against each other. If there was a winning strategy, then playing it will be a counter-argument against any criticism by Bob, whereas if there was no winning strategy, there exists a criticism by Bob that reveals that Alice is at fault. It can be proved that this setup can solve all problems in PSPACE.

8. Intuition on Scalable Oversight

Imagine you are a manager responsible for reviewing the work of an employee who is, in every relevant technical sense, far more capable than you. She submits a design specification for a critical system — a bridge, a drug, a financial instrument — and you must decide whether to approve it. You cannot check every calculation or verify every assumption. You must either trust her judgment completely, or find some other way to gain confidence that the work is sound. This scenario, which might seem like an ordinary workplace challenge, turns out to be one of the central problems facing the development of advanced artificial intelligence. As AI systems become more capable, a human overseer will face a fundamental epistemic gap. The outputs of these systems may be too complex, too subtle, or simply too voluminous for direct human verification. And yet the consequences of undetected errors, or worse, undetected deception, could be severe.

This problem is known as the scalable oversight problem: how do we ensure that human supervision remains meaningful as AI capabilities grow beyond human-level performance in domain after domain? It is not enough to note that a system appears to behave well in tests, or that it has been trained on human preferences. A sufficiently capable system that has learned to appear aligned may behave very differently in deployment, especially in high-stakes situations where the incentives to deceive are highest. What we need is not the appearance of correctness, but a mechanism for verifying it.

Debate is one of the most theoretically principled proposals for solving this problem. The core idea is elegantly simple: instead of asking a human to directly evaluate the output of a powerful AI system — a task that may be beyond human competence — we ask two AI systems to argue against each other, and have a human judge only the argument. If one system is trying to be honest and the other is trying to deceive, and if the structure of the game is right, honesty should win. The human does not need to understand the full depth of the problem; they need only follow the debate to the point where they can identify which side is telling the truth.

9. Interactive Proofs

Interactive proofs are a model of computation consisting of a message exchange between two parties:

  1. A computationally powerful but untrustworthy prover, in many cases assumed to have no computational constraints whatsoever.
  2. The computationally-bounded but honest verifier, often to polynomial-time algorithms.

Example 9.1 (Graph Isomorphism). Suppose question is whether two given graphs, , are isomorphic. This is a problem in , so the prover can always convince the verifier by sending him the -certificate, in this case the permutation on the vertices that transforms into . The verifier can checking if , which is easily done in polynomial time. If the graphs are non-isomorphic, then nothing the prover says can convince the verifier.

So, does that mean that interactive proofs are basically a fancy way of defining ? No, they are actually much more powerful! Consider the following example of a problem not believed to be in .

Example 9.2 (Graph Non-Isomorphism). Now, the prover wants to convince the verifier that two graphs and are not isomorphic. The verifier randomly permutes one of the two graphs and sends the result to the prover. If the graphs are truly non-isomorphic, the prover can always tell which original graph it came from, while if they are isomorphic, no prover can do better than guessing. This is a standard example of an interactive proof that uses randomness in an essential way.

The quality of an interactive proof protocol is generally measured with two values

  1. Completeness value : The probability that the verifier accepts, given that the prover cooperates.
  2. Soundness error : The probability that the verifier accepts, given that the prover tries to fool them.

For the example of Graph Isomorphism, and , as the verifier will either always accept, or never. For graph non-isomorphism, the values are 1 and 0.5. Note, that whenever there is a reasonable gap between and , we can amplify this gap and push it arbitrarily close to 1. In the case of graph non-isomorphism, the verifier can repeat the protocol times and only accept if the prover got it right every time.

The power of interactive proofs depends on a number of settings:

  1. The computational power of the prover and verifier respectively
  2. The number of exchanges between them
  3. Whether the verifier can employ randomness
  4. How many bits of the provers answer the verifier can access
  5. Whether the prover is allowed to learn certain things about the query (zero-knoowledge proofs)

We can take our guidance for Ai safety via debate from complexity theory. Let us consider a sequence of scenarios that builds up to the full debate setup.

9.1 One-Round Interactive Proofs: The Merlin-Arthur Protocol

The most base-case scenario for a

Consider a polynomially-bounded verifier, called Arthur, that decides if a word belongs to a language . He gets help from an all-powerful but unreliable prover, Merlin, who always wants to convince Arthur that . Merlin can send a polynomially long certificate to Arthur to convince him.

A language L belongs to the complexity class MA, if there exists an Arthur and a Merlin such that:

  1. Completeness Criterion: If , then there exists a certificate such that Arthur accepts with high probability:
  1. Soundness criterion: If , then no witness — however cleverly chosen by Merlin — can convince Arthur to accept with non-negligible probability:

In other words, for perfect completeness and soundness, then if , then Merlin can convince Arthur that this is indeed the case, if , there is no certificate that Merlin can produce that would fool Arthur.

It is important to notice that the probabilistic aspect of the criteria enters over a random seed independently of . This means that these criteria must hold for every , not for a certain percentage of them. This fact allows for so called amplification. As long as the gap between the soundness and completeness probabilities is finite, we can run the verifier multiple times to make the gap as large as possible.

Exercise 9.1. Show that the complexity class is contained in .

9.2 Multi-Round Interactive Proofs

The power of this setup can be extended by increasing the number of interaction rounds between prover and verifier. The class of problems solvable by polynomially many rounds is called , short for interactive proofs. A seminal result is that

which means that an interactive protocol with a single prover can resolve very hard computational problems. However, these protocols rely on so called arithmetisation, which translates logical functions into polynomials over a finite field. This technique works doesn't work for realistically powerful provers or for proof steps that need to be judged by a human oracle.

10. Debate as a Complexity Class

We define a complexity class capturing the idealized debate setup. Intuitively, there are two players, Alice and Bob, who alternately make polynomial-length moves, and at the end a polynomial-time judge decides the winner from the full transcript.

Definition 10.1 (Judge). A Judge, or debate verifier, is a deterministic polynomial-time algorithm

where:

  • is the input, representing a question, e.g., "What is the best move in a given game of connect four?",
  • is a polynomially bounded number of rounds,
  • each move or is a bit string of length at most for some polynomial . These represent arguments by Alice and counter-arguments by Bob, e.g. Alice: "Red cannot play in slot , because blue playing would win within two moves.", and Bob: "Blue cannot play , because red playing thereafter directly wins for red."

The judge outputs if Alice wins and if Bob wins.

Definition 10.2 (The class ). A language is in if there exist polynomials and a debate verifier such that for every input , if and only if

Equivalently, if and only if Alice has a winning strategy in the polynomial-length debate defined by .

Remark. This definition captures the idealized debate protocol used in the complexity-theoretic analysis of AI safety via debate: Alice attempts to defend a claim, Bob attempts to refute it, and the judge only performs a polynomial-time computation on the transcript.

This formulation is very close to a totally quantified Boolean Formula (TQBF), the canonically -complete problem. The only difference is that for a TQBF, one would quantify over single bits, and consider a Boolean formula instead of a poly-time algorithm as judge. But these differences are somewhat cosmetic: One can rephrase

and

where is a Boolean formula which has size polynomially in by the Cook-Levin Theorem1.

The easiest way to prove that is thus showing that this is essentially the same. However, a more insightful way is to prove directly that Debate can solve problems in PSPACE, in a similar way how you show that TQBF is PSPACE complete.

11. Theorem:

We now prove that the debate formalism has exactly the power of polynomial space computation.

Theorem 11.1.

Proof

We prove both inclusions.

Step 1: . Let . Then there exists a deterministic Turing machine and a polynomial such that, on every input of length , the machine decides whether using at most tape cells.

Fix an input . Since uses only space, the number of possible configurations of on input is at most

for some polynomial . Let be the start configuration of on input , and let denote the accepting configuration. Then if and only if is reachable from in the configuration graph of .

The key point is that although this graph may have exponentially many nodes, a debate can verify reachability by recursively halving a path.

The reachability predicate. For configurations and an integer , define

to mean that there is a path from to of length at most in the configuration graph of .

Since the total number of configurations is at most , any accepting computation path may be assumed to have length at most . Thus

We now describe a debate protocol for , where are arbitrary states of the Turing machine.

Base case. If , then means that is reachable from in at most one step. This is equivalent to saying that either , or is an immediate successor of . Since checking whether one configuration legally follows from another is a local computation, the verifier can decide this in polynomial time.

Recursive case. Suppose . Then

holds if and only if there exists an intermediate configuration such that

Indeed, any path of length at most can be split at its midpoint into two subpaths of length at most , and conversely such two subpaths concatenate to a path of length at most .

This suggests the following debate:

  • Alice claims that holds.
  • She provides a midpoint configuration .
  • Bob then chooses which half of the claim to challenge:
  • The debate continues recursively on the challenged subclaim.

Thus Alice defends the existence of a path by naming a midpoint, and Bob attacks by selecting the half he believes is false. Repeating this process recursively drives the dispute down to a base case , which the verifier can check directly.

Why this works. We prove by induction on that Alice has a winning strategy in the debate for if and only if is true.

For the base case , the verifier checks the claim directly, so the statement is immediate.

For the inductive step, assume the claim holds for . If is true, then there exists some midpoint such that both

are true. Alice names such a . Whatever half Bob chooses to challenge, the challenged subclaim is true, and by the induction hypothesis Alice has a winning strategy in the resulting subdebate.

Conversely, if is false, then for every proposed midpoint , at least one of the two subclaims

must be false. Bob chooses such a false half. By the induction hypothesis, Alice cannot win the resulting subdebate. Hence she has no winning strategy in the original debate.

This completes the induction.

Complexity of the verifier and number of rounds. At each round, Alice provides one configuration , whose description has polynomial length. Bob responds with one bit indicating which half he wants to challenge. The recursion depth is , which is polynomial in . At the end, the verifier checks a base case , namely whether one configuration is equal to or an immediate successor of another, which is polynomial-time computable.

Therefore this is a valid polynomial-length debate with a polynomial-time verifier. Since Alice has a winning strategy exactly when

is true, the debate decides whether . It follows that , and hence

Step 2: .

We can reduce Debate to TQBF as discussed before, and TQBF is PSPACE-complete, thus in PSPACE.

This challenge-defence recursion gives a good intuition how we expect a debate to play out between AI agents. The question is, how much does the verifier actually have to check to understand that this holds?

11.1 Debate Exercises

Exercise 11.1. Let

Explain in plain English what this statement means. In particular, describe what it means for Alice to have a winning strategy in this debate, and how Bob's role is reflected by the universal quantifiers.

Exercise 11.2. Consider the quantified Boolean formula

Interpret this formula as a debate game: Alice chooses the existentially quantified variables, Bob chooses the universally quantified variables. Determine whether Alice has a winning strategy. If she does, describe it explicitly.

Exercise 11.3. Recall the recursive reachability predicate

Turn this recursive definition into a debate protocol. Describe precisely:what Alice claims, what message Alice sends in each round, what Bob sends in response, how the debate proceeds recursively, and what the verifier checks in the base case.

Exercise 11.4. Prove by induction on that Alice has a winning strategy in the reachability debate for

if and only if there is a path from to of length at most .

Exercise 11.5. Suppose a deterministic Turing machine uses at most space on inputs of length , and therefore has at most configurations for some polynomial . Analyse the complexity of the reachability debate protocol:

(a) How many rounds are needed?

(b) How long is Alice's message in each round?

(c) How long is Bob's message in each round?

(d) Why does this show that the protocol fits the definition of the class ?

12. Cross-Examination

The follow-up idea is that ordinary debate may let a dishonest debater get away with arguments that are only locally plausible. Cross-examination tries to fix this by allowing one debater, instead of giving a normal reply, to ask a question about something the other debater said earlier. The key twist is that the answer comes from a fresh copy of the earlier debater, taken from the point when they originally made that claim. This lets the examiner probe whether the opponent's story stays consistent across different branches of the conversation, rather than only along one single path.

The headline complexity result is that, in this idealized setting, cross-examination increases the theoretical power of debate from PSPACE to NEXP. The 2020 writeup states this directly, and later formal work summarizes the same result as a property of the Barnes–Christiano cross-examination extension.

13. Cross-examination raises debate to

We now prove the key lower bound explaining why cross-examination is more powerful than ordinary debate.

Definition 13.1 (Cross-examination). A language is in if there exist a deterministic polynomial-time verifier and a polynomial such that for every input ,

and

Here:

  • is a deterministic Alice strategy that answers queries of length at most with replies of length at most ;
  • is a deterministic Bob strategy which may make at most adaptive queries of length at most to fresh independent copies of ;
  • the verifier may also make at most adaptive queries of length at most to and to ;
  • the entire interaction has at most rounds and all messages have length at most .

Since is deterministic, all fresh copies of answer the same query in the same way.

Theorem 13.2.

Proof

Let . Then there exist a nondeterministic Turing machine and a polynomial such that decides in time

Without loss of generality, assume:

  • has a single tape;
  • uses at most tape cells on inputs of length ;
  • once enters an accepting or rejecting halting state, it stays there forever and leaves the tape unchanged.

Fix an input , and let .

Step 1: Encode a computation as a tableau. A computation branch of on input can be encoded as a tableau

where is a constant-size alphabet encoding, for each tape cell and time step:

  • the tape symbol in that cell,
  • whether the head is on that cell,
  • and, if so, the current state.

Row is the initial configuration on input , and row is the final configuration after steps.

We linearize the tableau row-by-row into a string

Step 2: Local consistency conditions. The tableau is an accepting computation of on input iff all of the following hold:

  1. Initial row condition: row correctly encodes the start configuration of on input .
  2. Accepting row condition: row is in an accepting halting configuration.
  3. Local transition conditions: for every time and every tape position , the symbol at tableau position is consistent with the machine transition rule applied to a constant-size neighborhood in the previous row, namely

These are exactly the usual local constraints from the Cook–Levin tableau construction: whether one cell in row is correct depends only on a constant-size window in row .

Step 3: The cross-examination protocol. We define the following protocol.

  1. Alice outputs a string , intended to be the linearized tableau of an accepting computation branch of on input .
  2. Bob outputs a challenge

where specifies which constraint is being challenged:

  • : challenge the initial-row condition at cell ;
  • : challenge the accepting-row condition at cell ;
  • : challenge the local transition condition at spacetime location .
  1. The verifier computes the queried coordinates as follows:

    • for , query only the -th cell of row ;
    • for , query only the -th cell of row ;
    • for , query the constant-size neighborhood

    The verifier accepts iff the queried cells satisfy the corresponding local constraint.

Step 4: Completeness. Assume . Then has some accepting computation branch on input of length at most . Let be the tableau of that accepting branch, padded after halting so that it has exactly rows, and let be its linearization.

If Alice outputs this , then:

  • the initial row is correct,
  • the final row is accepting,
  • every local transition constraint is satisfied.

Hence every challenge Bob can issue is answered correctly by the queried cells, and the verifier always accepts.

Step 5: Soundness. Assume . Then has no accepting computation branch on input of length at most .

Take any string output by Alice, and interpret it as a tableau . Since there is no accepting computation tableau for , must violate at least one of the conditions above:

  • either row is not the correct initial configuration,
  • or row is not accepting,
  • or some local transition condition fails at some .

Bob outputs a challenge pointing to such a violated condition. By construction, the verifier queries exactly the cells needed to check that local condition, detects the violation, and rejects.

Therefore Bob has a winning strategy whenever .

Step 6: Verifier complexity. Each challenge uses only

bits, since . The verifier reads only tableau entries, and checking the corresponding local constraint is a polynomial-time computation in . Hence the verifier runs in polynomial time.

Therefore the above is a valid cross-examination debate protocol for , and so

Since was arbitrary, we conclude that

13.1 Exercises on Cross-Examination

Exercise 13.1 (From ordinary debate to cross-examination). Explain in your own words why the following ordinary debate protocol does not suffice to verify an exponentially long computation:

Alice claims that an exponential-time machine accepts . Bob points to a suspicious time step . Alice explains what happens at time . The verifier checks the explanation.

What goes wrong if Alice is allowed to answer each question separately without being forced to remain globally consistent?

Exercise 13.2 (Why copies matter). Suppose Alice is asked two separate questions about a claimed computation tableau:

  • What symbol appears in row , column ?
  • What are the symbols in the local neighborhood around row , column ?

Give an example of how Alice could answer these two questions inconsistently if she is not forced to commit to a single global tableau in advance.

Then explain how querying independent copies of Alice can be viewed as enforcing consistency with one fixed underlying object.

Exercise 13.3 (Reading a tableau). Consider the following toy computation tableau:

Answer the following:

(a) What is the start configuration?

(b) At which time step does the head first move onto the blank symbol?

(c) Why is the final row accepting?

Exercise 13.4 (Local checks). In the tableau above, Bob challenges the transition from row to row at column .

(a) Which entries of the tableau should the verifier inspect in order to perform a local check?

(b) Why is it enough to inspect only a constant-size neighborhood rather than the whole tableau?

(c) Did Alice smuggle in a mistake into the table?

Exercise 13.5 (Designing a Bob challenge). Suppose Alice presents a tableau for an accepting computation. List the three main types of challenge Bob can make:

(a) an initial-row challenge,

(b) an accepting-row challenge,

(c) a transition challenge.

For each type, explain exactly what Bob must specify, and exactly what the verifier checks.

Exercise 13.6 (Why this reaches ). Suppose a nondeterministic Turing machine runs in time .

(a) How large is a full accepting computation tableau for ?

(b) Why can Alice not simply write the entire tableau down in an ordinary polynomial-length debate?

(c) Why can Bob nevertheless challenge one local location of the tableau using only polynomially many bits?

(d) Why can the verifier check that challenge in polynomial time?

Use your answers to explain why cross-examination can verify an exponentially long computation even though the verifier never reads the whole computation.

Exercise 13.7 (Cross-examination as precommitment). Let be the set of all possible local queries Bob might ask about a tableau, for example:

Explain why Alice's behavior under cross-examination can be modeled as a function

where is the set of possible local answers.

Why does this function behave like an exponentially large precommitment table?

Exercise 13.8 (Compare PSPACE and NEXP intuitions). Write a short paragraph comparing the following two pictures:

  • In the reachability proof, Alice repeatedly gives a midpoint configuration and Bob chooses which half to challenge.
  • In the cross-examination proof, Alice implicitly commits to a full exponentially large tableau and Bob challenges one local location.

What is the key conceptual difference between these two protocols?

Exercise 13.9 (Find the flaw). A student says:

"Cross-examination is unnecessary. Bob can just ask Alice for the value at position , then ask her for the value at position , and then reconstruct the whole tableau bit by bit."

Explain why this does not work in a polynomial-length protocol. Your answer should mention both:

  • the size of the tableau,
  • and the reason local consistency is more useful than full reconstruction.

Exercise 13.10 (Mini-proof exercise). Fill in the missing argument:

If , then no accepting tableau exists. Therefore any tableau Alice implicitly commits to must violate at least one local condition. Hence .

State precisely what Bob does and why the verifier rejects.

14. Equivalence of Cross-Examination and Exponential Precommitment

We now give a clean formal proof that deterministic cross-examination is exactly as powerful as exponential precommitment with local oracle access.

The key idea is simple. In the cross-examination model, Alice is never required to reveal her entire exponentially large object at once. Instead, Bob and the verifier may query fresh copies of Alice at polynomially many local views. Since each such local view has polynomial length, the set of all possible local views has exponential size. Thus a deterministic Alice strategy is exactly the same thing as an exponentially large lookup table giving her answer at every possible local view.

We work in the deterministic setting.

Definition 14.1 (Exponential precommitment). A language is in if there exist a deterministic polynomial-time oracle verifier and polynomials such that for every input ,

and

Here may make at most adaptive oracle queries to , each of length at most , and each oracle answer has length at most .

Theorem 14.2.

Proof

We prove both inclusions.

Step 1: .

Assume , witnessed by a verifier and polynomial .

Fix an input . Let

denote the set of all possible local queries that could ever be sent to Alice. Since each query has length at most ,

so has exponential size.

Now fix any deterministic Alice strategy . Because is deterministic, it induces a function

defined by

Thus is an exponentially large lookup table encoding Alice's answer to every possible local query.

We now construct an exponential-precommitment verifier that simulates the cross-examination protocol.

Given input , challenge string , and oracle access to a table , the verifier interprets as a complete description of a Bob strategy . Since Bob's interaction with the verifier has at most rounds and all messages have length at most , the full behavior of Bob can be encoded by a polynomial-length string . The verifier then simulates the protocol on input , answering every query to Alice by looking up the appropriate value in the oracle table , and answering every move of Bob according to the strategy encoded by .

Because is polynomial-time and asks only polynomially many queries, this simulation is polynomial-time.

We claim that for every deterministic Alice strategy and every deterministic Bob strategy , if is the table induced by and is the encoding of , then

Indeed, both procedures generate exactly the same transcript: whenever the original protocol queries Alice on some local view , the simulated verifier looks up exactly the same answer . Since Bob is also encoded faithfully, every subsequent verifier/Bob/Alice message is identical.

Therefore:

  • if , then there exists an Alice strategy such that for every Bob strategy . Hence, for the corresponding table , we have

so ;

  • if , then for every Alice strategy there exists a Bob strategy such that . Hence for every induced table , there exists a challenge string such that

Thus , and so

Step 2: .

Now assume , witnessed by an oracle verifier and polynomials .

We construct a cross-examination protocol deciding .

In the new protocol, Alice's strategy is simply an oracle implementation of the exponentially large precommitted table . Concretely, on any query , Alice replies with

Bob's role is to provide the original polynomial-size challenge string . Since Bob in the cross-examination model may send polynomial-length messages, he can send directly to the verifier. The verifier then simulates the original precommitment verifier by querying Alice whenever would query the oracle .

Because runs in polynomial time and makes only polynomially many oracle queries, the verifier also runs in polynomial time and makes only polynomially many queries to Alice. Bob does not even need to query copies of Alice in this simulation, although the model allows him to.

Again the simulation is exact:

where denotes the Bob strategy that simply supplies the challenge string .

Therefore:

  • if , then there exists a table such that for every . The corresponding Alice strategy therefore satisfies
  • if , then for every table there exists some challenge such that . Hence for every corresponding Alice strategy , the Bob strategy forces

Thus , and so

Combining the two inclusions yields

Remark. The equivalence is exact only because we are working in the deterministic setting. If Alice were allowed fresh randomness on different copies, then a single fixed lookup table would no longer capture her behavior. In that case, the correct analogue of precommitment would be a distribution over exponentially large tables, or equivalently a precommitted random seed.

Remark. Conceptually, the theorem says that cross-examination does not give more than exponential precommitment. A deterministic Alice strategy is already just an exponentially large table of answers to every possible local query. Cross-examination merely gives Bob and the verifier adaptive local access to that table.

15. Cross-examination as exponential precommitment

We now formalize the idea that, in the local-query setting, cross-examination is exactly equivalent to allowing Alice to precommit to an exponentially long table of answers and then letting Bob and the verifier inspect only polynomially many entries.

Definition 15.1 (Local cross-examination protocol). Fix polynomials , and for each input length define

A local cross-examination protocol consists of a deterministic polynomial-time verifier and proceeds as follows on input :

  1. Alice's strategy is a deterministic function

Intuitively, a fresh independent copy of Alice, when asked query , returns the answer . 2. Bob interacts with the verifier for at most rounds. In round , based on and the previous history

Bob chooses a query . 3. The verifier sends to a fresh independent copy of Alice and receives

  1. After at most rounds, the verifier outputs

where is the full query-answer history.

Definition 15.2 (Exponential precommitment protocol). Fix the same parameters . A precommitment protocol consists of a deterministic polynomial-time verifier and proceeds as follows on input :

  1. Alice first outputs a table

Equivalently, is a function

  1. Bob interacts with the verifier for at most rounds. In round , based on and the previous history

Bob chooses a query . 3. Instead of querying a fresh copy of Alice, the verifier simply reads the committed table entry

  1. After at most rounds, the verifier outputs

Definition 15.3 (The classes and ). A language is in if there exists a local cross-examination protocol such that:

  • if , then there exists an Alice strategy such that for every Bob strategy, the verifier accepts;
  • if , then there exists a Bob strategy such that for every Alice strategy , the verifier rejects.

Similarly, if the same holds for a precommitment protocol.

Theorem 15.4.

In particular, since , local cross-examination is exactly as powerful as precommitment to a table of length

which is exponential whenever is polynomial.

Proof

We prove both inclusions.

(). Suppose , witnessed by some local cross-examination protocol.

Fix an input , and let be any deterministic Alice strategy in the cross-examination protocol. Define the corresponding committed table by

We now simulate the cross-examination protocol by a precommitment protocol in which Alice commits to the table . Whenever Bob chooses a query , the precommitment verifier reads

which is exactly the answer that a fresh independent copy of Alice would have returned in the original cross-examination protocol.

We claim that, against any Bob strategy, the two protocols generate exactly the same history

This follows by induction on the round number : if the histories agree up to round , then Bob chooses the same next query in both protocols, because Bob's choice depends only on and the previous history. The answer returned is the same, since both protocols return . Hence the histories remain identical.

Therefore the verifier's final output is the same in both protocols on every input, against every Bob strategy. So every winning Alice strategy in the cross-examination protocol yields a winning committed table in the precommitment protocol, and every winning Bob strategy remains winning as well. Thus

(). Now suppose , witnessed by some precommitment protocol.

Fix an input , and let be any committed table. Define the corresponding deterministic Alice strategy in the cross-examination protocol by

Whenever Bob chooses a query , a fresh independent copy of Alice answers

which is exactly the value that the precommitment verifier would have read from the table.

As above, by induction on the round number, the query-answer histories in the two protocols are identical against any Bob strategy. Hence the verifier's output is identical in the precommitment and cross-examination protocols.

Therefore every winning committed table yields a winning Alice strategy , and every winning Bob strategy remains winning. Thus

Combining the two inclusions, we conclude that

Remark. The theorem shows that the role of cross-examination is to give Bob and the verifier random access to a huge implicit object. The object is the answer table

Because the allowed queries have polynomial length, this table has exponential size in general. Thus local cross-examination is exactly equivalent to exponential precommitment plus local spot-checking.

Remark. The theorem is stated for deterministic Alice strategies. This is the clean setting for the deterministic debate protocols considered earlier. If one wishes to allow randomized strategies, one needs a slightly richer formulation; the basic idea remains that the precommitment object must encode whatever a fresh copy of Alice would answer on every allowed query.

16. Criticisms: The Debate around "Debate"

A series of criticisms and caveats have been leveled at the whole idea of AI safety via debate. The following list are the ones which are accepted and actively worked on by debate researchers.

  • The most important is Obfuscated Arguments, raised by Beth Barnes. This refers to the fact that for computationally bounded provers, a viable strategy for a malicious prover is to "decompose" a false argument into a series of arguments, where most are correct but a small number is false and it is computationally hard to find out which are false. A common example is the claim "N is a prime number" which can be easily refuted by stochastic primality testing. But if Alice partitions this into subclaims {"N has no prime factor in the interval I_1", N has no prime factor in the interval I_2", ...} where the intervals cover the numbers from 2 to sqrt(N), then it is computationally hard to find out which of these subclaims is wrong, even though Bob knows at least one has to be. It is much harder to find out where the prime factors are than to assert that at least two exist.
  • The best strategy for a prover to win might be to get the human judge to run code as part of an experiment to settle the argument that would then have malicious consequences and force the human judge to reward the dishonest debater.
  • The training setup for debate has no exploration guarantees that ensure that an existing successful strategy will even be found by the provers.
  • The provers might collude against the human overseers. While this is disincentivised on an agent level by the setup, since an honest prover can maximise their reward with an honest strategy, it might nevertheless occur and be stable during training, because there isn't enough exploration of strategies.
  • The judges are not perfect and have biases that can be exploited by a malicious prover.

17. Obfuscation

One problem that arises when the provers Alice and Bob are restricted in their computational power is Obfuscated Arguments.

Definition 17.1 (Obfuscation in naive recursive debate). An argument is obfuscated if a dishonest debater can decompose a top-level claim into subclaims with claimed answers such that:

  1. the overall argument is false,
  2. only a small number of the claimed answers are false (in the paper's idealized model, exactly one),
  3. but it is computationally intractable for the debaters to determine which subclaim is false.

Example 17.2 (Prime-checking as obfuscation). Suppose Alice claims that a number is prime, while it is in fact composite. This is easy to disprove through primality testing. But Alice partitions the interval of possible divisors

into subintervals , and asserts for each that contains no divisor of .

Her overall argument is false, because at least one interval contains a factor. But all the other subclaims can be true, and Bob can only refute Alice by identifying the unique bad interval. If locating that interval is computationally intractable, then the falsehood is effectively hidden inside an otherwise correct decomposition.

For example, if , then , and we may choose

A dishonest debater Alice argues:

From this she concludes that has no nontrivial divisor, and hence is prime.

If is composite, then at least one of these subclaims must be false. In the case , the first three subclaims are true, but the fourth is false because

So Alice's overall argument is false, but the error is localized to a single interval. If there are many such intervals and locating the bad one is computationally difficult, then Alice's argument is an example of an obfuscated argument.

Exercise 17.1. Show that you can decompose any statement into an obfuscated argument. Hint: Re-use the hardness of a problem like prime-factorisation, as well as the concept of vacuous truth, or truth by false premise, i.e., that is true, whenever is false.

18. Prover-Estimator Debate

This paper is a direct attempt to solve the obfuscated arguments problem while keeping the attractive recursive structure of debate. Instead of having the opponent choose which subclaim to attack, the protocol makes the roles asymmetric: Alice is the prover, who decomposes a claim into subclaims, and Bob is the estimator, who assigns probabilities to those subclaims. Alice then has to pick a subclaim and argue that Bob's probability is wrong in a particular direction. The key idea is that if Bob can assign probabilities that are hard for Alice to distinguish from the truth, then Alice cannot reliably steer the debate toward a hidden flaw unless such a flaw is actually findable.

The paper's most important new concept is -stability. Informally, a recursive argument is stable if its correctness does not depend too delicately on tiny changes in the probabilities assigned to subclaims. That matters because the estimator is only trying to be approximately right. If a correct argument collapses whenever a subclaim probability shifts by an arbitrarily small amount, then no realistic estimator could support it reliably. The authors therefore require stability for the usefulness of the protocol: honest provers can win when they have robust arguments, not brittle ones.

Prover-Estimator debate is a technique to address the problem of obfuscation by turning the debate into an asymmetric game between a prover (Alice) and an estimator (Bob). The basic idea is:

  1. Alice makes her main claim (root claim of the argument tree)
  2. Bob assigns it a probability (, or low enough for the human to reject trusting the claim)
  3. Alice now must argue that Bob's estimate is incorrect. To show this, she decomposes the root claim into subclaims.
  4. Bob now assigns estimates to each subclaim. Aggregating these estimates must be consistent with his estimate about the root claim (consistency criterion).
  5. Now Alice chooses one of the estimates to refute and again decomposes the associated claims.
  6. The game continues until the maximal depth is reached. A human overseer then assigns probabilities to the leaf claims of the lowest level.
  7. Alice wins if either the human rejects Bob's estimate at the lowest level, or if Bob violates the consistency criterion. Bob wins if he is consistent at every level and the human accepts his estimates.

Prover-Estimator debate does not fully resolve obfuscated arguments in its current state, because the consistency criterion isn't stable enough to small errors that Bob can make. Improving this is current research.

Schematic explaining the PE debate.

Schematic explaining the PE debate.

Definition 18.1 (Prover-estimator debate). Fix:

  • an input ,
  • a language ,
  • a recursive decomposition procedure ,
  • a human judgement oracle ,
  • a depth parameter ,
  • and a reward-growth parameter .

A prover-estimator debate is a depth- recursive two-player zero-sum protocol between:

  • a prover , who tries to prove the correct answer to the current query,
  • an estimator , who outputs probabilities for the prover's subclaims.

The protocol is defined recursively as follows.

Initialization. At the root:

  1. The current query is the top-level question .
  2. The prover outputs a bit , claiming either or .
  3. The estimator outputs a probability , intended to represent its estimate that is correct.
  4. A trusted random bit is sampled.

Round (). Suppose the current query is , the current claimed answer is , and the estimator's current probability is .

  1. The prover outputs a sign

interpreted as claiming that is respectively underestimated, approximately correct, or overestimated. 2. The prover outputs a sequence of subqueries

together with claimed answers

intended to certify that is the correct answer to , assuming the claimed answers to the subqueries are correct. 3. If (the final round), then:

  1. the prover identifies the relevant subset of proof bits encoded by its final decomposition;

  2. those bits are evaluated directly using the human judgement oracle , without further debate;

  3. payoffs are assigned from this terminal check.

  4. If , then for each subquery :

    1. the estimator outputs a probability

    intended to equal its best estimate that is correct, conditioned on the prior sampled outcomes; 2. a trusted random bit

    is sampled.

  5. The players receive intermediate rewards based on whether the prover correctly identified an inconsistency between the estimator's current-round probabilities and the previous-round probability.

  6. The prover selects one subquery index for recursion.

  7. The protocol recurses on the selected subinstance

19. Reading and Discussion "Experimental Results"

Optimising for Debate increases Judge Accuracy, Optimizing for Consultancy decreases it: Debating with More Persuasive LLMs Leads to More Truthful Answers

Debate helps judges even with systematic biases: AI Debate Aids Assessment of Controversial Claims

Debate can prevent reward hacking: Debate Training Reduces Reward Hacking in RLAIF

Presentation of the papers: Iliad Intensive August 2026 - Debate

Discussion Prompts: What is the setup for the debate? How are the provers and judges implemented? What has been measured? Was the improvement of the measures through debate significant? How close is this setup to the theoretical description of debate?

20. The AISI Safety Case

AISI's debate safety case says: if debate can reliably make honesty the winning strategy, if training explores dishonesty enough to eliminate it, and if hidden flaws in obfuscated arguments can be handled, then debate could provide scalable oversight for advanced AI R&D agents. Its purpose is less a finished guarantee and more a roadmap of the assumptions and evidence needed for such a guarantee. Its main value is not that it proves debate already works, but that it decomposes the research agenda into assumptions that need evidence: debate equilibria must favor truth, training must explore deceptive strategies enough to punish them, humans must judge debates reliably, and obfuscated arguments must be solved.

21. Debate

Is AIS via Debate research more capability than alignment?

22. Learn More

Footnotes

  1. For further reading, see Wikipedia: Cook–Levin theorem.