Verifying That a Predictor's Probabilities Don't Contradict Each Other

Paper: 2608.11181 Authors: Orr Paradise, Oliver Richardson, Yoshua Bengio, Shafi Goldwasser Categories: cs.CC, cs.AI, cs.LG

The Gap

The classical question is old and well understood. Boole asked it informally; Nilsson (1986) formalized “probabilistic logic” as a linear program; Georgakopoulos, Kavvadias and Papadimitriou (1988) showed the resulting decision problem (probabilistic satisfiability, PSAT) is NP-complete. The setup: you are handed $m$ explicit claims of the form $\Pr[Y=1 \mid X=x] = p$ over $n$ Boolean variables, and you ask whether a single joint distribution over $\{0,1\}^n$ makes all of them true at once.

Three limitations block the road from there to auditing an actual predictive model:

1. Claims must be listed. A neural predictor does not hand you $m$ claims. It hands you a function. Feed it any context $x \in \{0,1\}^n$ and it asserts a conditional probability, so it implicitly asserts $2^n$ claims. The LP now has exponentially many constraints and exponentially many variables, and the classical vertex/Carathéodory argument that bounds witness support by $m+1$ atoms gives you nothing.
2. Precision is swept under the rug. “The LP is feasible” is not the same as “there is a short certificate.” The witness distribution’s weights are real numbers; whether the problem is genuinely in NP depends on how bit-precision $B$ of the input enters the certificate length. Prior statements are loose here.
3. The verifier reads everything. NP-completeness means a certificate exists, not that a cheap auditor can use it. If the object under audit is exponential in size, you want sublinear, spot-check verification.

Meanwhile the AI-safety side of the literature audits models statistically: calibration curves, conformal prediction, held-out evaluation. All of those need ground truth, and none of them produce a proof. Debate-style protocols produce something proof-shaped but carry no complexity guarantee. So there is a genuine hole: no formal verification story for the one honesty property you can check without ground truth, namely that the model’s own answers don’t contradict each other.

PROBLEM: a predictor implicitly asserts 2^n conditional probability
         claims. Are they jointly realizable. Can a poly time
         verifier check that.
             |
             v
PRIOR ART: Boole / Nilsson 1986 -- consistency == LP feasibility
           Georgakopoulos+ 1988 -- PSAT is NP-complete
           blocked by: (a) claims must be listed explicitly
                       (b) bit precision B hidden in certificate size
                       (c) verifier must read the whole instance
             |
             v
ASSUMPTION: exact equality is the wrong target. Score inconsistency
            in l_2 and weight each context by the model own
            confidence Q. Slack buys sparsity.
             |
             v
METHOD: [sparse witness lemma] + [low degree encoding of the witness]
        + [sumcheck style interaction]  ==  an interactive PCP
             |
             v
EVIDENCE: explicit claims -- l_2 consistency is in NP with
          certificate O(m*n + log B) .. and O(m*n) once you allow
          a small additive completeness soundness gap
          implicit claims -- poly time verifier that evaluates
          P and Q at a few points + reads a few oracle bits
          + talks to one untrusted prover
             |
             v
CONCLUSION: self consistency of a probabilistic predictor is a
            certifiable property. Next step: train the model to
            emit its own certificate.

The Increment

One sentence: Before, “are these probability claims consistent” was an NP-complete question about a short explicit list; after, it is a property of a *circuit-specified predictor that a polynomial-time verifier can approximately check while looking at only a handful of points of the model and a handful of bits of an alleged witness.

Core Mechanism

The model is given as two circuits. $P$ is the probability circuit: on context $x$ it outputs the predicted $\Pr[Y=1 \mid X=x]$. $Q$ is a confidence circuit: on the same $x$ it outputs how much the model stands behind that prediction. That second circuit is not decoration, it is what makes the problem tractable. Demanding exact consistency across $2^n$ contexts is brittle and forces dense witnesses; instead the target becomes a confidence-weighted $\ell_2$ inconsistency score, roughly $\sum_x Q(x)\,\big(P(x) - \Pr_\mu[Y=1 \mid X=x]\big)^2 \le \epsilon$ for some distribution $\mu$. Consistency becomes a quantity, not a bit.

That relaxation is what buys the crucial structural fact: a sparse witness suffices. For explicit claims this is close to classical LP geometry — if $m$ constraints are satisfiable, some solution sits at a vertex with at most $m+1$ atoms, and the paper’s contribution is nailing down the bookkeeping so the certificate is $O(mn + \log B)$: essentially just the list of atoms (each an $n$-bit string) plus enough precision to pin down the weights. Allowing a small additive gap between the accept and reject thresholds removes even the $\log B$ term, because near-vertices with rounded weights are good enough. For the implicit, exponentially-many-claims case you cannot use vertices, so you need a sparsification argument that keeps the $\ell_2$ score small with polynomially many atoms.

Then comes the proof-system layer. The witness $\mu$ is written down as a low-degree encoding and handed to the verifier as a proof oracle — a long string the verifier reads at only a few locations, so that any local tampering is detectable. But the statement being proved is a sum over exponentially many contexts, and no fixed number of oracle queries can confirm a sum. That is what the interaction is for: the verifier runs a sumcheck-style protocol with a single untrusted prover, who supplies subtotals; the verifier randomly picks which subtotal to drill into, and after logarithmically many rounds the exponential claim has collapsed to a statement about one random point. At that point the verifier can finish alone, because it holds $P$ and $Q$ and can evaluate them itself, and it can read the corresponding location of the proof oracle. Neither ingredient works alone: the oracle commits the prover to a single witness it cannot revise mid-protocol, and the interaction compresses the exponential sum. Hence *interactive PCP.

              the model                            the certificate
   +----------------------------+        +-----------------------------+
   |  P : x |-> Pr[Y=1 | X=x]   |        |  sparse witness mu          |
   |  Q : x |-> confidence      |        |  atoms w_1 .. w_k in \{0 1\}^n
   +----------------------------+        |  plus weights               |
              |                          +-----------------------------+
              |                                       |
              |                              low degree extension
              |                                       v
              |                          [ PROOF ORACLE -- read at a
              |                            few locations only ]
              v                                       |
  claim:  sum over all 2^n contexts x of                |
          Q(x) * ( P(x) - Pr_mu[Y=1|X=x] )^2  <=  eps   |
              |                                        |
              v                                        v
     +--------------------------------------+
     |  VERIFIER   (polynomial time)        | <== sumcheck rounds ==>  PROVER
     |  - evaluates P and Q at a few points |     subtotals and        (untrusted
     |  - queries the oracle at a few spots |     random drill down     unbounded)
     |  - checks low degree + arithmetic    |
     +--------------------------------------+
              |
      accept  /  reject

The metaphor: auditing a bookmaker. A set of probability claims is inconsistent exactly when you can construct a Dutch book against it — a package of bets that wins money in every possible world. So think of the predictor as a bookmaker publishing odds on astronomically many conditional bets (“given this action, odds on harm”), and $Q$ as the stake it is willing to accept on each: it does not much matter if the odds are off on a bet the house won’t take.

The witness distribution $\mu$ is the bookmaker’s book of scenarios: a list of possible worlds with weights that, if you priced everything off them, would reproduce the published odds. The sparse witness lemma says the book does not need one line per possible world — a few hundred well-chosen scenarios reprice the whole board to within $\epsilon$. The proof oracle is that book deposited with a notary in tamper-evident form, so that erasing one line shows up in many places. The prover is the house’s accountant: unbounded, motivated, untrusted. The auditor cannot read the whole board or the whole book, so it asks the accountant for subtotals (“total exposure across this half of the board”), picks one at random, asks him to split it again, and keeps drilling. At the bottom of the drill-down sits a single bet, whose published odds the auditor computes itself from $P$ and $Q$, and one line of the notarized book, which it reads directly. If the accountant ever fudged a subtotal, the random drill-down catches it with high probability, because he had to commit to the book before the questions started. The verdict is not “the odds are correct” — the auditor never sees a race run. It is “these odds are internally arbitrage-free, up to $\epsilon$, weighted by the stakes the house accepts.”

Key Concepts

• Probabilistic consistency (probabilistic satisfiability): Suppose someone tells you $\Pr[\text\{rain\}] = 0.5$, $\Pr[\text\{wet grass\} \mid \text\{rain\}] = 1$, and $\Pr[\text\{wet grass\}] = 0.2$. Each number is individually plausible, and no pair obviously clashes, yet no distribution over the world satisfies all three at once — rain alone already forces wet grass to at least 0.5. Consistency asks: does there exist a single joint distribution over the $n$ variables reproducing every claim? Write one unknown per possible world ($2^n$ of them, each a nonnegative weight summing to 1) and each claim becomes a linear equation in those unknowns, so the whole question is a linear feasibility problem. That is Nilsson’s reformulation, and it is why the problem is in NP-hard territory rather than trivially easy: the variables are exponentially many, and you cannot afford to look at them all.

• Sparse witness: The reason the exponential LP is not fatal. Geometrically, a feasible region carved out by $m$ linear equations, if nonempty, has a corner, and a corner of the probability simplex under $m$ constraints touches at most $m+1$ coordinates. Concretely: if you made 50 probability claims and they are jointly satisfiable, there is a distribution supported on 51 specific worlds satisfying all 50. So the certificate is a short list of bit-strings, not a giant table. When claims are exponentially many this argument dies, and the paper’s relaxation to weighted $\ell_2$ error is what restores a sparse (poly-size) approximate witness — you no longer need to hit every claim exactly, only to keep the aggregate weighted error small, and a small set of scenarios can do that.

• Interactive PCP: Two verification tricks, welded together. A PCP is a proof written in a redundant, error-corrected format, so a verifier can read three or four random symbols and be convinced — any proof with a real flaw is flawed almost everywhere. An interactive proof is instead a conversation: the verifier’s unpredictable questions stop a lying prover from keeping its story straight. An interactive PCP (Kalai–Raz) gives the verifier both a fixed proof string it can spot-check *and a live prover to interrogate. You need both here for a specific reason: the object under audit is a distribution over $2^n$ worlds, far too big to send, so it lives in the oracle where the prover is bound to it; while the claim being checked is a sum over $2^n$ terms, which only interaction can compress into $O(\log)$ rounds.

Framework Shift

Before (Boole / Nilsson / PSAT):        After (this paper):

  m claims listed explicitly              circuits (P Q) handed over
    c_1 .. c_m                              implicitly 2^n claims
        |                                          |
        v                                          v
  LP over 2^n world weights               confidence weighted l_2
    feasible.  yes / no                     inconsistency score
        |                                          |
        v                                          v
  certificate == a vertex                 sparse witness mu with
    support m+1  precision B                poly many atoms
        |                                          |
        v                                          v
  verifier reads the whole                low degree encoding
    instance and certificate                + sumcheck interaction
        |                                          |
        v                                          v
  cost poly(m n B)                        verifier touches O(1) spots
  a yes / no answer about                   of P Q and of the proof
  a list someone wrote down               a graded answer about the
                                            model itself

From a decision problem about a written-down list to a proof system about a running model, the core shift is that consistency stops being a boolean property of claims and becomes a locally auditable, confidence-weighted quantity of the predictor that produces them.

Expert Assessment

Problem choice: A real gap, and a well-chosen one. The honesty property you can check without ground truth is coherence, and nobody had made that formally checkable for a model-sized object. It also sits naturally in the authors’ trajectories — Paradise and Goldwasser on self-proving models, Richardson on quantitative inconsistency in probabilistic graphical structures, Bengio on safety-via-honest-world-models. My reservation is about how much weight the safety framing can bear. A predictor that outputs 0.5 everywhere is perfectly self-consistent and perfectly useless; a coherent but wrong world model passes this audit cleanly. The paper appears to know this (it says “safety is derived from honesty,” not from consistency), but readers will over-read it. Consistency is a necessary condition and a cheap continuous monitor, not a safety guarantee.

Method maturity: Mostly skilled assembly rather than a new hammer — LP geometry for sparsity, low-degree extension, sumcheck, the IPCP model, all off the shelf. The genuine technical content is (a) getting a sparse witness to exist under the approximate, confidence-weighted notion when the claim set is exponential, and (b) the precision accounting, including the neat observation that a small completeness–soundness gap makes the $\log B$ dependence vanish. That second point is the kind of detail that separates a real theorem from a hand-wave, and it is good that they did it. On simpler alternatives: for practical auditing you could just Monte-Carlo it — sample contexts, sample worlds from the model, estimate the inconsistency score, and get a statistical guarantee with no proof machinery at all. The proof system’s advantage is soundness against an *adversarially constructed model, and it is a fair question whether that threat model matches a trained network. It does match a model that has been fine-tuned to game its own audit, which is presumably the point.

Experimental integrity: There are no experiments; this is a complexity-theory paper and should be read as one, so the honest evaluation is about theorem statements rather than baselines. Two things I would push on in review. First, the guarantee is an *average over an exponential context space, weighted by the model’s own confidence: a model can be wildly incoherent on a tiny but safety-critical set of contexts, or simply set $Q$ low there, and still pass with a tiny $\ell_2$ score. Who audits $Q$? Second, the additive completeness–soundness gap that removes the precision dependence needs scrutiny — if the gap is not quantitatively small relative to $\epsilon$, the theorem is cheap. I am reading from the abstract on the internal structure of the sparsification argument, so treat my reconstruction of it as informed inference, not verified fact.

Writing quality: The abstract is unusually clear about its own logical order, which is a good sign. The predictable weak spot in papers of this shape is the bridge between the theorem and the motivation. The section that would most elevate the paper is an explicit adversary analysis: given a model that wants to look consistent, exactly what can it still get away with — concentrating inconsistency where $Q$ is small, on sparse context sets, on the specific queries a downstream user cares about? Second, “a first step toward training models to prove their own consistency” needs at least a concrete sketch of how a model would emit the proof oracle, or it reads as a promissory note.

Verdict: weak accept — a well-posed and genuinely new formulation with correct-looking machinery and modest technical depth, whose stated guarantee (average, self-weighted, approximate) is considerably weaker than the safety story surrounding it.

Takeaways

Concrete things that transfer:

• The confidence circuit as an escape valve. Letting the system say “I don’t stand behind this one” is what makes verification tractable, because you only hold it to what it commits to. That is a reusable design pattern for any audit scheme: pair every prediction with a declared stake, verify against the stakes, and separately audit whether the stakes are honestly declared. Adopt the pattern *and remember the second half, which this paper leaves open.
• Sparse witnesses make coherence auditing practical today, no PCP needed. The lemma says a few dozen weighted scenarios can reprice a large set of conditional claims. Operationally: ask an LLM for $k$ concrete possible worlds plus weights, then check its stated conditional probabilities against that little empirical distribution. You get a quantitative incoherence number from a handful of queries, with no proof system, no ground truth, and no labels.
• Consistency as a differentiable loss. The confidence-weighted squared inconsistency score is exactly the shape of a self-supervised regularizer: sample contexts, sample from a proposed witness, penalize weighted squared mismatch. This is where the paper’s “train models to prove their own consistency” line actually cashes out, and it connects directly to existing consistency-loss and amortized-inference training.
• The framing itself. Split model auditing into honesty (internal coherence — no data required, checkable continuously, potentially adversarially sound) and accuracy (needs ground truth, expensive, always lagging). Most evaluation effort goes into the second. The first is cheaper than people assume, and this paper is the argument that it can be made rigorous.