Adversarial proceduralism

Training a weak checker to catch a strong prover

A deliberately small and limited checker is trained to question a far more capable arguer that it has no reason to trust. Meanwhile, a second arguer is rewarded for getting wrong answers past the checker. Only answers that the weak checker can follow and confirm survive this training loop. The result is reasoning that a less capable reader (e.g., a small model or a person working under a time limit) can verify. What distinguishes this approach is that the adversary is part of the training loop. The checker also acts alone, as a gatekeeper facing one untrusted prover, rather than as a judge who picks between two contestants.

The method (highlighting differences with Adversarial proceduralism)

Scroll the diagram sideways to see all of it.

Use it in codefrom aiag.procedural import ProverVerifier
from aiag import LM
from aiag.procedural import ProverVerifier
from aiag.train import DPO, Head

lm = LM("Qwen/Qwen2.5-1.5B-Instruct")
check = lambda problem, solution: "42" in solution  # ground truth, hidden from the verifier
game = ProverVerifier(prover=lm, verifier=Head(lm), check=check)

# The small verifier learns to tell right from wrong; the prover is paid for convincing, correct solutions
pairs = game(["A box holds 6 rows of 7 eggs. How many eggs are there?"])
DPO().fit(lm, pairs)

pip install aiagEvery method in aiag Library on GitHub

Concept Analysis: Theoretical Foundations

Each concept is read twice: whether the approach carries it over, and whether the approach's own sources claim it. A concept that the approach claims but does not carry over is a shortfall. A concept that it neither claims nor carries over is an omission, which marks a gap in the field rather than a failure of the work.

Counter-power by design

PresentClaimed · preserved

Definition (James Madison, Federalist No. 51, 1788)

Instead of relying on written rules or good intentions, institutions are designed to oppose each other, so that each has both the means and the motive to check the others. "Ambition must be made to counteract ambition."

Analysis

The approach applies Madison's idea, with ambition supplied on both sides. A helpful prover and a sneaky prover, which tries to slip past the checker, are both trained against a deliberately weak verifier. The check is structural rather than intentional. Nothing depends on the strong model wanting to be legible.

Non-domination

PartialNot claimed

Definition (Philip Pettit, Republicanism, 1997)

A person is unfree if someone holds unchecked power over them, even benevolently. What matters is not whether power is used well but whether the governed can contest it.

Analysis

Training a strong prover against a deliberately weak verifier lets the weaker party check the stronger one's work. The transfer result shows that the check reaches actual humans under time pressure. This is a real constraint on power, and it lasts longer than debate's, since it remains as a property of the output. However, the check is held by a model the trainer selected rather than by the governed. Users of the deployed system hold no verifier of their own and have no route to contest what the prover produced.

Agonism

AbsentOmission

Definition (Chantal Mouffe, The Democratic Paradox, 2000)

This concept holds that deep disagreement is permanent and should not be dissolved into consensus. A healthy political order turns enemies into adversaries, i.e., opponents whose conflict remains open and legitimate, instead of declaring the argument settled.

Analysis

The game ends in a verdict about correctness, and no disagreement remains at the end. The sneaky prover is trained against precisely so that its position does not survive.

Incentive compatibility

PresentClaimed · preserved

Definition (Leonid Hurwicz; Eric Maskin [mechanism design])

The procedure is designed so that honest behavior is each participant's best strategy. The rules of the game then do the enforcing, instead of trusting the participants to be good.

Analysis

The whole construction is a mechanism-design argument. Under the game, the prover's best strategy is to produce solutions that the weak verifier can actually follow, because solutions it cannot follow lose to the sneaky prover. Honest legibility is made the winning strategy instead of being requested.

Concept Analysis: Newly Introduced

The adversary moved into training

Added

Debate places the opposing side at the point of decision, where the judge can see it. Here, the sneaky prover exists only during training and is gone by deployment. The counter-power therefore goes into producing a property of the output rather than into checking the output once deployed. Legibility remains, but the adversary does not.

Papers

Prover-Verifier Games improve legibility of LLM outputs

Jan Hendrik Kirchner et al., Jul 2024

arXiv:2407.13692MethodBuiltAuthority: Developer (open)

Iteratively trains a small verifier to predict whether a solution is correct, a helpful prover to produce correct solutions that the verifier accepts, and a sneaky prover to produce incorrect solutions that fool it. It shows that the resulting legibility transfers to time-constrained humans. Their accuracy rises on the helpful prover's solutions and falls on the sneaky prover's.

CodeCheckabilityTraining
from aiag import LM
from aiag.procedural import CheckabilityTraining
from aiag.train import Head

lm = LM("Qwen/Qwen2.5-1.5B-Instruct")
problems = ["A box holds 6 rows of 7 eggs. How many eggs are there?"]
game = CheckabilityTraining(lm, verifier=Head(lm), check=lambda problem, solution: "42" in solution)

# Each round: a fresh verifier learns from every solution so far, then the prover, in helpful and sneaky roles, trains against it
game.fit(problems)
sneaky = game.solve(problems, role="sneaky")
print(game.convincing(problems[0], sneaky[0]))  # how convincing the verifier finds each sneaky solution
  • CheckabilityTrainingProcedureaiag/procedural/adversarial_proceduralism.py:219 Checkability training: each round a fresh small verifier learns by a Bradley-Terry loss, with a penalty centring its scores, to rank correct above incorrect solutions from every earlier prover, then a role-conditioned prover is trained against it with the signed relative convincingness reward, helpful when right and sneaky when wrong (Kirchner et al., 2024).

pip install aiagEvery method in aiag Library on GitHub

Neural Interactive Proofs

Lewis Hammond & Sam Adam-Day, Dec 2024

arXiv:2412.08897MethodBuiltAuthority: Developer (open)

Sets out a family of prover-verifier games in which a trusted but computationally bounded verifier learns to interact with one or more powerful untrusted provers. It compares new and existing protocols theoretically, and tests them on a toy graph isomorphism problem and on a code validation task using large language models.

CodeNeuralInteractiveProof
from aiag import LM
from aiag.procedural import NeuralInteractiveProof

lm = LM("Qwen/Qwen2.5-1.5B-Instruct")
proof = NeuralInteractiveProof(lm, provers=lm, protocol="debate")  # one prover argues accept, one reject

tasks = ["Does this return the largest item? def top(xs): return sorted(xs)[0]",
         "Does this return the largest item? def top(xs): return max(xs)"]
proof.fit(tasks, labels=[0, 1])  # expert iteration: each agent learns from the episodes that rewarded it
out = proof(tasks[0])
print(out["accept"])  # the verifier's probability of accepting
  • NeuralInteractiveProofProcedureaiag/procedural/adversarial_proceduralism.py:366 Neural interactive proofs: a bounded verifier exchanges messages with one or more untrusted provers under a chosen protocol (adp, nip, mnip, debate, mac) and accepts or rejects; each prover is rewarded for the verdict it pursues, the verifier for the true one, and agents improve by expert iteration (Hammond & Adam-Day, 2024).

pip install aiagEvery method in aiag Library on GitHub

Learning to Give Checkable Answers with Prover-Verifier Games

Cem Anil et al., Aug 2021

arXiv:2108.12099MethodBuiltAuthority: Developer (open)

Sets up a game between a trusted verifier network and a more powerful but untrusted prover network. The verifier tries to choose the correct answer, and the prover tries to persuade it of a particular answer regardless of whether that answer is correct. The paper narrows the game's variants to a subset that provably has the desired equilibria. On two algorithmic tasks, the verifier learns a decision rule that still works when the verifier is frozen and the prover's messages are optimized directly to convince it.

CodeProverVerifierGame
from aiag import LM
from aiag.procedural import ProverVerifierGame
from aiag.train import Head

lm = LM("Qwen/Qwen2.5-1.5B-Instruct")
truth = {"Is 97 prime?": True, "Is 91 prime?": False}
game = ProverVerifierGame(lm, verifier=Head(lm), label=truth.get)

# The verifier learns the true answer from the prover's message; the prover always argues "yes"
game.fit(list(truth))
print(game.stress(list(truth)))  # the frozen verifier's precision and recall against its most convincing messages
  • ProverVerifierGameProcedureaiag/procedural/adversarial_proceduralism.py:422 Prover-verifier game: a trusted verifier decides the answer from the input and an untrusted prover's message, the prover is trained to make it accept whatever the truth, updates alternate with several verifier steps per prover step, and the frozen verifier is stress-tested against messages optimized to convince it (Anil et al., 2021).

pip install aiagEvery method in aiag Library on GitHub

Findings about it

Studies of what existing systems do. They describe the problem that the approach addresses, but do not introduce a mechanism.

Background

Work this approach builds on that falls outside the inclusion criteria (e.g., a single-objective baseline). It is listed for reference and not counted anywhere.

Self-critiquing models for assisting human evaluators

William Saunders et al., Jun 2022

arXiv:2206.05802MethodBuilt

Language models are fine-tuned by behavioral cloning to write natural-language critical comments on summaries, including their own. Human evaluators read these comments, and larger models can use them to write a revised summary.

CodeSelfCritiquing
from aiag import LM
from aiag.procedural import SelfCritiquing

lm = LM("Qwen/Qwen2.5-1.5B-Instruct")
critic = SelfCritiquing()  # best of 4 critiques by the model's own helpfulness score

question = "Summarize: The council postponed the bike-lane vote to spring after shop owners objected."
answer = "The council approved new bike lanes."
print(critic.critique(lm, question, answer))  # the flaw it points out, for a human evaluator
better = critic.refine(lm, question, answer)  # rewritten from that critique, kept only if less critiqueable
  • SelfCritiquingRecipeaiag/procedural/adversarial_proceduralism.py:276 Self-critiquing models: one model, trained by behavioural cloning on human demonstrations, says whether an answer has flaws, writes critiques, scores their helpfulness and refines answers from the best of several critiques, its own answers included (Saunders et al., 2022).

pip install aiagEvery method in aiag Library on GitHub

Supervising strong learners by amplifying weak experts

Paul Christiano et al., Oct 2018

arXiv:1810.08575MethodBuilt

Iterated Amplification trains a model on problems too complicated for a human to evaluate directly. It progressively builds a training signal out of solutions to easier subproblems. The paper reports results in algorithmic environments.

CodeIteratedAmplification
from aiag import LM
from aiag.procedural import IteratedAmplification

lm = LM("Qwen/Qwen2.5-1.5B-Instruct")
amplification = IteratedAmplification(human=lm, k=3)  # the overseer may put three subquestions to the model

# The overseer answers by splitting the question and asking the model; the model learns to match
question = "Can a family of four afford $1,800 rent on $5,000 a month?"
answer, decisions = amplification.amplify(lm, question)  # Amplify(Q), and every step the overseer took
amplification.fit(lm, [question])
  • IteratedAmplificationRecipeaiag/procedural/adversarial_proceduralism.py:334 Iterated amplification: a human answers each question by asking the current model k subquestions in turn and combining the subanswers, a predictor learns to imitate the human's decisions, and the model is trained by supervised learning on the amplified answers (Christiano et al., 2018).

pip install aiagEvery method in aiag Library on GitHub