How to Verify Probabilistic Consistency of Predictive Models

This paper addresses the question of whether a probabilistic predictor's answers to many conditional-probability queries are self-consistent, and whether this consistency can be verified in polynomial time. The authors formalize a predictive model as a pair of circuits (P, Q): a prediction circuit P that outputs probabilities P(yx) for target events y given contexts x, and a confidence circuit Q that outputs confidence scores, allowing the model to abstain when uncertain. Together, P and Q implicitly specify exponentially many probabilistic claims.

The paper defines the Model-Consistency Problem: Given a predictive model (P, Q) and a tolerance τ ≥ 0, is there an efficient way to verify that there exists µ such that Inc P,Q (µ) ≤ τ? The inconsistency measure is defined as:

Inc P,Q (µ):= sqrt((1/∥Q∥1) Σ x,y Q(x, y) · (µ(x ∧ y) − P (y x) · µ(x))2)

The authors emphasize that we do not ask whether the model's predictions are true of the world, nor whether they are calibrated against empirical data; we ask only whether the model's claims could all hold simultaneously under some distribution.

The main difficulty is scale: "A variable is indexed by a d-bit string, so the model may refer to n = 2 d Boolean variables, and as the sample space consists of the 2 n joint assignments to them, the natural alleged witness distribution µ which would certify consistency is a vector of real numbers whose length is doubly exponential in d." Even multi-prover interactive proofs handle witnesses that are exponentially long, whereas the natural witness here has doubly exponential description length.

The authors model the problem of verifying consistency of probabilistic predictors, building on classical work going back to Boole (1854). The mutual consistency of explicitly given probabilistic claims is a classical question, but the new subject is a predictive model whose claims can be exponentially many but are specified implicitly by a circuit.

The paper places Explicit-Consistency in NP, extending classical work on probabilistic satisfiability. The key result (Proposition 9, informal): "There is a verifier for explicit probabilistic consistency that runs in time O(m3(B + log m)2 + m2n), with a certificate of length O(mn + log B), consisting of the support of a sparse witnessing distribution together with a single auxiliary prime, i.e., Explicit-Consistency ∈ NP."

The proof uses Carathéodory's theorem to show that if a collection of m probabilistic claims is consistent, then some distribution supported on only m+1 points is consistent with it as well. The authors then bound the bit-length of the rational weights via Hadamard's inequality and Cramer's rule.

For the gapped case (Proposition 8, informal): Explicit-Consistency can be verified with a gap ε gap with an explicit witness of length O(nm + m log(1/ε gap)), and in time O(m2(n + B log(m/ε gap))).

The main result (Theorem 38 with Corollary 33, informal): Model-Consistency admits a polynomial-time Interactive PCP, verifying consistency up to an additive gap ε gap = 2(-poly(l,d,B)).

The protocol works as follows:

• The Prover encodes a sparse witnessing distribution as a proof oracle using a Reed–µller encoding

• The Verifier runs an encoding check (VerEnc) to certify the oracle is close to a valid codeword

• Two SumCheck protocols reduce the inconsistency computation and the total confidence ∥Q∥1 to evaluations at random points

• Two marginal checks (VerMarginoid) verify the marginals of the encoded distribution

• The Verifier directly evaluates the model circuits at a few points

The paper describes the protocol as a chain of reductions: an arrow E → E′ means that verifying E reduces to verifying E′, interacting with the Prover via the sub-protocol labeling the arrow.

The proof oracle is built from a locally-verifiable encoding of sparse distributions that enables delegation of marginal computation. This encoding, called Rµ, represents a distribution µ supported on m points by encoding the support vectors and weights as multilinear extensions. The encoding satisfies three properties: multilinearity, Booleanity (on the hypercube), and unit measure (weights sum to 2 B).

The paper presents this as a self-contained library, which may be used to verify other properties than consistency: the encoding, a codeword-validity verifier, and a marginal verifier.

The paper shows that Explicit-Consistency is NP-hard even for deterministic CPCs (where all probabilities are 0 or 1), via a reduction from Exact-kSAT. The reduction preserves the fraction of violated claims, and Lemma 15 shows that for deterministic CPCs: Viol(P) ≤ Inc(P) ≤ sqrt(Viol(P)).

Corollary 18 establishes that Model-Consistency is NEXP-complete.

A central step is showing the existence of a sparsely supported distribution that can serve as a proof witness. The authors use Carathéodory's theorem to show that any distribution can be replaced by one supported on at most m+1 points with the same inconsistency. They then prove bounds on the bit-length of the weights:

• For the gapped case: weights can be rounded to O(log(m/ε gap)) bits

• For the exact case: weights are rationals with common denominator representable in O(m log m + Bm) bits

The protocol (Algorithm 6, VerConsist) works as follows:

1. Read dimensions off the oracle signature and check bounds

2. Run VerEnc to verify the oracle is close to a valid encoding

3. Receive alleged inconsistency value v Inc and check it against the threshold

4. Run two SumChecks to reduce the inconsistency and total confidence to point evaluations

5. Run two VerMarginoid calls to verify marginals at the random point

6. Evaluate the model circuits directly at the random points

7. Accept if all checks pass

The soundness proof uses a case analysis: if the oracle is far from all codewords, VerEnc rejects; otherwise, the protocol behaves as if run on a genuine codeword, and the SumChecks and marginal checks bound the acceptance probability.

Section 8.3 replaces direct circuit evaluations with delegation of computation using doubly-efficient interactive proofs (VerifyMLE from [Tha13]), removing the dependence on circuit degree ∆ and replacing it with circuit depth D. This gives a Verifier that runs in poly(l, d, B, log(1/ε gap), 1/ε sound), plus the three VerifyMLE calls, O(P + Q + D(ld + log S)) field operations.

The paper motivates this work through AI safety: we do not want AI systems to manipulate us by giving conflicting answers in different contexts. The Scientist AI project aims to produce "an unbiased consistent Bayesian predictor that promises use not only in scientific prediction, but also as a guardrail for an AI agent: by predicting the probability that a proposed agent action causes a specified type of harm."

The authors argue that probabilistic consistency is a fundamental aspect of what is needed to trust AI systems. A highly inconsistent agent may be unable to reliably execute tasks, let alone reliably help with enhancing our knowledge.

The paper identifies several open problems:

• Can we train AI systems to produce proofs of self-consistency for restricted classes of distributions?

• What does it take to convince an auditor that an allegedly consistent model is mostly consistent?

• Can the protocol be instantiated over approximate SumCheck protocols so that the honest Prover need only estimate inconsistency?

• Other loss functions beyond l2 (e.g., cross-entropy)

• Zero-knowledge variants that hide user inputs

• Succinctness and delegation as separate axes

• Lemma 10: Bounds the perturbation of inconsistency when weights are rounded: if ∥α − α̂∥∞ ≤ δ, then Inc2 P(µ z,α̂) − Inc2 P(µ z,α) ≤ 2δ(m+1)3/m

• Lemma 11: Shows the density of fixed-precision binary numbers on the simplex

• Lemma 13: Bounds the common denominator of optimal weights via Hadamard's inequality: det M ≤ (2 B(m+2))(2(m+2))

• Claim 12: Combines these to show sparse witnesses exist at bounded precision with a gap

• Claim 16: Reduces Exact-kSAT to deterministic CPCs preserving violation fractions

• Lemma 15: For deterministic CPCs, Viol(P) ≤ Inc(P) ≤ sqrt(Viol(P))

Based on this paper, here are specific improvements to AI systems and what the improved systems can do:

• Improvement: Integrate the Interactive PCP protocol (VerConsist) as a verification layer in AI systems that output probabilistic predictions across multiple contexts.

• What the improved AI can do: Before deployment, an AI system can generate a certificate proving that its conditional probability claims are mutually consistent within a specified tolerance τ, without needing to enumerate all 2 n possible states. This catches logical contradictions in the model's beliefs (e.g., P(AB)=0.9 and P(BA)=0.1 when they should be related by Bayes' theorem).

• Improvement: Use Carathéodory-based sparse support (at most m+1 points) to construct compact certificates of consistency.

• What the improved AI can do: An auditor can request a short proof (polynomial in model size, not exponential in state space) that the model's claims are consistent. The AI can generate this proof efficiently, enabling third-party verification without access to training data or full model internals.

• Improvement: Incorporate the confidence circuit Q into the training objective, penalizing inconsistency weighted by confidence scores.

• What the improved AI can do: The system learns to abstain (output low confidence) on queries where its predictions would create inconsistencies, while maintaining high confidence only on self-consistent subsets. This prevents the confidently wrong but contradictory failure mode.

• Improvement: Use the gapped consistency check (ε gap = 2(-poly)) to allow approximate verification in resource-constrained settings.

• What the improved AI can do: In real-time applications (e.g., autonomous driving), the system can run a lightweight consistency check with a larger gap, trading verification precision for speed. If the check fails, it escalates to a full verification or falls back to a safer mode.

• Improvement: Replace direct circuit evaluation with doubly-efficient interactive proofs (VerifyMLE), reducing verifier complexity from circuit degree to circuit depth.

• What the improved AI can do: For deep neural networks (high depth, low degree per layer), the verifier can check consistency in time proportional to network depth rather than total parameter count, making verification feasible for models with billions of parameters.

• Improvement: Use the inconsistency measure Inc(P,Q) as a differentiable regularization term during training.

• What the improved AI can do: The model is trained to minimize both prediction error and self-inconsistency, producing predictors that are not only accurate but also logically coherent across different query contexts. This is particularly valuable for multi-task models or models queried in varied contexts.

• Improvement: Apply the protocol recursively to sub-models or components.

• What the improved AI can do: A large AI system can verify consistency of individual modules (e.g., perception, planning) separately, then verify cross-module consistency, localizing sources of inconsistency for debugging or targeted retraining.

• Improvement: Extend the protocol with zero-knowledge properties to hide sensitive inputs.

• What the improved AI can do: A medical AI can prove its diagnostic probabilities are self-consistent to a regulator without revealing patient data or the exact query contexts, enabling privacy-preserving audits.

• Improvement: Use the gap between the model's inconsistency and the threshold τ to calibrate confidence scores.

• What the improved AI can do: When the model is far from consistency, it automatically lowers confidence across all outputs; when comfortably consistent, it can be more assertive. This creates a natural uncertainty budget tied to logical coherence rather than just statistical calibration.

• Improvement: Use the marginal verifier (VerMarginoid) to check consistency of counterfactual queries.

• What the improved AI can do: An AI planning system can verify that its predicted outcomes under hypothetical actions (e.g., what if I take this route?) are consistent with its general world model, preventing contradictory plans or false confidence in counterfactual reasoning.

When a probabilistic predictor answers many conditional-probability queries, are its answers self-consistent, and can this be verified in polynomial time? This problem is of interest for AI safety, where safety is derived from honesty about probabilistic predictions of unwanted outcomes potentially caused by an AI action. We construct an interactive PCP as follows. Let a predictive model be specified by a probability circuit P and a circuit Q which outputs confidence in predictions. Together, P and Q implicitly specify exponentially many probabilistic claims. We show a protocol in which a polynomial-time verifier can verify the approximate consistency of (P,Q). The verifier is given the pair of circuits (P,Q), which it evaluates at only a few points; alongside them it is given a proof oracle, an encoding of a witnessing probability distribution allegedly consistent with the predictions of (P,Q), which it reads at a few locations while interacting with a single untrusted prover. En route, we must ensure the existence of a sparse witnessing distribution consistent with the model's predictions. To do so, we first consider witness distributions for the consistency of explicit probabilistic claims, rather than claims specified by a predictor: say m claims, each of the form Pr[Y = 1 X = x] = p, over n Boolean variables. Building on work initiated by Nilsson (Artif. Intell., 1986), we place l 2-approximate probabilistic consistency of explicit claims in NP, with certificates of length O(mn + log B) in the input bit-precision B; we further show how a small additive completeness-soundness gap removes the dependence on B. Together these results provide a complexity-theoretic foundation for certifying the self-consistency of probabilistic predictors. We view our interactive PCP as a first step toward training predictive models to prove their own consistency.