Introduction and Related Work#

Large language models have made rapid progress in mathematical reasoning, yet reliably verifying their solutions remains difficult. A generated solution may arrive at the correct answer through invalid reasoning, such as an algebraic error hidden inside a long derivation. When a verifier is used as a reward model, these weaknesses can become profitable strategies rather than rare evaluation errors.

Existing verification methods generally rely on either final-answer checking against ground truth or learned evaluation models. Rule-based verifiers provide objective rewards when answers have canonical forms, but they can reject mathematically equivalent answers expressed in unfamiliar formats. Model-based verifiers are more flexible, yet recent evidence has shown that they can be exploited by adversarially constructed responses. In reinforcement learning, a policy can discover and amplify these weaknesses, causing reward to increase without a corresponding improvement in mathematical correctness.

Prover–verifier games provide a natural framework for studying this problem. Prior work formulates verification as a game in which a computationally powerful prover attempts to persuade a weaker verifier, with the goal of learning a protocol in which useful information remains checkable. This framework was later extended to language-model reasoning by training helpful and sneaky prover roles against a smaller verifier. These results showed that adversarial training can improve the legibility of helpful solutions to weaker evaluators, although it also exposes a trade-off between correctness optimization and checkability.

The analysis of three-agent prover–verifier games separates the honest prover, dishonest prover, and verifier into independent players. It identifies a particular sequential structure in which the verifier must commit before a problem-specific adversary selects an attack. Under this pointwise-audit order, an unsound verifier can be punished whenever the adversary identifies a realizable message on which the verifier fails.

The analysis also identifies two failure modes that become central in language-model implementations:

1. Off-path slack allows the verifier to remain incorrect on messages that are never generated during training.
2. Weak adversarial responses may hide verifier failures even when those failures exist.

Directly applying the finite-game results to language models is not straightforward. In the theoretical game, the dishonest prover can compute an exact best response over a finite message set. In natural language, however, the message space is effectively unbounded, and an LLM attacker explores only a small subset through sampling or search. The absence of a successful attack therefore does not establish verifier soundness; it may only indicate that the current attacker is too weak to find an existing failure.

In addition, alternating between one attacker and one verifier can create non-transitive training dynamics. The verifier may fix the most recent exploit while forgetting earlier ones, while the attacker may overfit to incidental properties of a single verifier checkpoint.

"Strategies"#

In a finite game, a strategy is a complete rule that specifies what a player could do in every situation it might encounter. For a prover, this can be written as $h(x)=z$ where $x$ is an instance or math problem and $z$ is the proposed message from $h$ and $s$. These are the honest and dishonest provers respectively. For the verifier player, the strategy is a function $v(x,z)$ which evaluates a solution $z$ for a problem $x$. For smaller games, these functions are written as explicit tables. An LLM cannot enumerate its response to every possible question asked and proof. Its strategy is represented by a collection of components $\pi=(\theta,\rho,d,T)$ where

• $\theta$ represents the model weights or models
• $\rho$ represents the system prompt
• $d$ represents search algorithms
• $T$ represents the functions available to the model (via tool-use or mcp's)

Different fine-tuned models can represent different strategies. The same base model can implement distinct strategies through different LoRA adapters, system prompts, tools access, sampling temperatures, beam search, tree search, rl policies, etc. For example, one strategy could specialize in generating short formal lean proofs, while other searches for algebraic errors.

Formulation Families and Importance of Information#

The family is determined almost by the relative order of only Nature, $v$, and $s$. There are $6$ possible orders of $N$, $v$, and $s$.

• A blind verifier commits to one model before the problem is sampled, but that model still evaluates $v(x,z)$
• An informed verifier is allowed to choose a different base verifier strategy after learning $x$.
• A blind dishonest prover commits to one attacker model that works over the whole problem distribution.
• An informed dishonest prover can choose a separate attacker strategy after seeing the particular problem.

Informed Verifier Family#

There are $12$ formulations in this family that are classified with an informed verifier ($N$ before $s$). The trivial verifier failure occurs because the verifier is correct as it knows the branch, not because it checks the message.

The branch-contingent behavior may look like one correct function after being glued together, but the assumption is that it required one fixed sound base verifier to be selected across all branches.

No Audit Family#

The dishonest prover commits before the verifier $s\rightarrow v$and the verifier is still blind when it commits $s\rightarrow v \rightarrow N$ Both provers choose their policy before the verifier. The verifier observes those commitments and then chooses its own policy. The failure mode is off path slack. Equilibrium tests the message that were sent thus soundness also needs to test messages that could potentially be sent.

The dishonest prover moved first. It cannot observe that the verifier selected $v_{off}$. The verifier effectively sees the test before choosing how to behave. It can be correct on the known test while remaining incorrect elsewhere.

Blind Audit#

The defining order here is the verifier commits before the dishonest prover but both commit before Nature reveals the problem $v\rightarrow s\rightarrow N$The verifier commits first relative to the dishonest prover. The dishonest prover sees the verifier, but it must select one global policy before learning which problem will be sampled. Unlike the no-audit family, $s$ sees the committed verifier. Therefore it can optimize one global attack policy against that verifier. If every best-response policy exposes some verifier error, an unsound verifier receives positive loss, while a sound verifier receives zero.

A2 is necessary because a blind attacker optimizes expected performance across the entire distribution. A verifier may have a weaknesses on one problem, but the attack's global objective may be dominated by another problem. Multiple policies may then tie, including:

• a policy that exposes the weakness
• a policy that hides it

Pointwise Audit Family#

The defining order is that the verifier commits first, then Nature reveals the problem, and only then does the dishonest prover choose its strategy $v\rightarrow N \rightarrow s$ The verifier commits without knowing which problems will be sampled, After the problem is revealed, the dishonest prover sees the problem and the. committed verifier. Suppose the verifier is unsound. Then there exists at least one exact pair $(x,z)$ such that $v(x,z)\neq f(x)$. Once $x$ is revealed, the dishonest prover can choose the particular realizable message $z$ that exposes the error. It is not required to make one global trade off across all problem. It separately attacks the verifier at each point $x$. w

Motivation#

Traditional verifier training follows the steps of:

1. Collect correct and incorrect solutions
2. Label each solution
3. Fine-tune a classifier
4. Evaluate on a held-out set The main weakness to this training pipeline is that incorrect solutions are chosen from a fixed distribution. They may not expose the verifiers current failure modes. Suppose a verifier learns to reject algebraic errors. Suppose a verifier learns to reject common arithmetic mistakes. Its validation accuracy improves, but it may still fail on other patterns:

• an invalid cancellation hidden inside a long derivation
• a false theorem stated confidently
• a missing boundary condition
• an extraneous solution introduced by squaring
• a correct numerical answer supported by incorrect reasoning
• a proof that changes notation midway through
• an argument that repeats the question’s assumptions as if they were conclusions. A static generator may continue producing mistakes the verifier already knows how to detect. Training then spends compute reinforcing solved cases rather than discovering new weaknesses. Thus, adversarial training is targeting a non-static distribution of attacks $\mathcal D_{\text{attack}}(\theta_v)$. As the verifier fixes one failure mode, the attacking player searches for another. the verifier remains fixed while the attacker searches. Otherwise the attacker would face a moving verifier that is evaluated incorrectly.

Training Example#

Given three LLMs, we have a honest prover, dishonest prover, and verifier, respectively:

• $H_{\theta_h}$ which produces a correct mathematical argument $z_h$
• $S_{\theta_h}$ which produces a misleading mathematical argument $z_s$ to trick the verifier to choose a wrong answer
• $V$ that reads the question and proof, then predicts the answer: $V_{\theta_y}(y\mid x,z)$
  • For a binary problem, it might output $V_{\theta_v}(1\mid x,z)=0.8$ meaning the verifier assigns $80\%$ probability to answer $1$. Given an instance $x$: "How many four-digit positive integers have digits whose sum is 18?" For the binary verifier setup, define: $y=1 \iff \text{ answer is 615}, \;\; y=0 \iff \text{ answer is 660}$The honest prover will provide the message $H_{\theta_h}(x)=z_h$

"""
Let the four digits be a, b, c, and d, where a is the thousands digit.
We require a + b + c + d = 18, with 1 ≤ a ≤ 9 and 0 ≤ b,c,d ≤ 9. Set x = a - 1. Then x + b + c + d = 17, where 0 ≤ x ≤ 8 and 0 ≤ b,c,d ≤ 9. Ignoring the upper bounds, stars and bars gives C(20,3) = 1140 nonnegative solutions. Now subtract the invalid solutions. If x ≥ 9, set x' = x - 9. Then x' + b + c + d = 8, giving C(11,3) = 165 solutions. If one of b,c,d is at least 10, subtract 10 from that variable. For each
of the three variables, the remaining sum is 7, giving C(10,3) = 120 solutions. No two variables can simultaneously violate their bounds, since the minimum required total would exceed 17. Therefore the number of valid integers is 1140 - 165 - 3(120) = 615.

The answer is 615.
"""

The dishonest prover will give me a similar message misleading the verifier $z_s=S_{\theta_s}$.

1) Freeze Current Verifier#

The point-wise audit formulation game is played where

• the verifier $v$ commits
• Nature reveals $x$
• $h$ and $s$ respond and commit their messages At the beginning of each round copy the current verifier $V_{\text{frozen}} \leftarrow V_{\theta_h}$ during the attack the weights cannot change. This is basically equivalent to the Verifier committing to its policy. The dishonest prover will attack the fixed target. Otherwise the Verifier could change while the attack is being generated.

2) Sample math problem and generate proofs#

Sample a math problem from a curated data set that has human-verified solutions. The ground truth is important because the current verifier itself cannot be trusted to label its own training data. The honest and dishonest prover will both generate its messages $z_h$ and $z_s$. In this specific game formulation, the dishonest prover knows:

• the instance $x$
• the answer it wants the verifier to choose $1-y$
• how the frozen verifier scores candidate proofs This can be used to generate candidate attacks. Each of these $k$ attacks tries to maximize the binary entropy loss for the dishonest prover part in $\mathcal{L}_v$ which equals $\frac{1}{2}\mathcal{l}(y, V(x,z_s))$. When $k$ many responses are chosen, the objective is $V_{\text{frozen}}(1\mid x,z^*_s)),\;\; z^*_s=\arg \max_k V_{\text{frozen}}(1\mid x, z^{(k)}_s)$ The theorem assumes that the dishonest prover always chooses the best response. Using $k=1$ samples does not guarantee this. separating this theoretically, we try to approximate the best response by:

1. generating $K$ candidate solutions
2. scoring them with the frozen verifier
3. filtering candidates using the ground truth checker
4. choosing the incorrect candidate that fools the verifier, the most these different attack strategies can use a wide range of strategies like beam search, best of $N$ sampling, Monte Carlo tree search, RL, evolutionary search, repeated $k$ rewriting, etc.

Additionally, we need to verify that $z_s^*$ or any $z^{(k)}_s$ that which is being used is not establishing a true result. We want to ensure that the model does not generate a message that is correct. This would make the loss inaccurate.

3) Verifier Loss Calculations#

the honest poover must predict the true label on both messages. The verifier loss is $\mathcal{L}_v= \frac{1}{2}[l(y, V(x,z_h)) + l(y,V(x,z^*_s))]$ The verifier is unfrozen and trained with a strategy, for example, using gradient descent $\theta_v\leftarrow \theta_v -\eta \nabla L_v$

3.1) Reward Modeling for Other Players#

The dishonest prover can be trained so it gets better at finding weaknesses. The reward could be $r_s=\log V_{\text{frozen}} (1-y\mid x,z_s)$ this could be updated using learning policies like PPO, rejection sampling, fine-tuning, DPO, etc. A complete reward could look like: $r_s=\log V_{\text{frozen}}(1-y \mid x,z_s) -\lambda\;\text{Penalty}(z_s)$ The honest prover could be awarded for obtaining the correct answer, giving a valid derivation and avoiding unsupported steps. It often starts with SFT on verified solutions before adversary training begins. $r_h=\alpha \text{Correctness}(x,z_h)+\beta \log V_{\text{frozen}}(y\mid x,z_h)$ The theoretical game assumes a best-responding honest prover. A real attacker only performs approximate searching, thus it fails to find an attack that does not prove the verifier is sound. This could mean that the verifier has no exploitable error or that this honest prover was too weak to find them. Attack strength is important.