Paper deep dive
How to Verify Consistency of Probabilistic Claims
Orr Paradise, Oliver Richardson, Yoshua Bengio, Shafi Goldwasser
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 93%
Last extracted: 8/16/2026, 3:53:19 AM
Summary
This paper addresses the problem of verifying the self-consistency of probabilistic predictors, which is critical for AI safety. The authors define a predictive model as a pair of circuits (P, Q) and propose an interactive Probabilistically Checkable Proof (PCP) system. This system allows a polynomial-time verifier to check if a model's probabilistic claims are consistent with some underlying probability distribution. Key contributions include placing the 'Explicit Consistency' problem in NP using sparse Carathéodory witnesses and constructing an Interactive PCP for 'Model Consistency' that handles exponentially many implicit claims via a proof oracle encoding a sparse witnessing distribution.
Entities (12)
Relation Signals (9)
Interactive PCP → verifies → Model Consistency
confidence 97% · We show a protocol in which a polynomial-time verifier can verify the approximate consistency of (P,Q).
Explicit Consistency → belongstocomplexityclass → NP
confidence 96% · we place l_2-approximate probabilistic consistency of explicit claims in NP
Predictive Model → composedof → Circuit Q
confidence 95% · Let a predictive model be specified by a probability circuit P and a circuit Q
Predictive Model → composedof → Circuit P
confidence 95% · Let a predictive model be specified by a probability circuit P and a circuit Q
Interactive PCP → uses → Proof Oracle
confidence 94% · alongside them it is given a proof oracle, an encoding of a witnessing probability distribution
Proof Oracle → encodes → Carathéodory Witness
confidence 92% · the proof oracle encodes the witness, a sparsified probability distribution
Model Consistency → belongstocomplexityclass → MIP
confidence 90% · places Model-Consistency in MIP as a black-box corollary
AI Safety → motivates → Model Consistency
confidence 88% · This problem is of interest for AI safety
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract: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.
Tags
Links
- Source: https://arxiv.org/abs/2608.11181v1
- Canonical: https://arxiv.org/abs/2608.11181v1
Trouble viewing inline? Open PDF directly →
Full Text
271,309 characters extracted from source content.
Expand or collapse full text
How to Verify Consistency of Probabilistic Claims Orr Paradise Oliver Richardson Yoshua Bengio Shafi Goldwasser Affiliation: EPFL Université de Montréal, Mila -- Quebec AI Institute, LawZero MIT, UC Berkeley Abstract When a probabilistic predictor answers many conditional-probability queries, are its answers self-consistent—and if so, can this be verified in polynomial-time? This problem is of interest for AI safety, when safety is derived from honesty about probabilistic predictions of unwanted outcomes potentially caused by an AI action. To address it, 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. P and Q together implicitly specify exponentially many probabilistic claims. We show a protocol in which a polynomial time verifier can verify (P,Q)(P,Q)’s approximate consistency. The verifier is given the pair of circuits (P,Q)(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)(P,Q), which it reads at a few locations while interacting with a single un-trusted prover. En-route to the above result, we need to ensure the existence of a sparse witnessing probability distribution consistent with the model predictions. To do so, we first consider witness distributions for the consistency of explicit (rather than specified by a predictor) probabilistic claims: say m claims, each of the form “Pr[Y=1∣X=x]=p [Y=1 X=x]=p”, over n Boolean variables. Building on a body of literature initiated by Nilsson (Artif. Intel. 1986), we place ℓ2 _2 approximate probabilistic consistency of explicit claims in NP with certificates of length O(mn+logB)O(mn+ B) in the input bit-precision B; and further show how a small additive completeness–soundness gap removes dependence on the model’s precision B. This will be important for our interactive PCP constructions. Together these results provide a complexity-theoretic foundation for certifying the self-consistency of probabilistic predictors. We view the explicit Interactive PCP we present as the first step toward the eventual training of predictive models to prove their own consistency. †footnotetext: Correspondence to: papers@orrp.net, oliver.richardson@umontreal.ca 1 Introduction Suppose a probabilistic predictor claims that Pr[X=1]=0.9 [X=1]=0.9, Pr[Y=1∣X=1]=0.9 [Y=1 X=1]=0.9, and Pr[Y=1]=0.8 [Y=1]=0.8. Although each pair of answers is plausible in isolation, the three cannot all be correct, since the first two imply that Pr[Y=1]≥0.81 [Y=1]≥ 0.81. Yet intuitively the degree of inconsistency is relatively small. A predictor that implicitly contains the answers to many overlapping probability questions can exhibit much more complex versions of the same defect: subsets of claims may make sense locally, yet there is no single probability distribution that is consistent with them all. Is it possible to efficiently verify that the degree of inconsistency within a predictive model (e.g., the weights of a large neural network) is small? We remark that this question arises naturally in the context of AI safety: we do not want AI systems to manipulate us by giving conflicting answers in different contexts. The currently most advanced general-purpose AI systems show signs of misalignment, sometimes acting towards goals that go against the human designers’ intentions (BCP+ 25). The Scientist AI BCF+ 25; BRG+ 26 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. This approach can only work if the guardrail is based on a predictor that reflects a consistent probability distribution about events in the world, chosen in a non-strategic way (such as an approximation of a Bayesian posterior). Self-consistency, and coherence with the observed facts, are properties that are more generally desirable for AIs. Indeed, consistent AI systems are also envisioned for scientific discovery: they will generate hypotheses, assign them probabilities in light of the available evidence, and update those probabilities as new information arrives—and in a way that is not designed to please a specific human user or reflect cultural biases inconsistent with facts. Such scientific reasoning is inherently probabilistic: a system does not necessarily know which hypothesis is true, but it must reason coherently under uncertainty. Whereas in the traditional mathematical claim setting we may ask a model to prove that a definite answer is correct (cf. hallucination), the natural question here is different: do the model’s probabilistic claims correspond to a single coherent view of a (probabilistic) world? And if perfect coherence is too much to ask of a learned model ZG 24, is it approximately consistent, up to some threshold? Rewording this question using the terminology of Interactive Proof systems GMR 89, we ask: Can powerful but un-trusted Prover(s) convince an efficient Verifier that the probabilistic claims made by a predictive model are jointly consistent? In this paper, we answer these question(s) affirmatively. Predictive Model Consistency We formalize a predictive model by a pair of circuits (P,Q)(P,Q): a prediction circuit P and a confidence circuit Q. • P is a circuit, such as a neural network, that takes as input a description x of a context consisting of values assigned to a set of Boolean variables, and a variable y representing the target event of interest, and produces a (rational) number p=P(y∣x)∈[0,1]p=P(y x)∈[0,1] that is to be interpreted as “the probability of y given x equals p”, i.e., “Pr[y∣x]=p [y x]=p.” • Q(x,y)Q(x,y) represents the confidence of the model in its prediction. This in particular allows the model to abstain from making predictions when uncertain and set Q=0Q=0. Informally, we say that the model (P,Q)(P,Q) is (approximately) consistent if there exists a joint distribution μ over all variables that (approximately) agrees with P on all possible inputs where Q>0Q>0, in the sense that violations of μ(y∣x)≈P(y|x)μ(y x)≈ P(y|x) are small in aggregate over queries (x,y)(x,y), weighted by Q. Formally, we propose the following measure of inconsistency of a distribution μ, with respect to a model (P,Q)(P,Q). Writing ‖Q‖1\|Q\|_1 for the sum of all confidence scores over all queries (x,y)(x,y), the model inconsistency is given by IP,Q(μ)≔1‖Q‖1∑x,yQ(x,y)⋅(μ(x∧y)−P(y∣x)⋅μ(x))2 _P,Q(μ) 1\|Q\|_1 _x,yQ(x,y)· (μ(x y)-P(y x)·μ(x) )^2 (1) The proposed measure, which has been studied in the past Pot 14, is a simplified variant of the inconsistency measure developed in the theory of probabilistic dependency graphs RH 21; Ric 22, which unifies and justifies many loss functions in machine learning via a natural information-theoretic measure of inconsistency. In contrast to RH 21; Ric 22 (which uses relative entropy and thus requires averaging logarithms of real numbers), we use ℓ2 _2 norm directly which allows us to work with polynomials and bring some of the machinery of interactive proofs to bear on the current problem. Furthermore, we believe it is better suited to the foundations of BCF+ 25. Putting it all together, the technical question we pose is The - Model-Consistency Problem: Given a predictive model (P,Q)(P,Q) and a tolerance τ≥0τ≥ 0, is there an efficient way to verify that there exists μ such that IP,Q(μ)≤τ _P,Q(μ)≤τ? We 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. This is the probabilistic analogue of logical consistency: a collection of deterministic claims is consistent if some assignment satisfies all of them, and a collection of probabilistic claims is consistent if some distribution does. Consistency is thus a necessary condition for trust rather than a sufficient one, and a model can certainly be coherent and wrong. Whereas consistency does not imply certainty, an incoherent model is not merely uncertain: it is internally inconsistent, and its answers cannot be understood as arising from any single probabilistic belief state. The Verification Challenge So, how can we hope to verify model consistency as defined above? The difficulty is one of scale. A variable is indexed by a d-bit string, so the model may refer to n=2dn=2^d Boolean variables, and as the sample space consists of the 2n2^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. This is an enormous object. Even putting aside concerns about real numbers and precision, it is hard to fathom how a verifier could efficiently compute or verify all the required marginals. For example, even Multi-Prover interactive proofs handle statements whose witnesses are exponentially long BFL 91, whereas the natural witness for our problem, the distribution μ, has doubly exponential description length. Thus, it is not clear, a priori, that a probabilistic polynomial-time Verifier can verify the consistency of a model with any amount of help. The Sparse Support Distribution A central step is to show the existence of another, “sparsely” supported, distribution that can serve as a proof witness in place of the naive one. Our route goes through a closely-related sub-problem. Rather than considering exponentially many variables encoded by a circuit, consider just n=dn=d variables, and rather than letting a circuit implicitly encode exponentially many claims, suppose that they are given as an explicit Collection (i.e., multiset) P of Probabilistic Claims, referred to as a CPC hereafter. We call a CPC P consistent if there exists a joint distribution μ that agrees with all constituent claims, and focus on a notion of “approximate consistency” measured by a normalized ℓ2 _2 norm. Given a CPC P and a tolerance τ≥0τ≥ 0 the problem Explicit Consistency is to decide whether there exists a probability measure μ∈Δ(2n)μ∈ (2^n) over the n-hypercube of joint variable assignments such that I(μ)≔1||∑(x,y,p)∈(μ(x∩y)−p⋅μ(x))2≤τ. _P(μ) 1|P| _ (x,y,p) (μ(x∩ y)-p·μ(x) )^2≤τ. It is not hard to see that - Explicit-Consistency is NP-hard, as in the restricted case of tolerance τ=0τ=0 and probabilities p∈0,1p∈\0,1\, it essentially encodes a constraint satisfaction problem (CSP), from which this problem inherits hardness of approximation (see also Section 6). But is it in NP, PSPACE, EXP, NEXP? The obvious candidate for a consistency witness is a joint distribution μ∈[0,1]2nμ∈[0,1]^2^n, which would seem to require exponential time and space to verify, putting aside issues of precision. At least in the consistent setting (τ=0τ=0), however, this is not the obstacle it appears to be: classical small-model theorems FHM 90; KM 94; GKP 88 show that a consistent collection of m claims is witnessed by a distribution supported on O(m)O(m) points, with probabilities that are rationals of polynomial bit-length, which places that case in NP (see Section 3). Prior work formalizing inconsistent settings (τ>0τ>0) has suggested the problem to be harder KN 95; RHS 23. What our setting needs is that this survives the passage to approximate consistency, and at a precision fine enough that the witness can be written into a proof oracle. - Explicit-Consistency: verifying m explicit claims- Model-Consistency: verifying an entire predictive modelPr[y1∣x1]=p1 [y_1 x_1]=p_1⋮ Pr[ym∣xm]=pm [y_m x_m]=p_mCPC Pshort proofVerifierread in fullaccept/rejectPredictive model (P,Q)(P,Q)exponentially long proof oracleVerifierProvertwo queriesinteractionpoly queriesaccept/reject Figure 1: Left: m probabilistic claims, collected, e.g., as the outputs of a predictive model, are verified against a short proof certificate that the Verifier reads in full (- Explicit-Consistency; Proposition 9). Right: the entire model is verified in one go via an Interactive PCP; the Verifier evaluates the model at two points, reads polynomially many positions of an exponentially long proof oracle, and interacts with a single untrusted Prover (- Model-Consistency; Theorem 32). In both settings, the Verifier should accept if its input is probabilistically consistent, and reject otherwise. In this paper we resolve both problems. We proceed to detail our full set of contributions: modeling and results. 1.1 Summary of Contributions Throughout the paper, we let n be the number of Boolean variables in the system, m:=||m:=|P| be the number of claims in the CPC, and B be the maximum binary precision among those claims. Formalizing verifiable consistency. Our first contribution is the above modeling of the problem of verifying the consistency of a probabilistic predictor, such as that of the ScientistAI BRG+ 26; BCF+ 25. The mutual consistency of explicitly given probabilistic claims is a classical question, going back to Boo 54 (see Section 3); our new subject is a predictive model, whose claims can be exponentially many but are specified implicitly by a circuit, and our goal is not to decide consistency but to verify it against an untrusted Prover. Short witnesses for explicit consistency. We place - Explicit-Consistency in NP, extending a classical line of work on probabilistic satisfiability (see Section 3 for related works). Proposition (Proposition 9, informal). There is a verifier for explicit probabilistic consistency that runs in time O(m3(B+logm)2+m2n)O(m^3(B+ m)^2+m^2n), with a certificate of length O(mn+logB)O(mn+ B), consisting of the support of a sparse witnessing distribution together with a single auxiliary prime, i.e., -∈ Explicit-Consistency∈ NP. Next, by introducing a very small gap11 1 The gap is between values of the inconsistency measure: given a valid certificate it accepts whenever I()≤τ−εgap (P)≤τ- _ gap, it rejects every certificate whenever I()>τ (P)>τ, and for I() (P) in between no guarantee is made (Proposition 8). between the completeness and soundness guarantees, we obtain a witness whose weights are written out explicitly, at low precision, and which the Verifier checks rather than computes. We note that at exact precision the weights alone grow quadratically in the number of claims, which is likely prohibitively expensive given that OpenAI, at the time of writing, serves over 2 billion queries per day. It is important to pay careful attention to the length of the proof, when envisioning deployment of the Interactive PCP below, where the witnessing distribution will need to be written out explicitly, weights included, inside the proof oracle. Proposition (Proposition 8, informal). - Explicit-Consistency can be verified with a gap εgap _ gap with an explicit witness of length O(nm+mlog(1/εgap))O(nm+m (1/ _ gap)), and in time O(m2(n+Blog(m/εgap)))O(m^2(n+B ( m _ gap))). An Interactive PCP for model consistency. Our main result is an Interactive PCP (a proof oracle combined with an interactive proof with a single prover KR 08) for - Model-Consistency, thereby showing the first probabilistically checkable proof system for model consistency. Theorem (Theorem 38 with Corollary 33, informal). - Model-Consistency admits a polynomial-time Interactive PCP, verifying consistency up to an additive gap εgap=2−(ℓ,d,B) _ gap=2^- poly( ,d,B). Reed–μ : a marginal-verifiable encoding of distributions. The proof oracle at the heart of our protocol is built from a primitive that may be of independent interest: a locally-verifiable encoding of sparse distributions that enables delegation of marginal computation (Section 7). We present it 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. Improvements to its parameters would carry over directly to Theorem 38 (see Remark 34). Distributions as witnesses. Combining the existence of NP witnesses for - Explicit-Consistency and = MIP= NEXP BFL 91 places - Model-Consistency in MIP as a black-box corollary, (Corollary 18), but here we go substantially further. Building on the low-precision (gap) Carathéodory witness of Proposition 8, we give a direct construction, of an Interactive PCP in which the proof oracle encodes the witness, a sparsified probability distribution, and the interaction reduces approximate consistency to point queries on that distribution. The distinction is not merely cosmetic: the generic derivation compiles the problem into a computation-checking instance, losing the fact that the witness is a probability distribution and that the claims are conditional-probability constraints, whereas the explicit protocol preserves this structure. Put differently, where the IP, MIP and PCP tradition encodes proofs of deterministic mathematical facts, the object encoded here is a distribution. The protocol that drives this reduction and its analysis are developed in Section 8. We believe that for sub-classes of probabilistic predictions which arise in an AI setting, an Interactive PCP with efficient provers can be developed in the Self-Proving model of AGPR 25. The two roles of “the prover” in an interactive PCP, a stateless proof oracle and a stateful Prover, can be played by a single model, assuming the Verifier can control its context: reset before each oracle query, and carried across interactive rounds (see Remark 1). Finally, we consider pointing the way to a new era for interactive and probabilistic proofs, a contribution in its own right. Our protocol extends the classical toolkit of probabilistic proof systems (multilinear extensions, the SumCheck protocol, self-correction), now aimed at a new kind of problem domain. Ultimately, we argue, 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. Indeed, much of training and inference in machine learning can be viewed as the process of resolving inconsistencies in probabilistic models Ric 22; Ric 24. Being highly intelligent and useful does not ensure consistency, and it is at this point inconsistency becomes a safety concern: we do not want highly intelligent systems whispering different things in our ears, which can be manipulative and dishonest. For these reasons, training for consistency is a key part of the Scientist AI approach to designing safe AI systems BCF+ 25—especially when combined with probabilistic claims that enforce consistency with a Bayesian posterior. Indeed, the Scientist AI they envision is essentially a circuit that implicitly encodes all succinctly specified probabilistic claims; for such a system, consistency is not a technical nicety but part of what it means to behave as a coherent scientific reasoner. Finally, many open problems emerge. Can we train AI systems to produce proofs of self-consistency of their claims for restricted classes of distributions? What exactly does it take to convince an auditor that an allegedly consistent model is, in fact, (mostly) consistent? We leave these questions to future work. 2 Technical overview This section describes the ideas behind our two main results, the two verification settings of Figure 1; the full proofs occupy the remainder of this paper. Section 2.1 outlines our proof that consistency admits a sparse witness: if a CPC of m claims is consistent, then some distribution supported on only m+1m+1 points is consistent with it as well, and in fact one whose exact description takes polynomially many bits, placing - Explicit-Consistency in NP. Section 2.2 uses this witness as its starting point: to verify the consistency of a predictive model, whose implicit claims are exponentially many, the Prover encodes a sparse witnessing distribution as a proof oracle, and the Verifier tests the model’s inconsistency against this encoding. 2.1 -∈ Explicit-Consistency∈ NP and a low-precision witness for the gapped case We start by describing the techniques used to establish the NP-verifier for - Explicit-Consistency. Here the instance is explicit: a CPC P of m probabilistic claims (x,y,p)(x,y,p) over n variables, together with a tolerance τ≥0τ≥ 0, and the question is whether some distribution μ∈Δ0,1nμ∈ \0,1\^n satisfies I(μ)=1m∑(x,y,p)∈(μ(x∩y)−p⋅μ(x))2≤τ. _P(μ)= 1m _(x,y,p) (μ(x∩ y)-p·μ(x) )^2\;≤\;τ. The natural witness is the distribution itself, and therein lies the difficulty: a priori, μ is an arbitrary vector of 2n2^n nonnegative reals summing to one. Because the degree of inconsistency can be viewed as an ℓ2 _2 norm of an m-dimensional constraint residual vector (the vector of the m summands above), Carathéodory’s theorem guarantees the existence of another distribution μ′μ supported on only m+1m+1 points. We call these points z, and the distribution over them α. Thus we refer to a pair (z,α)∈(0,1n)m+1×[0,1]m+1(z,α)∈(\0,1\^n)^m+1×[0,1]^m+1 that has the same inconsistency as μ as a Carathéodory Witness. In symbols: for every μ∈Δ0,1nμ∈ \0,1\^n there exist support points z=(z1,…,zm+1)z=(z_1,…,z_m+1) with zj∈0,1nz_j∈\0,1\^n and weights α∈Δ[m+1]α∈ [m+1] such that I(μz,α)=I(μ),where μz,α(ω)≔∑j=1m+1αj 1[zj=ω]. _P( _z,α)= _P(μ), _z,α(ω) _j=1^m+1 _j\, 1[z_j=ω]. However, Carathéodory’s theorem only guarantees the existence of a sparse vector of real weights; the remaining work, which is where our analysis departs from the classical small-support arguments (see Section 3), is to obtain a distribution μ′μ representable exactly, by rational numbers of polynomial bit-length. To do this, we start by fixing the identities z of the support points in the Carathéodory witness, and formulate the problem as a convex optimization problem, specifically a quadratic program: writing Vz∈ℤm×(m+1)V_z ^m×(m+1) for the matrix whose jjth column lists the constraint residuals of the single point zjz_j, rescaled to integers, the best weights for the support z are those minimizing ‖Vzα‖22\|V_zα\|_2^2 subject to α≥0α≥ 0 and ∑jαj=1 _j _j=1. Therefore, the square in our ℓ2 _2 measure of inconsistency plays a critical role: it turns the stationary conditions of the optimization problem into a system of linear equations. Concretely, on the support of an optimal α the only active constraint is that the weights sum to one, and setting the gradient of the Lagrangian to zero gives the linear system [2VzVz0][αλ]=[1] bmatrix2V_z TV_z&1\\ 1 T&0 bmatrix bmatrixα\\ λ bmatrix= bmatrix0\\ 1 bmatrix over the support, where λ is the multiplier of the sum-to-one constraint (Equation 5). We then argue that the size of the coefficients in this linear system of equations is small by Hadamard’s inequality, which bounds the magnitude of the determinant of a matrix; finally, we bound the denominator of the solution via Cramer’s Rule. In fact, the Verifier need not receive the weights at all: given the support, it solves this very system itself, exactly, and the determinant bounds now control its running time rather than the certificate’s length. The certificate for Proposition 9 is thus the support, O(mn)O(mn) bits, together with a single prime of O(logm+logB)O( m+ B) bits, which lets the Verifier certify that the system is non-singular before it solves, and seeds the exact solve. Finally, the gapped case, which our Interactive PCP requires because its proof oracle must store the weights explicitly: the exact rational weights above may need O(m(B+logm))O(m(B+ m)) bits each, but rounding each weight to O(log(1/εgap)+logm)O( (1/ _ gap)+ m) bits perturbs the squared inconsistency by at most εgap2 _ gap^2 (Lemma 10), and the completeness gap leaves exactly this much room: (τ−εgap)2+εgap2≤τ2(τ- _ gap)^2+ _ gap^2≤τ^2. This is 12, which yields the logarithmic-precision witness of Proposition 8. 2.2 An IPCP for - Model-Consistency We first briefly recall some probabilistic proof systems. In an interactive proof GMR 89, a polynomial-time Verifier tosses coins and exchanges messages with an all-powerful but untrusted Prover,22 2 Throughout this paper, the Prover is always written out in words; the symbol P is reserved for the model’s probability circuit. then accepts or rejects; the requirement is that some Prover convinces it of every true claim (completeness), and that no Prover strategy convinces it of a false one, except with small probability (soundness). In a probabilistically checkable proof (PCP) AS 98; FRS 94 there is no interaction: the proof is a fixed string, possibly far too long to read in full, of which the Verifier inspects a few randomly chosen locations. An Interactive PCP ( IPCP) KR 08 combines the two: the Prover first commits to a proof string (the proof oracle), and the interactive proof is then carried out, during which the Verifier may also query the oracle (Definition 29). The essential distinction is that the oracle is stateless: its answer at each location is fixed in advance, whereas the Prover answers each message having seen those that preceded it. Next, the cast (Figure 1, right). The instance is the model itself: the circuits (P,Q)(P,Q) and a tolerance τ, all held by the polynomial-time Verifier, which can afford to evaluate the circuits at a point but not to enumerate their claims. A witness is a distribution μ attaining IP,Q(μ)≤τ _P,Q(μ)≤τ. As the model can be viewed as making 2Θ(ℓd)2 ( d) implicit probabilistic claims, even the sparse witness of Section 2.1 is an exponentially long object, with each of its support points being an assignment to all n=2dn=2^d variables. Obviously, no polynomial-time Verifier can read such a witness in full, and it is thus encoded in a proof oracle π: an exponentially long string of which the Verifier reads a few locations of its choosing, while the untrusted Prover assists, interactively, in reducing statements about all of π to those few locations. In contrast to the PCP tradition, in which the string behind the oracle encodes a proof, here it encodes a distribution. The Verifier’s task boils down to confirming a single inequality: that the squared inconsistency I2(μ) ^2(μ) of the model (P,Q)(P,Q) stays below the threshold τ2τ^2. It must do so given only the access above: point queries to π, which allegedly encodes μ, and point evaluations of the model. Reducing this inequality to queries to π and evaluations of the model is the work of Section 8; Figure 2 depicts the reductions involved. For readability, this overview omits all normalization factors; they are restored in the full treatment of Section 8.2. It will be instructive to present the protocol as a sequence of randomized reductions: reducing a statement the Verifier cannot afford to check (a sum of 2Θ(ℓd)2 ( d) terms compared against a threshold), to statements that it can (evaluations of P P, Q Q and π). The Verifier could not carry out such a reduction on its own; instead, each step is performed in interaction with the untrusted Prover, and is sound in the sense that if the statement before the step is false then, with high probability over the Verifier’s coins, so is the statement after it. The reduction used for the sums is the famous SumCheck protocol LFKN 92, viewed as a randomized reduction from the claim that an exponential sum of a low-degree polynomial equals a given value to the claim that the polynomial takes a given value at a single random point (cf. Mei 13; CFS 17). Figure 2 depicts the protocol in this light: each arrow is one reduction, and the leaves are the only statements the Verifier checks directly. Why should the proof oracle be an encoding of that table, rather than the table itself? For two reasons. The quantities that the model’s claims refer to are marginals of μ, each a sum of exponentially many of its entries; storing the table as (the evaluations of) low-degree polynomials over a large field turns each marginal into a sum of polynomial values, exactly the kind of statement that SumCheck reduces to a few point queries. The Verifier must check, by reading a few locations and with the Prover’s interactive help, that it is close to a valid encoding of some distribution in the first place. The encoding that accomplishes both, which we term “Reed–μ ,” is presented in Section 7 as a self-contained “library”; for this overview, we summarize its two capabilities: • VerEnc: an interactive protocol verifying that an alleged codeword is close to a valid one. Validity is defined so that every valid codeword encodes a genuine distribution, with nonnegative weights summing to one (Definition 21); passing the test thus certifies at once proximity to the code and that the encoded object is a distribution. • VerMarginal: an interactive protocol verifying any marginal of the underlying distribution, namely, the mass it places on a partial assignment to the variables.33 3 The protocol proper calls the field-valued variant VerMarginoid, whose costs this overview quotes; the distinction is deferred to Section 7. ‖Q‖1I2(μ)≤τ2‖Q‖1\|Q\|_1 ^2(μ)≤τ^2\|Q\|_1the statement‖Q‖1\|Q\|_1I2(μ) ^2(μ)Q^(q^′) Q( q )Q^(q^) Q( q)⋅(CLOSE· (μ[(s^=b^)∩t^=1]μ[( s= b)∩ t=1]−-μ[s^=b^]μ[ s= b]P^(q^) P( q)OPEN)2 )^\!2 QQPPconfidence circuitproof oracle π circuit SumCheck SumCheckdirect eval.direct eval. VerMarginal VerMarginaldirect eval. VerEnc Figure 2: The protocol as a chain of reductions: an arrow E→E′E→ E means that verifying E reduces to verifying E′E , interacting with the Prover via the sub-protocol labeling the arrow. The root is the statement the Verifier sets out to check; rounded boxes are intermediate expressions that get reduced further; and the bottom row holds the only objects accessed directly: the input circuits P,QP,Q (gray), which the Verifier evaluates itself, and the proof oracle π (blue), written by the untrusted Prover and read at a few locations. The sub-protocols labeling the arrows ( SumCheck, VerEnc, VerMarginal) are interactive, carried out with the Prover’s help; “evaluate” the Verifier does alone. Hats mark field-valued objects. Conceptually, the protocol has three parts: it checks that π is close to a valid encoding of some distribution ( VerEnc); it obtains the marginals of that distribution to which the model’s claims refer ( VerMarginal); and it verifies, by SumCheck, that the model’s aggregate inconsistency against those marginals stays below the threshold. Figure 2 depicts how the parts fit together. Reading it top-down, we proceed with a strawman that gets progressively closer to the full protocol. Reducing the threshold ‖Q‖1\|Q\|_1. The Verifier compares I2(μ) ^2(μ) against the threshold τ2τ^2, and the former requires dividing by ‖Q‖1=∑qQ(q)\|Q\|_1= _qQ(q). Note that this is a sum over the set of all possible queries Q, which is of exponential size in the model’s input length. The first SumCheck reduces ‖Q‖1\|Q\|_1 to an evaluation at a random point q^′∈log|| q |Q|, where F is a large finite field over which all of the protocol’s arithmetic runs. Here and throughout, hats mark objects over F: Q Q is the polynomial extending Q to F (30), and the random point q^′ q is a vector of field elements, so it has the “shape” of a query but need not describe an actual one: ‖Q‖1 =∑q∈Q(q)↦ Q^(q^′) . to30.24pt to13.4pt 15.11801pt -6.7pt to0.0pt @begingroup@_scopebegin @begingroup@stroke @begingroup@fill @setlinewidth @begingroup@stroke-width @inpgf@ignorespaces to0.0pt @begingroup@_scopebegin @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @inpgf@ignorespaces @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @stroke @drawpath@unclippedM 17.87 8.99 L -17.87 8.99 C -19.4 8.99 -20.64 7.76 -20.64 6.23 L -20.64 -6.23 C -20.64 -7.76 -19.4 -8.99 -17.87 -8.99 L 17.87 -8.99 C 19.4 -8.99 20.64 -7.76 20.64 -6.23 L 20.64 6.23 C 20.64 7.76 19.4 8.99 17.87 8.99 Z M -20.64 -8.99fill:none @inpgf@ignorespaces @closescope @inpgf@ignorespaces @begingroup@_scopebegin @transformcm1.00.00.01.0-13.41801pt-2.5pt @begingroup@transform @hbox58 @closescope @closescope @closescope @inpgf@ignorespaces @inpgf@ignorespaces @discardpath @closescope @closescope = _q Q(q)\; SumCheck\; to25.09pt to13.42pt 12.54724pt -6.70891pt to0.0pt @begingroup@_scopebegin @begingroup@stroke @begingroup@fill @setlinewidth @begingroup@stroke-width @inpgf@ignorespaces to0.0pt @begingroup@_scopebegin @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @inpgf@ignorespaces @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @stroke @drawpath@unclippedM 14.32 9.01 L -14.32 9.01 C -15.85 9.01 -17.08 7.77 -17.08 6.24 L -17.08 -6.24 C -17.08 -7.77 -15.85 -9.01 -14.32 -9.01 L 14.32 -9.01 C 15.85 -9.01 17.08 -7.77 17.08 -6.24 L 17.08 6.24 C 17.08 7.77 15.85 9.01 14.32 9.01 Z M -17.08 -9.01fill:none @inpgf@ignorespaces @closescope @inpgf@ignorespaces @begingroup@_scopebegin @transformcm1.00.00.01.0-10.84724pt-2.50891pt @begingroup@transform @hbox58 @closescope @closescope @closescope @inpgf@ignorespaces @inpgf@ignorespaces @discardpath @closescope @closescope . Verifying the inconsistency I2 ^2. The root of the figure is the squared inconsistency I2(μ) ^2(μ), a sum over the query universe Q of an expression depending on the model (P,Q)(P,Q) and the marginals of the distribution μ. Verifying such a sum is precisely what the SumCheck protocol is designed for LFKN 92, so one SumCheck randomly-reduces it to a single uniformly random point q^∈log|| q |Q|: I2(μ) =∑q∈Q(q)(μ[(s=b)∩(t=1)]−μ[s=b]P(q))2 to34.41pt to14.04pt 17.2058pt -7.02pt to0.0pt @begingroup@_scopebegin @begingroup@stroke @begingroup@fill @setlinewidth @begingroup@stroke-width @inpgf@ignorespaces to0.0pt @begingroup@_scopebegin @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @inpgf@ignorespaces @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @stroke @drawpath@unclippedM 20.76 9.44 L -20.76 9.44 C -22.29 9.44 -23.53 8.2 -23.53 6.67 L -23.53 -6.67 C -23.53 -8.2 -22.29 -9.44 -20.76 -9.44 L 20.76 -9.44 C 22.29 -9.44 23.53 -8.2 23.53 -6.67 L 23.53 6.67 C 23.53 8.2 22.29 9.44 20.76 9.44 Z M -23.53 -9.44fill:none @inpgf@ignorespaces @closescope @inpgf@ignorespaces @begingroup@_scopebegin @transformcm1.00.00.01.0-15.5058pt-2.82pt @begingroup@transform @hbox58 @closescope @closescope @closescope @inpgf@ignorespaces @inpgf@ignorespaces @discardpath @closescope @closescope = _q Q(q) (μ[(s=b)∩(t=1)]-μ[s=b]P(q) )^2 ↓ SumCheck Q^(q^) ( μ[(s^=b^)∩t^=1] − μ[s^=b^] P^(q^) )2. to22.29pt to13.4pt 11.14447pt -6.7pt to0.0pt @begingroup@_scopebegin @begingroup@stroke @begingroup@fill @setlinewidth @begingroup@stroke-width @inpgf@ignorespaces to0.0pt @begingroup@_scopebegin @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @inpgf@ignorespaces @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @stroke @drawpath@unclippedM 12.38 8.99 L -12.38 8.99 C -13.9 8.99 -15.14 7.76 -15.14 6.23 L -15.14 -6.23 C -15.14 -7.76 -13.9 -8.99 -12.38 -8.99 L 12.38 -8.99 C 13.9 -8.99 15.14 -7.76 15.14 -6.23 L 15.14 6.23 C 15.14 7.76 13.9 8.99 12.38 8.99 Z M -15.14 -8.99fill:none @inpgf@ignorespaces @closescope @inpgf@ignorespaces @begingroup@_scopebegin @transformcm1.00.00.01.0-9.44447pt-2.5pt @begingroup@transform @hbox58 @closescope @closescope @closescope @inpgf@ignorespaces @inpgf@ignorespaces @discardpath @closescope @closescope ( to68.87pt to13.4pt 34.43501pt -6.7pt to0.0pt @begingroup@_scopebegin @begingroup@stroke @begingroup@fill @setlinewidth @begingroup@stroke-width @inpgf@ignorespaces to0.0pt @begingroup@_scopebegin @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @inpgf@ignorespaces @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @stroke @drawpath@unclippedM 44.6 8.99 L -44.6 8.99 C -46.13 8.99 -47.37 7.76 -47.37 6.23 L -47.37 -6.23 C -47.37 -7.76 -46.13 -8.99 -44.6 -8.99 L 44.6 -8.99 C 46.13 -8.99 47.37 -7.76 47.37 -6.23 L 47.37 6.23 C 47.37 7.76 46.13 8.99 44.6 8.99 Z M -47.37 -8.99fill:none @inpgf@ignorespaces @closescope @inpgf@ignorespaces @begingroup@_scopebegin @transformcm1.00.00.01.0-32.73502pt-2.5pt @begingroup@transform @hbox58 @closescope @closescope @closescope @inpgf@ignorespaces @inpgf@ignorespaces @discardpath @closescope @closescope - to33.87pt to13.4pt 16.935pt -6.7pt to0.0pt @begingroup@_scopebegin @begingroup@stroke @begingroup@fill @setlinewidth @begingroup@stroke-width @inpgf@ignorespaces to0.0pt @begingroup@_scopebegin @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @inpgf@ignorespaces @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @stroke @drawpath@unclippedM 20.39 8.99 L -20.39 8.99 C -21.92 8.99 -23.16 7.76 -23.16 6.23 L -23.16 -6.23 C -23.16 -7.76 -21.92 -8.99 -20.39 -8.99 L 20.39 -8.99 C 21.92 -8.99 23.16 -7.76 23.16 -6.23 L 23.16 6.23 C 23.16 7.76 21.92 8.99 20.39 8.99 Z M -23.16 -8.99fill:none @inpgf@ignorespaces @closescope @inpgf@ignorespaces @begingroup@_scopebegin @transformcm1.00.00.01.0-15.235pt-2.5pt @begingroup@transform @hbox58 @closescope @closescope @closescope @inpgf@ignorespaces @inpgf@ignorespaces @discardpath @closescope @closescope to22.29pt to13.4pt 11.14447pt -6.7pt to0.0pt @begingroup@_scopebegin @begingroup@stroke @begingroup@fill @setlinewidth @begingroup@stroke-width @inpgf@ignorespaces to0.0pt @begingroup@_scopebegin @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @inpgf@ignorespaces @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @stroke @drawpath@unclippedM 12.38 8.99 L -12.38 8.99 C -13.9 8.99 -15.14 7.76 -15.14 6.23 L -15.14 -6.23 C -15.14 -7.76 -13.9 -8.99 -12.38 -8.99 L 12.38 -8.99 C 13.9 -8.99 15.14 -7.76 15.14 -6.23 L 15.14 6.23 C 15.14 7.76 13.9 8.99 12.38 8.99 Z M -15.14 -8.99fill:none @inpgf@ignorespaces @closescope @inpgf@ignorespaces @begingroup@_scopebegin @transformcm1.00.00.01.0-9.44447pt-2.5pt @begingroup@transform @hbox58 @closescope @closescope @closescope @inpgf@ignorespaces @inpgf@ignorespaces @discardpath @closescope @closescope )^2. Here s^,b^,t s, b, t denote the blocks of the point q q that, in a Boolean query q=(s1,b1,…,sℓ,bℓ,t)q=(s_1,b_1,…,s_ ,b_ ,t), would hold the context variable descriptions, the context bits, and the target. Four quantities are left at q q: the marginals μ[s^=b^],μ[(s^=b^)∩(t^=1)]μ[ s= b],μ[( s= b)∩( t=1)] and the model values P^(q^),Q^(q^) P( q), Q( q). We account for each in turn. The marginals μ[s^=b^],μ[(s^=b^)∩(t^=1)]μ[ s= b],μ[( s= b)∩( t=1)]. The first is the mass the encoded distribution places on the context read off q q, and the second extends that context by requiring the target be true; that is, each is a marginal of μ. The marginal check VerMarginal (the second capability of the encoding) verifies each, reducing it to O(ℓ)O( ) point queries on the proof oracle: μ[s^=b^] , μ[(s^=b^)∩(t^=1)] ↦O(ℓ) point queries to π . to33.87pt to13.4pt 16.935pt -6.7pt to0.0pt @begingroup@_scopebegin @begingroup@stroke @begingroup@fill @setlinewidth @begingroup@stroke-width @inpgf@ignorespaces to0.0pt @begingroup@_scopebegin @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @inpgf@ignorespaces @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @stroke @drawpath@unclippedM 20.39 8.99 L -20.39 8.99 C -21.92 8.99 -23.16 7.76 -23.16 6.23 L -23.16 -6.23 C -23.16 -7.76 -21.92 -8.99 -20.39 -8.99 L 20.39 -8.99 C 21.92 -8.99 23.16 -7.76 23.16 -6.23 L 23.16 6.23 C 23.16 7.76 21.92 8.99 20.39 8.99 Z M -23.16 -8.99fill:none @inpgf@ignorespaces @closescope @inpgf@ignorespaces @begingroup@_scopebegin @transformcm1.00.00.01.0-15.235pt-2.5pt @begingroup@transform @hbox58 @closescope @closescope @closescope @inpgf@ignorespaces @inpgf@ignorespaces @discardpath @closescope @closescope ,\ to78.87pt to13.4pt 39.435pt -6.7pt to0.0pt @begingroup@_scopebegin @begingroup@stroke @begingroup@fill @setlinewidth @begingroup@stroke-width @inpgf@ignorespaces to0.0pt @begingroup@_scopebegin @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @inpgf@ignorespaces @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @stroke @drawpath@unclippedM 51.52 8.99 L -51.52 8.99 C -53.05 8.99 -54.29 7.76 -54.29 6.23 L -54.29 -6.23 C -54.29 -7.76 -53.05 -8.99 -51.52 -8.99 L 51.52 -8.99 C 53.05 -8.99 54.29 -7.76 54.29 -6.23 L 54.29 6.23 C 54.29 7.76 53.05 8.99 51.52 8.99 Z M -54.29 -8.99fill:none @inpgf@ignorespaces @closescope @inpgf@ignorespaces @begingroup@_scopebegin @transformcm1.00.00.01.0-37.735pt-2.5pt @begingroup@transform @hbox58 @closescope @closescope @closescope @inpgf@ignorespaces @inpgf@ignorespaces @discardpath @closescope @closescope \; VerMarginal\;$O( )$ point queries to to9.79pt to9.79pt -4.89555pt to0.0pt @begingroup@_scopebegin @begingroup@stroke @begingroup@fill @setlinewidth @begingroup@stroke-width @inpgf@ignorespaces to0.0pt @begingroup@_scopebegin @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @begingroup@fill @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @begingroup@fill @fillstroke @drawpath@unclippedM 6.5 0 C 6.5 3.59 3.59 6.5 0 6.5 C -3.59 6.5 -6.5 3.59 -6.5 0 C -6.5 -3.59 -3.59 -6.5 0 -6.5 C 3.59 -6.5 6.5 -3.59 6.5 0 Z M 0 0 @inpgf@ignorespaces @closescope @inpgf@ignorespaces @begingroup@_scopebegin @transformcm1.00.00.01.0-2.85013pt-2.15277pt @begingroup@transform @hbox58 @closescope @closescope @closescope @inpgf@ignorespaces @inpgf@ignorespaces @discardpath @closescope @closescope . The model values P^(q^),Q^(q^),Q^(q^′) P( q), Q( q), Q( q ). These are the input circuits P,QP,Q, viewed as the polynomials they compute (30), at the SumChecks’ random points. The Verifier evaluates each itself, by running the circuit over F at a single point—no interaction with the Prover: P^(q^) , Q^(q^) , Q^(q^′) ↦30evaluations of the circuits P , Q . to22.29pt to13.4pt 11.14447pt -6.7pt to0.0pt @begingroup@_scopebegin @begingroup@stroke @begingroup@fill @setlinewidth @begingroup@stroke-width @inpgf@ignorespaces to0.0pt @begingroup@_scopebegin @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @inpgf@ignorespaces @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @stroke @drawpath@unclippedM 12.38 8.99 L -12.38 8.99 C -13.9 8.99 -15.14 7.76 -15.14 6.23 L -15.14 -6.23 C -15.14 -7.76 -13.9 -8.99 -12.38 -8.99 L 12.38 -8.99 C 13.9 -8.99 15.14 -7.76 15.14 -6.23 L 15.14 6.23 C 15.14 7.76 13.9 8.99 12.38 8.99 Z M -15.14 -8.99fill:none @inpgf@ignorespaces @closescope @inpgf@ignorespaces @begingroup@_scopebegin @transformcm1.00.00.01.0-9.44447pt-2.5pt @begingroup@transform @hbox58 @closescope @closescope @closescope @inpgf@ignorespaces @inpgf@ignorespaces @discardpath @closescope @closescope ,\ to22.29pt to13.4pt 11.14447pt -6.7pt to0.0pt @begingroup@_scopebegin @begingroup@stroke @begingroup@fill @setlinewidth @begingroup@stroke-width @inpgf@ignorespaces to0.0pt @begingroup@_scopebegin @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @inpgf@ignorespaces @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @stroke @drawpath@unclippedM 12.38 8.99 L -12.38 8.99 C -13.9 8.99 -15.14 7.76 -15.14 6.23 L -15.14 -6.23 C -15.14 -7.76 -13.9 -8.99 -12.38 -8.99 L 12.38 -8.99 C 13.9 -8.99 15.14 -7.76 15.14 -6.23 L 15.14 6.23 C 15.14 7.76 13.9 8.99 12.38 8.99 Z M -15.14 -8.99fill:none @inpgf@ignorespaces @closescope @inpgf@ignorespaces @begingroup@_scopebegin @transformcm1.00.00.01.0-9.44447pt-2.5pt @begingroup@transform @hbox58 @closescope @closescope @closescope @inpgf@ignorespaces @inpgf@ignorespaces @discardpath @closescope @closescope ,\ to25.09pt to13.42pt 12.54724pt -6.70891pt to0.0pt @begingroup@_scopebegin @begingroup@stroke @begingroup@fill @setlinewidth @begingroup@stroke-width @inpgf@ignorespaces to0.0pt @begingroup@_scopebegin @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @inpgf@ignorespaces @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @stroke @drawpath@unclippedM 14.32 9.01 L -14.32 9.01 C -15.85 9.01 -17.08 7.77 -17.08 6.24 L -17.08 -6.24 C -17.08 -7.77 -15.85 -9.01 -14.32 -9.01 L 14.32 -9.01 C 15.85 -9.01 17.08 -7.77 17.08 -6.24 L 17.08 6.24 C 17.08 7.77 15.85 9.01 14.32 9.01 Z M -17.08 -9.01fill:none @inpgf@ignorespaces @closescope @inpgf@ignorespaces @begingroup@_scopebegin @transformcm1.00.00.01.0-10.84724pt-2.50891pt @begingroup@transform @hbox58 @closescope @closescope @closescope @inpgf@ignorespaces @inpgf@ignorespaces @discardpath @closescope @closescope \; @crefcreftypecap @tilde refnumfact:arith\;evaluations of the circuits to13.01pt to13.01pt 6.50542pt -6.50542pt to0.0pt @begingroup@_scopebegin @begingroup@stroke @begingroup@fill @setlinewidth @begingroup@stroke-width @inpgf@ignorespaces to0.0pt @begingroup@_scopebegin @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @begingroup@fill @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @begingroup@fill @fillstroke @drawpath@unclippedM 8.72 0 C 8.72 4.82 4.82 8.72 0 8.72 C -4.82 8.72 -8.72 4.82 -8.72 0 C -8.72 -4.82 -4.82 -8.72 0 -8.72 C 4.82 -8.72 8.72 -4.82 8.72 0 Z M 0 0 @inpgf@ignorespaces @closescope @inpgf@ignorespaces @begingroup@_scopebegin @transformcm1.00.00.01.0-3.90451pt-3.41666pt @begingroup@transform @hbox58 @closescope @closescope @closescope @inpgf@ignorespaces @inpgf@ignorespaces @discardpath @closescope @closescope , to14.46pt to14.46pt 7.22807pt -7.22807pt to0.0pt @begingroup@_scopebegin @begingroup@stroke @begingroup@fill @setlinewidth @begingroup@stroke-width @inpgf@ignorespaces to0.0pt @begingroup@_scopebegin @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @begingroup@fill @inpgf@ignorespaces @inpgf@ignorespaces @begingroup@_scopebegin @begingroup@stroke @begingroup@fill @fillstroke @drawpath@unclippedM 9.72 0 C 9.72 5.37 5.37 9.72 0 9.72 C -5.37 9.72 -9.72 5.37 -9.72 0 C -9.72 -5.37 -5.37 -9.72 0 -9.72 C 5.37 -9.72 9.72 -5.37 9.72 0 Z M 0 0 @inpgf@ignorespaces @closescope @inpgf@ignorespaces @begingroup@_scopebegin @transformcm1.00.00.01.0-3.95277pt-2.44444pt @begingroup@transform @hbox58 @closescope @closescope @closescope @inpgf@ignorespaces @inpgf@ignorespaces @discardpath @closescope @closescope . Validity of the encoding. Every reduction above reads the proof oracle π as a genuine μ R -encoding of a witnessing distribution, but a cheating Prover could instead supply an arbitrary string. The encoding check ( VerEnc), run once at the outset, certifies that π is close to a genuine codeword. It is the first capability of the encoding, and the one global check in the protocol: it reduces to nothing further. All together, the protocol runs the encoding check once; two SumChecks for I2 ^2 and ‖Q‖1\|Q\|_1; two marginal checks for the marginals at q q; and three direct circuit evaluations for P^(q^),Q^(q^),Q^(q^′) P( q), Q( q), Q( q ) (30).44 4 We think of these as two evaluations of the model, one at q q and the other at q^′ q . Each sub-protocol runs with its own fresh randomness, and the oracle π is read only through VerEnc and VerMarginal. The honest proof oracle is constructed in Section 8.1, and the full protocol is given as Algorithm 6 and analyzed in Section 8.2; Section 8.3 then improves the efficiency of the direct evaluations by delegating them to the Prover. This gives an explicit route by which a model could, in principle, prove its own probabilistic consistency; Remark 1 elaborates. Remark 1 (Learning the Prover?). An IPCP can be viewed as a stateless prover (the proof oracle, whose answers depend only on the query location) and a stateful prover (the interactive Prover). These roles can be realized by a single model in a scenario where a user (Verifier) attempts to ascertain the probabilistic consistency of a (large language) model with which it is interacting. Namely, when training the model to act as a Prover AGPR 25, a single Self-Proving model PθP_θ can play both roles through its state or “context”: the Verifier implements the proof oracle by resetting PθP_θ’s context before each query (cf. backtracking BLM+ 25; RSS+ 25), so that an answer cannot depend on the queries that preceded it, and implements the interactive Prover by letting the context persist across rounds. And of course, a proof oracle is equivalent to non-communicating provers FRS 94, which is how an IPCP KR 08 formally is a type of multi-prover interactive proof system BFLS 91. 3 Related work Verifying distribution properties. Verifying (or testing) consistency of predictive models can be viewed as an inverse problem to that of verifying properties of distributions. This is because in the latter settings, the Verifier is given access to samples from a distribution and is tasked with certifying whether a global property of this distribution holds. In the case that the property can be cast as a (possibly huge) set of probabilistic claims (constraints on the distribution’s marginals), this setting can be viewed as inverse to ours: in that setting access is given to the distribution and the task is to determine whether a set of claims hold, whereas in ours access is given to the claims (or a predictive model) and the task is to determine whether there exists a distribution consistent with them. In more detail, Interactive Proofs (IPs, GMR 89) have been adapted to verify properties of distributions CG 18, and this setting has since been studied extensively, showing that a rich family of properties can be verified, including, e.g., label-invariant properties HR 22; HR 23; Her 24; HR25a; HR25b; GHR 25. In the context of machine learning GRSY 21 introduced the IP-PAC systems, in which the Verifier certifies the accuracy of a given learned model with respect to a distribution (see also MS 23; GJK+ 24). Without the aid of a prover, GR 00; BFR+ 00 studied property testing RS 96; GGR 98 for distribution properties, wherein a Tester is given access to samples and determines a property of the distribution from which they were drawn (see survey Can 22). Of this rich line of work, particularly relevant is when the tester can draw samples from marginals of the distribution in what is known as subcube-conditioned sampling CRS 15; BC 18; CCK+ 21; CM 24; CCR+ 25: in the Boolean setting, a context x∈0,1,∗nx∈\0,1,*\^n specifies a subcube, and the claim “Pr[y=1∣x]=p [y=1 x]=p” is the (alleged) expectation of the yyth coordinate conditioned on this subcube. Probabilistic Consistency. The pursuit of probabilistic consistency has been salient since the development of probability itself Key 21; Ram 31. Boo 54 posed it as the search for the “conditions of possible experience”, and Dutch book arguments, beginning with the coherence theorem of de Finetti dF 37, contend that a bettor who fails to be probabilistically consistent can be easily exploited. The standard axioms of probability, due to Kolmogorov Kol 50, are intended to ensure that a probability measure—which without constraints would be simply a function that assigns numbers in [0,1][0,1] to events in a σ-algebra—behaves as one would expect. The complexity of probabilistic satisfiability has been studied in several settings Nil 86; GKP 88; FHM 90; Luk 01; KM 94. The question of whether m explicit unconditional probability claims can be jointly satisfied (PSAT) was posed by Nil 86, who recast it as a linear program; GKP 88 proved it NP-complete, with hardness already at two literals per clause. Via classical theory of linear programming, GKP 88 argue that the problem is in NP by appeal to the fact that a linear program with m constraints, corresponding to unconditional claims, has a solution supported on at most m+1m+1 points. They also show that the problem remains hard even for clauses of at most two literals. FHM 90 study a variant with inequalities, and bound the binary representation of the witnesses, placing the consistency problem for rational weights in NP under the standard model of computation (their Sec. 2.4). GKP 88; FHM 90 both remark in passing that the construction can be extended to handle explicit conditional claims of the form Pr[y∣x]=p [y x]=p that we use (essentially our - Explicit-Consistency problem restricted to the case of τ=0τ=0). Our proof of Proposition 9 is related to this classical approach, except that we operate in an inconsistency-tolerant setting (τ≥0τ≥ 0) whose objective is not merely a constraint residual of a linear program, and at a precision that requires us to be more careful about certificate length and introduce a gapped analogue. Tolerance of inconsistency (τ>0τ>0) has received less attention, at least until recently. Kilian and Naor KN 95 call a set of statistics ε -inconsistent if every distribution violates one of them by at least ε , and prove that distinguishing consistent from ε -inconsistent statistics is NP-hard for a constant ε ; however, they do not upper bound its complexity. Pot 14 proposes a family of ℓp _p-based inconsistency measures, including our I for p=2p=2, but only places its complexity in EXP. This kind of inconsistency minimization is useful for database consolidation PT 14. These ℓp _p measures are surveyed in DFPT 18, where they are connected to the degree of vulnerability to Dutch books; the entropy-based divergences of RH 21 are a separate line. RHS 23 show that approximating a notion of inconsistency closely related to ours is #P-hard. In machine learning, probabilistic consistency appears not as a property to be decided but as one to be trained for XN 18; ZPIE 17; JLKK 19; KJPJ 20; RSS+ 26. Systems are trained to ensure consistency between different representations, in both generative ZPIE 17 and semi-supervised settings KJPJ 20. Ensuring consistency between forward and backward probabilistic trajectories is a key idea behind Generative Flow Networks BLD+ 23. This has led to the Scientist AI project, which aims to generalize the techniques used to train GFlowNets for consistency to systems of exponentially more variables BCF+ 25; FRG+ 26—which is precisely the primary problem we tackle in this paper. It has been argued that all of these results fit together as part of a bigger theory of machine learning as probabilistic modeling that is tolerant to inconsistency Ric 24; Ric 22. The Integer Carathéodory theorem. Previous work studied “Integer Carathéodory theorems” CFS 86; Seb 90; ES 06, in which any integer point in the conic hull of a Hilbert basis (or a finite set of integer vectors) is representable as an integer conic combination supported on linearly many basis vectors. Our bounds (Section 5) can be viewed as complementary in that they give a sparsity bound for rational convex combinations of Boolean vectors, with explicit control on the bit-length of the coefficients. To the best of our understanding, our results fundamentally cannot be derived from the existing literature because, essentially, clearing denominators to reduce our setting to theirs would blow up coefficient magnitudes exponentially in the input precision, which would defeat our goal of a polynomial-length certificate. Also related is literature on “approximate Carathéodory theorems” Bar 15; MLVW 17, however these results bound the ℓp _p-approximation error of a sparse convex combination at a fixed support size, rather than the bit-complexity of an (almost-)exact stochastic representation. Interactive Proofs and AI. IPs have been demonstrated to hold theoretical and empirical promise as a way of establishing trust in learned models (“AI Safety”). ICA 18 proposes using Debate Systems (with two competing provers, cf. CFLS 93; FK 97), later extended to the double-efficient setting in BIP 24 and studied further in BIP 25; BIM+ 26. AZWG 21 introduced Prover–Verifier Games, in which a non-interactive ( NP-)Verifier is learned jointly with a Proof-generating model. This setting was used in large-scale experiments by OpenAI in KCE+ 24, and generalized to that of Interactive Proofs (including MIPs and Zero Knowledge proof systems) in HA 25. Relatedly, WST+ 24 studied a variant (MA-Classifiers) towards obtaining more interpretable model outputs. AGPR 25 introduced Self-Proving models, which are trained to act as Provers in a prescribed IP, that is, generate proofs that convince a given Verifier. This approach, which formalizes earlier empirical work (e.g., PS 20), can be viewed as complementary to our main result: We show how a proof oracle and a prover can convince a verifier of the consistency of a model; future work can explore whether both roles can be learned as Self-Proving models themselves. The two roles differ only in statefulness—the proof oracle is a stateless prover, the interactive prover a stateful one—so a single “generalist” model can play both: its “memory” is reset before each oracle query and persists across the interactive rounds (cf. Remark 1 and recent empirical works POC+ 23; DLT+ 24). Sum-of-squares and pseudodistributions. The Sum-of-Squares (SoS) hierarchy of Nes 00; Las 01; Par 03, and the pseudo-distribution viewpoint BBH+ 12; BS 14 share a conceptual resemblance to our setting, in that their goal is to certify that a system of constraints admits a (perhaps approximate) probability-distribution solution. There are significant technical differences, however: A degree-d pseudo-distribution is a linear functional on degree-d polynomials with no guarantee of extending to a genuine distribution, and the relevant parameter is the polynomial degree d with a semidefinite program of size exponential in d; more importantly, the SoS hierarchy prescribes algorithms for deciding approximate consistency, whereas we offer algorithms for verifying a (different notion of) approximate consistency. Namely, our setting instead measures inconsistency by ℓ2 _2 distance from a genuine distribution, parameterizes by a tolerance τ (and an additive gap ε ), and our verification methods utilize an auxiliary proof or interactive proof system. 4 Conventions and definitions For a natural number m≥1m≥ 1, we use [m]:=1,…,m[m]:=\1,…,m\ for the set of positive integers at most m. All logarithms are base 22. We write (⋅) poly(·) for an unspecified polynomial in its arguments, and O~(⋅) O(·) suppresses factors polylogarithmic in the argument. For a finite set X, we write ΔX X for the set of all distributions ν over the elements of X, and use the same symbol (ν, in this case) for both: (a) the simplex point (or probability mass function) ν:X→[0,1]ν:X→[0,1] satisfying ∑x∈Xν(x)=1 _x∈ Xν(x)=1, which uniquely corresponds to (b) the probability measure ν:2X→[0,1]ν:2^X→[0,1], assigning a probability to events E⊆XE X satisfying the Kolmogorov Axioms of probability (i.e., ν(X)=1ν(X)=1, and ν(A∪B)=ν(A)+ν(B)ν(A∪ B)=ν(A)+ν(B) for all disjoint A,B⊆XA,B X) agreeing with the pmf form (a) on singletons and is extended by ν(E)=∑x∈Eν(x)ν(E)= _x∈ Eν(x). In particular, the set of joint distributions on the n-dimensional hypercube is denoted Δ0,1n=Δ2n \0,1\^n= 2^n. Here and throughout, 2n2^n for a number n denotes the hypercube 0,1n\0,1\^n, whereas 2X2^X for a set X denotes its power set, as in (b) above. Variables and partial assignments. Throughout this paper, n∈ℕn will be used to refer to a number of Boolean variables. A (joint) assignment to all variables is therefore a point ω∈0,1nω∈\0,1\^n on the n-dimensional hypercube. We are especially interested in the restricted set of events on the hypercube, namely those with that can be described through partial assignments to variables. A partial assignment is x∈0,1,∗nx∈\0,1, \^n, where xi=∗x_i= should be interpreted as having the iith variable be unassigned in x. Assignment ω∈0,1nω∈\0,1\^n agrees with x, written w⊧xw x, if, for all i∈[n]i∈[n], xi∈wi,∗x_i∈\w_i, \; that is, w and x agree on all non-∗ entries of x. Thus, we allow ourselves to implicitly regard the partial assignment x as the event ω∈2n:∀i∈[n].xi∈ωi,∗\ω∈ 2^n:∀ i∈[n].~x_i∈\ _i,*\\ when discussing its probability. We will often be interested in a target event of the form y=1y=1 for some variable index y∈[n]y∈[n], which we formally regard as the event ω∈2n:ωy=1\ω∈ 2^n: _y=1\. Machines and oracles. Our model of computation is the Turing machine, and the running times of the combinatorial algorithms of Section 5 are counted in machine steps, that is, bit operations. An oracle machine MfM^f is a machine M with query access to a function f: it may write down an input x and read back f(x)f(x), at unit cost per query. This is the access model behind every oracle in this paper, the proof oracle of the Interactive PCP (Definition 29) in particular. The superscript names the oracle: Z,A VerEnc_F^Z,A, for example, has query access to the pair of functions (Z,A)(Z,A). Circuits are Boolean unless stated otherwise, and the size |C||C| of a circuit C is its number of gates, inputs and outputs included. When a circuit is an explicit input to an algorithm, as the predictive model (P,Q)(P,Q) is to the Verifier of Section 8, the input length is Θ(|P|+|Q|) (|P|+|Q|); a polynomial-time Verifier may therefore run in time polynomial in |P|+|Q||P|+|Q|, which in particular dominates the circuits’ own input length ℓ(d+1)+d (d+1)+d and output precision B. Precision of rational numbers. Except where noted otherwise, all numbers in the paper are assumed to be rational. A non-trivial part of our techniques is devoted to controlling the errors introduced when doing arithmetic over rational numbers, and so we must explicitly deal with how these numbers are represented. Throughout this paper we will say that a rational number q∈[0,1]q∈[0,1] is specified to precision B∈ℕB to mean that q is represented by a numerator q†q as a B-bit string, so that q=q†/2Bq=q /2^B. For example, if we say that a Turing machine takes as input a rational number q∈[0,1]q∈[0,1] to precision B, then it takes the B-bit string q†q . The convention extends to collections: when several rationals q1,…,qkq_1,…,q_k are specified to a common precision B (as are, e.g., the claims of a CPC and the weights of our witnessing distributions), the machine takes just the numerators (q1†,…,qk†)(q _1,…,q _k), the shared denominator 2B2^B being given once. In any case, when analyzing running time or proof lengths, the description will be made explicit. Finite fields and polynomials. For a field F of odd characteristic we let 2−12^-1 denote the inverse of 1+11+1 in F. For an n-variate polynomial φ∈[X1,…,Xn] [X_1,…,X_n], the total degree of φ is the maximum, over its monomials, of the sum of the variables’ exponents, and its individual degree is the largest exponent with which any single variable appears in it. Working over a prime field, we identify the elements of F with the integers 0,…,||−1\0,…,|F|-1\. An (in)equality asserted over ℤZ compares these integer representatives as integers, rather than as field elements; unlike its over-F counterpart, such an assertion is sensitive to wraparound, and controlling it is what the field-size hypotheses of Section 8 are for. Running times in Sections 7 and 8 are counted in field operations (additions, multiplications, inversions, and samples of a uniformly random element of F), each of which costs (log||) poly( |F|) bit operations. Finally, we say that a random vector is marginally uniform on a set of coordinates if each of those coordinates, viewed on its own, is uniformly distributed; nothing is implied about their joint distribution. Pseudocode. We write x←ex← e for the assignment of the value e to x; inside a procedure call, f(p←e)f(p← e) runs f with the named parameter p set to e. We write a=?ba ?=b for an equality the Verifier asserts, rejecting if it fails. “Expect v from the Prover” receives a message from the (untrusted) Prover and names it v; nothing is assumed of v beyond its type. A sub-protocol invoked by the Verifier runs on the Verifier’s own fresh randomness, and “reject if it rejects” propagates its verdict. 4.1 Collections of Probabilistic Constraints (CPCs) and their inconsistency We now formally define our object of study: a collection of probabilistic claims (CPC). When specified explicitly, this is the key data of an - Explicit-Consistency instance; when specified succinctly, it is the data of a - Model-Consistency instance. Definition 2 (CPC specified to precision B). Let B,n∈ℕB,n . A probabilistic claim specified to precision B is a tuple (x,y,p)(x,y,p) where x∈0,1,∗nx∈\0,1,*\^n is the context, y∈[n]y∈[n] is the target, and p∈[0,1]∩12Bℤp∈[0,1]∩ 12^BZ can be represented as p†/2Bp /2^B for some integer p†∈0,…,2B−1p ∈\0,…,2^B-1\. A Collection of Probabilistic Constraints (CPC) specified to precision B∈ℕB is a multi-set 55 5 We will still use P∈P to denote membership in the multi-set, and use |||P| to denote its size (sum of multiplicities). P of probabilistic claims all specified to precision B. We will commonly use m=||m=|P| to refer to the number of claims, i.e., elements in the multi-set P. The length of P in bits is m(nlog2(3)+⌈log2n⌉+B)∈O(mn+mB)m(n _2(3)+ _2n +B)∈ O(mn+mB). Definition 3 (Approximate consistency and - Explicit-Consistency). Let P be a CPC of m claims over n variables, and let μ∈Δ0,1nμ∈ \0,1\^n. We define the (normalized, ℓ2 _2-)inconsistency of μ with P to be I(μ)≔1||∑(x,y,p)∈(μ(x∩y)−p⋅μ(x))2, _P(μ) 1|P| _(x,y,p) (μ(x∩ y)-p·μ(x) )^2, (2) and the inconsistency of the CPC instance P to be I()≔infμ∈Δ0,1nI(μ) (P) _μ∈ \0,1\^n _P(μ). For a given tolerance τ≥0τ≥ 0, we say that P is τ-consistent if I()≤τ (P)≤τ. We let - Explicit-Consistency denote the set of all pairs (,τ)(P,τ) such that P is τ-consistent. 4.2 Predictive models and their consistency In this paper, a (predictive) model is a computer program that takes as input a description of events x and y and outputs a number to be interpreted as the conditional probability of y given x. A common example is neural predictive models, which are neural network architectures instantiated with a set of weights, and claims described by a sequence of natural language sentences. It is useful to allow the model to output a confidence score in addition to its prediction. In particular, a zero confidence score allows the model to abstain from making a prediction all together, a capability whose utility is well-studied GKKM20a; GKKM20b; K21a; K21b; GHMS 23. Definition 4 (Predictive model). Fix a variable description length d∈ℕd , a context length ℓ∈ℕ , and a precision B∈ℕB , and write n≔2dn 2^d for the number of variables these parameters address, indexed by their d-bit descriptions: ωz _z for z∈0,1dz∈\0,1\^d. A predictive model is a pair of Boolean circuits (P,Q)(P,Q), where P is the probability circuit and Q is the confidence circuit, each taking a query as input and outputting B bits. A query is a string q=(s1,b1,…,sℓ,bℓ,t)∈,≔0,1ℓ(d+1)+d,q=(s_1,b_1,…,s_ ,b_ ,t) , \0,1\ (d+1)+d, where Q is the query universe. Its components are the variable descriptions s1,…,sℓ∈0,1ds_1,…,s_ ∈\0,1\^d of the context, the corresponding context bits b1,…,bℓ∈0,1b_1,…,b_ ∈\0,1\, and the target variable description t∈0,1dt∈\0,1\^d. On a query q, the probability circuit outputs P(q)∈0,…,2B−1P(q)∈\0,…,2^B-1\, interpreted as an (alleged) probability P(q)/2BP(q)/2^B, and the confidence circuit outputs an integer Q(q)∈0,…,2B−1Q(q)∈\0,…,2^B-1\. Fix a distribution μ over 0,1n\0,1\^n. For a context (s1,b1,…,sℓ,bℓ)(s_1,b_1,…,s_ ,b_ ) we abbreviate by s=bs=b the event that every context literal holds, that is, ωsk=bk _s_k=b_k for all k∈[ℓ]k∈[ ], and use square brackets μ[s=b]μ[s=b] for its probability under μ—note the square brackets: μ[s=b]≔μ(ω∈0,1n:ωsk=bk for all k∈[ℓ]).μ[s=b] μ ( \ω∈\0,1\^n: _s_k=b_k for all k∈[ ] \ ). Writing t=1t=1 for the target literal ωt=1 _t=1, we similarly write μ[(s=b)∩(t=1)]μ[(s=b)∩(t=1)] for the probability of the context event together with ωt=1 _t=1. Definition 5 (τ-consistent predictive models). Let (P,Q)(P,Q) be a model with variable description length d and context length ℓ , and let μ be a distribution over 0,1n\0,1\^n. Let ‖Q‖1=∑q∈Q(q)\|Q\|_1= _q Q(q) denote the total confidence the model places over all queries.66 6 We treat Q’s outputs as unsigned (nonnegative) integers, so ‖Q‖1=∑q|Q(q)|\|Q\|_1= _q|Q(q)| is the ℓ1 _1-norm of Q over its inputs. IP,Q(μ) _P,Q(μ) ≔1‖Q‖1∑q=(s1,b1,…,sℓ,bℓ,t)∈Q(q)(μ[(s=b)∩(t=1)]−P(q)2Bμ[s=b])2 1\|Q\|_1 _q=(s_1,b_1,…,s_ ,b_ ,t) Q(q) (μ[(s=b)∩(t=1)]- P(q)2^Bμ[s=b] )^2 I(P,Q) _(P,Q) ≔infμ∈Δ0,1nIP,Q(μ). _μ∈ \0,1\^n _P,Q(μ). For a tolerance τ, we say that (P,Q)(P,Q) is τ-consistent if I(P,Q)≤τ _(P,Q)≤τ, and define the set - Model-Consistency comprising all (P,Q,τ)(P,Q,τ) such that (P,Q)(P,Q) is τ-consistent. 4.3 Aside: Models as implicit CPCs The two inconsistency operators defined above deliberately share the symbol I : a predictive model is a succinct description of a collection of claims, and its inconsistency is the inconsistency of that collection. We formalize this next. Definition 6 (Implicit CPC). Let (P,Q)(P,Q) be a predictive model. Call a query q=(s1,b1,…,sℓ,bℓ,t)q=(s_1,b_1,…,s_ ,b_ ,t) conflicting if there are indices k≠k′∈[ℓ]k≠ k ∈[ ] with sk=sk′s_k=s_k yet bk≠bk′b_k≠ b_k . The implicit CPC P,QP_P,Q is the multiset of claims over n=2dn=2^d variables obtained as follows. For each q∈q : if q is non-conflicting, let xq∈0,1,∗nx_q∈\0,1, \^n be the partial assignment with (xq)sk=bk(x_q)_s_k=b_k for all k∈[ℓ]k∈[ ] and ∗ in all other entries, and add Q(q)Q(q) copies of the claim (xq,ωt,P(q)/2B) (x_q, _t,\ P(q)/2^B ); if q is conflicting, add Q(q)Q(q) copies of the tautological claim (xq,ωt,0) (x_q, _t,0 ), where xqx_q sets (xq)t=0(x_q)_t=0 and ∗ in all other entries. Claim 7. For every distribution μ over 0,1n\0,1\^n, IP,Q(μ)=I(P,Q)(μ) _P_P,Q(μ)= _(P,Q)(μ): the inconsistency of the implicit CPC, as a CPC, equals the inconsistency of the model, as a model. In particular, (P,Q)(P,Q) is τ-consistent if and only if P,QP_P,Q is. Proof. By construction, |P,Q|=∑qQ(q)=‖Q‖1|P_P,Q|= _qQ(q)=\|Q\|_1, and the claims group by the query that produced them: each q contributes Q(q)Q(q) copies of one claim. For a conflicting q the context event is empty, so μ[s=b]=μ[(s=b)∩(t=1)]=0μ[s=b]=μ[(s=b)∩(t=1)]=0 and q contributes 00 to the model sum; its tautological claim contributes μ(xq∩ωt)−0⋅μ(xq)=0μ(x_q∩ _t)-0·μ(x_q)=0 to the CPC sum, since (xq)t=0(x_q)_t=0. Both are weighted Q(q)Q(q), so |P,Q|=∑qQ(q)=‖Q‖1|P_P,Q|= _qQ(q)=\|Q\|_1 is unchanged and the two sums agree term by term. For any query q=(s1,b1,…,sℓ,bℓ,t)q=(s_1,b_1,…,s_ ,b_ ,t), the claim (xq,ωt,P(q)/2B)(x_q, _t,P(q)/2^B) has μ(xq)=μ[s=b]μ(x_q)=μ[s=b] and μ(xq∩ωt)=μ[(s=b)∩(t=1)]μ(x_q∩ _t)=μ[(s=b)∩(t=1)]. Therefore IP,Q(μ) _P_P,Q(μ) =1|P,Q|∑(x,t,p)∈P,Q(μ(x∩y)−p⋅μ(x))2 = 1|P_P,Q| _(x,t,p) _P,Q (μ(x∩ y)-p·μ(x) )^2 =1|P,Q|∑(xq,ωt,P(q)/2B)∈P,Q(q)(μ(xq∩ωt)−P(q)2B⋅μ(xq))2 = 1|P_P,Q| _(x_q, _t,P(q)/2^B) _P,QQ(q) (μ(x_q∩ _t)- P(q)2^B·μ(x_q) )^2 =1‖Q‖1∑q∈Q(q)(μ[(s=b)∩(t=1)]−P(q)2B⋅μ[s=b])2=I(P,Q)(μ).∎ = 1\|Q\|_1 _q Q(q) (μ[(s=b)∩(t=1)]- P(q)2^B·μ[s=b] )^2= _(P,Q)(μ). In light of 7, we use I for both operators without further comment. 5 Verifying consistency of probabilistic claims This section is concerned with establishing the following two results. Proposition 8. The Verifier V of Algorithm 1, which takes as input a collection of probabilistic claims P specified to precision B, a tolerance τ≥0τ≥ 0 and gap εgap>0 _ gap>0, has the properties of: • Efficiency: V runs in time O(m2(n+Blog(m/εgap)))O(m^2(n+B ( m _ gap))). • Soundness: if I(μ)>τ _P(μ)>τ for all μ∈Δ(0,1n)μ∈ (\0,1\^n), then V(,τ,π)=rejectV(P,τ,π)= reject for all certificates π. • Completeness (up to OPENεgap) _ gap): If I()≤τ−εgap (P)≤τ- _ gap, then there exists a proof certificate π such that V(,τ,π)=acceptV(P,τ,π)= accept. Moreover, π satisfies: • Near-linear length and logarithmic certificate precision: accepting proofs π consist of at most m+1m+1 pairs (z,α)(z,α) with z∈0,1nz∈\0,1\^n and α∈[0,1]α∈[0,1] specified in binary to precision Bεgap∈O(log(m/εgap))B_ _ gap∈ O( ( m _ gap))—thus satisfying length(π)∈O(m(n+log(m/εgap)))length(π)∈ O(m(n+ ( m _ gap))). Our main construct (Theorem 32) relies on Proposition 8. Crucially, the weights of the witnessing distribution are rounded so as to be specifiable in Bεgap∈O(log(m/εgap))B_ _ gap∈ O( ( m _ gap)) bits. As noted in Section 3, the complexity of verifying approximate consistency is of independent interest within its related literature, and so we then adapt Proposition 8 to obtain a gap-free variant: Proposition 9 (-∈ Explicit-Consistency∈ NP). There exists a Verifier that, when run on input ,τP,τ, satisfies: • Efficiency: The Verifier runs in O(m3(B+logm)2+m2n)O(m^3(B+ m)^2+m^2n) time. • Completeness: If I()≤τ (P)≤τ, there exists a proof certificate such that the Verifier accepts. • Soundness: if I()>τ (P)>τ, the Verifier rejects regardless of the given proof certificate. • Certificate length: proof certificates are of length O(mn+logB)O(mn+ B). To compare the two: In Proposition 8 the Prover sends the weights, rounded, and the Verifier only checks them; the rounding introduces the gap, but it buys weights whose precision scales logarithmically with m/εgapm/ _ gap. In Proposition 9 only the support vectors (and a prime number) are sent: the Verifier solves for the exact optimal weights, which removes the gap at the price of a precision polynomial in m and B, and a running time to match. The gap-free variant cannot be directly used for our main construct (Theorem 32), as elaborated in Remark 36. 5.1 The Verifier Consider a finite collection of probabilistic claims =(xi,yi,pi)i=1mP=\(x_i,y_i,p_i)\_i=1^m with each p∈ℚp representable as the integer p†≔p⋅2B∈0,…,2B−1p p· 2^B∈\0,…,2^B-1\. Define the constraint residuals, a vector ϕ:0,1n→ℤmφ:\0,1\^n ^m over the space of joint assignments to variables, according to: ϕ(ω)≔[(2Bωyi−pi†)[ω⊧xi]]i=1m, φ(ω) [(2^B _y_i-p_i ) 1[ω x_i] ]_i=1^m, whose components each have magnitude at most 2B2^B. The key feature of this representation is that I2(μ)=1m⋅22B‖ω∼μ[ϕ(ω)]‖22=1m∑i=1m(μ(xi,yi)−μ(xi)pi)2 for all μ∈Δ0,1n. ^2_P(μ)= 1m· 2^2B \| _ω μ[φ(ω)] \|_2^2= 1m _i=1^m(μ(x_i,y_i)-μ(x_i)p_i)^2 for all μ∈ \0,1\^n. (3) Carathéodory’s Theorem Car 07 states that any point in the convex hull of a set S⊂ℝdS ^d can be expressed as a convex combination of at most d+1d+1 points from S. We will use this to demonstrate that, if there exists a distribution μ∗μ^* with small constraint violation I(μ∗)≤τ _P(μ^*)≤τ, then there also exists one supported on only m+1m+1 points. That sparsely supported distribution (or rather, a discretization of it) will ultimately be the proof certificate. To be more precise, start with the observation that μ[ϕ]:μ∈Δ0,1n=convϕ(ω):ω∈0,1n\ _μ[φ]:μ∈ \0,1\^n\=conv\φ(ω):ω∈\0,1\^n\ is convex by definition of the expectation. Therefore, by Carathéodory’s Theorem, for every μ, the point μ[ϕ]∈ℝm _μ[φ] ^m can be expressed as a convex combination μ[ϕ]=∑j=1m+1αjϕ(zj) _μ[φ]= _j=1^m+1 _j\,φ(z_j) of some joint assignments z1,…,zm+1∈0,1nz_1,…,z_m+1∈\0,1\^n. This yields a (typically different) distribution μ′=μz,α∈Δ0,1nμ = _z,α∈ \0,1\^n with the same constraint residual as μ, but supported on only m+1m+1 points. Stated more formally: ∀μ∈Δ(0,1n).∃α=(αj)j=1m+1∈Δ[m+1],z∈(0,1n)m+1.μ[ϕ]=∑j=1m+1αjϕ(zj)=μz,α[ϕ], ∀μ∈ (\0,1\^n).~∃α=( _j)_j=1^m+1∈ [m+1],~z∈(\0,1\^n)^m+1. _μ[φ]= _j=1^m+1 _jφ(z_j)= _ _z,α[φ], where μz,α(ω)≔∑j=1m+1αj 1[zj=ω] has |supp(μz,α)|≤m+1. where _z,α(ω) _j=1^m+1 _j\, 1[z_j=ω]~~ has ~~ |\,supp( _z,α) |≤ m+1. We remark that such sparsification arguments have been used in the literature: the same fact appears as a statement about basic feasible solutions of a linear system in GKP 88, (KM 94, Theorem 2.3), and is what enables the small-model theorem in (FHM 90, Theorem 2.6), both in the service of placing exact (τ=0τ=0) consistency of unconditional claims in NP. The other key ingredient is a bound on the lengths of the rational coefficients of this witness, which FHM 90 repurposed from the non-negative integer linear programming literature Chv 83. The bound that we prove in Lemma 13 serves the same role for us, although we must do it directly, since our ℓ2 _2 inconsistency formulation cannot be cast as a linear program, and we also need to very precisely bound the bit complexity of the weights of an approximate witness (c.f., Remark 36). This leads us to Algorithm 1. Its certificate specifies the weights to precision BεgapB_ _ gap: per our convention, only the numerators αj†=2Bεgapαjα _j=2^B_ _ gap _j are sent. Input: Collection P of m probabilistic claims to precision B, tolerance τ, gap εgap>0 _ gap>0. Input: A proof certificate comprising: an integer k∈[m+1]k∈[m+1], assignments z1,…,zk∈0,1nz_1,…,z_k∈\0,1\^n, and weights α1†,…,αk†∈0,…,2Bεgapα _1,…,α _k∈\0,…,2^B_ _ gap\ for Bεgap:=⌈log2(2(m+1)3/(εgap2m))⌉B_ _ gap:= _2\! (2(m+1)^3/( _ gap^2m) ) . Check that the certificate is of the form declared above, and that ∑jαj†=2Bεgap _jα _j=2^B_ _ gap, else reject. 1 Calculate 2≔∑(x,y,p)∈(∑j=1kαj†(2Bzj,y−p†)[zj⊧x])2. ^2 _(x,y,p) ( _j=1^k _j \,(2^Bz_j,y-p ) 1[z_j x] )^2. 2 Output: accept if 2≤m⋅22B+2Bεgap⋅τ2inc^2≤ m· 2^2B+2B_ _ gap·τ^2; else reject Algorithm 1 Verification of Approximate Probabilistic Consistency Write Vz≔[ϕ(z1),ϕ(z2),⋯,ϕ(zk)]∈ℤm×kV_z [φ(z_1),\,φ(z_2),\,·s,\,φ(z_k) ] ^m× k for the residual matrix of the support, whose jjth column lists the constraint residuals of the single point zjz_j. It is what ties the algorithm’s arithmetic back to the inconsistency it is meant to measure: for any weights α∈Δ[k]α∈ [k] over the support, ‖Vzα‖22=‖∑j=1kαjϕ(zj)‖22=m⋅22B⋅I2(μz,α),\|V_zα\|_2^2= \| _j=1^k _j\,φ(z_j) \|_2^2=m· 2^2B· ^2_P( _z,α), (4) so that 2=22Bεgap‖Vzα‖22=m(2B+Bεgap)2I2(μz,α)inc^2=2^2B_ _ gap\|V_zα\|_2^2=m(2^B+B_ _ gap)^2 ^2_P( _z,α). Therefore, the final check of Algorithm 1 holds exactly when I(μz,α)≤τ _P( _z,α)≤τ, and the best weights for a given support are those minimizing ‖Vzα‖22\|V_zα\|_2^2 over the simplex. Runtime Analysis. Let’s take a closer look at the calculation on the last line. In the inner sum, we: 1. calculate whether or not zj⊧xz_j x, which involves comparing each of the n bits of x against the n bits of zjz_j, and hence takes n steps. 2. Subtract p†p , a non-negative integer at most 2B2^B, from either 2B2^B or zero, depending on the bit zyj∈0,1z_y^j∈\0,1\, which takes B steps, and produces a (B+1)(B+1)-bit number. 3. Multiply this number by αj† _j , an integer at most 2Bεgap2^B_ _ gap. This can be done in 1+BBεgap1+B_ _ gap steps (since the additional bit is a sign that can be copied in one step) and produces a (B+Bεgap)(B+B_ _ gap)-bit number. We repeat these three steps k≤m+1k≤ m+1 times, which takes at most (m+1)(1+n+B+BBεgap)∈O(m(n+BBεgap))(m+1)(1+n+B+B_ _ gap)∈ O(m(n+B_ _ gap)) steps, and results in an integer that can be represented in 1+B+Bεgap+log2(m+1)1+B+B_ _ gap+ _2(m+1) bits. Then we square it, resulting in a number that can be represented in 2(1+B+Bεgap+log2(m+1))2(1+B+B_ _ gap+ _2(m+1)) bits, and sum over all m probabilistic claims in P, for a total of m((m+1)(1+n+B+BBεgap)⏟inner loop+4(1+Bεgap+B+2log(m))2⏟accumulation)∈O(m2(n+BBεgap))steps.m (\, (m+1)(1+n+B+B_ _ gap)_inner loop\,+ 4(1+B_ _ gap+B+2 (m))^2 |_accumulation\, )∈ O(m^2(n+B_ _ gap))~~steps. Since Bεgap∈O(log(m/εgap))B_ _ gap∈ O( ( m _ gap)), this is O(m2(n+Blog(m/εgap)))O(m^2(n+B ( m _ gap))) steps. The modified Verifier of Section 5.3 runs the same accounting at a larger denominator, and pays for its solve on top. Soundness. The proof π=(z,α†)π=(z,α ) sent by the Prover exactly encodes a distribution μz,α _z,α, and by (4) the quantity computed on the last line satisfies 2=m(2B+Bεgap)2I2(μz,α)inc^2=m(2^B+B_ _ gap)^2 ^2_P( _z,α), so the final check holds if and only if I(μz,α)≤τ _P( _z,α)≤τ. Therefore, if the Verifier accepts, μz,α _z,α itself is a distribution with I(μz,α)≤τ _P( _z,α)≤τ. The procedure is thus perfectly sound: the gap will be paid only in completeness. 5.2 Logarithmic-precision weights, at the cost of a gap (Proposition 8) The honest Prover sends an approximate witness (z,α^)(z, α): a support z, and weights α α rounded to BεgapB_ _ gap bits, satisfying ‖α−α^‖∞≤δ\|α- α\|_∞≤δ for the exact optimum α on that support. Two lemmas make the rounding precise: the first bounds the error it incurs, and the second shows that weights of any prescribed precision exist within any rounding radius. 12 then puts them together, and Proposition 8 follows. Lemma 10. If α,α^∈Δ[m+1]α, α∈ [m+1] are such that ‖α−α^‖∞≤δ\|α- α\|_∞≤δ, i.e., ∀j∈[m+1].|αj−α^j|≤δ∀ j∈[m+1].~| _j- α_j|≤δ, then for all z=(zj)j=1m+1z=(z_j)_j=1^m+1, |I2(μz,α^)−I2(μz,α)|≤2δ(m+1)3/m | ^2_P( _z, α)- ^2_P( _z,α) |≤ 2δ(m+1)^3/m. Proof. First, we show that, since α,α^∈Δ[m+1]α, α∈ [m+1] are probabilities over [m+1][m+1] that are close in the sense that maxi|αi−α^i|≤δ _i| _i- α_i|≤δ, then |αiαj−α^iα^j|≤2δ−δ2| _i _j- α_i α_j|≤ 2δ-δ^2 for all i,j∈[m+1]i,j∈[m+1]. This is evident in the following picture:αi _iα^i α_iαj _jα^j α_j≤δ ≤δ(0,0)(0,0)(1,1)(1,1) In this unit square, the difference between the areas of the red and blue rectangles can be at most 2δ2δ. We now compute m⋅22B⋅|I2(μz,α^)−I2(μz,α)| m· 2^2B· | ^2_P( _z, α)- ^2_P( _z,α) | =|‖∑j=1m+1α^jϕ(zj)‖22−‖∑j=1m+1αjϕ(zj)‖22| = |\, \| _j=1^m+1 α_jφ(z_j) \|_2^2- \| _j=1^m+1 _jφ(z_j) \|^2_2\, | =|∑i=1m∑k=1m+1∑j=1m+1 = | _i=1^m _k=1^m+1 _j=1^m+1 α^jα^kϕi(zj)ϕi(zk)−∑(x,y,p)∈∑k=1m+1∑j=1m+1αjαkϕi(zj)ϕi(zk)| α_j α_k _i(z_j) _i(z_k)- _(x,y,p) _k=1^m+1 _j=1^m+1 _j _k _i(z_j) _i(z_k) | =|∑i=1m∑k=1m+1∑j=1m+1(α^jα^k−αjαk)ϕi(zj)ϕi(zk)| = | _i=1^m _k=1^m+1 _j=1^m+1( α_j α_k- _j _k) _i(z_j) _i(z_k) | ≤∑i=1m∑k=1m+1∑j=1m+1|α^jα^k−αjαk||ϕi(zj)ϕi(zk)| ≤ _i=1^m _k=1^m+1 _j=1^m+1| α_j α_k- _j _k|\,| _i(z_j) _i(z_k)| ≤(2δ−δ2)∑i=1m∑k=1m+1∑j=1m+1|ϕ(zj)ϕ(zk)| ≤(2δ-δ^2) _i=1^m _k=1^m+1 _j=1^m+1|φ(z_j)φ(z_k)| ≤2δ(m+1)3⋅(2B)2 ≤ 2δ(m+1)^3·(2^B)^2 Canceling the 22B2^2B scaling factor and dividing by m gives the desired result. ∎ We will also need the following straightforward fact about the density of fixed-precision binary numbers on the simplex. Lemma 11. For all α∈Δ[m+1]α∈ [m+1] and B∈ℕB , there exists an α′∈Δ[m+1]α ∈ [m+1] satisfying ‖α−α′‖∞≤2−B\|α-α \|_∞≤ 2^-B whose components are rational numbers of the form αi′=αi†/2Bα _i=α _i/2^B for some αi†∈ℤ≥0α _i _≥ 0. Proof of Lemma 11. Given α∈Δ[m+1]α∈ [m+1], start by truncating the first B bits of its binary representation of each component, i.e., define α′∈[0,1]m+1α ∈[0,1]^m+1 to be the vector whose ithi^th component is ⌊2Bαi⌋/2B 2^B _i /2^B. Clearly ‖α−α′‖∞≤2−B\|α-α \|_∞≤ 2^-B, but α′α will not be a distribution since ∑iαi′<1 _iα _i<1 unless 2Bα2^Bα is already a vector of integers. Let β:=1−∑iαi′β:=1- _iα _i be total mass missing from α′α required for it to be a distribution. Since the number 11 and each αi′α _i is an integer multiple of 2−B2^-B, so too is β. Let β†:=β⋅2B∈ℤβ :=β· 2^B be that multiple. Since each (αi−αi′)<2−B( _i-α _i)<2^-B by the definition of rounding, we know that β, which is the sum across all m+1m+1 components of the vector must be at most 2−B(m+1)2^-B(m+1), i.e., β†<m+1β <m+1. Finally, choose any vector v∈0,1m+1v∈\0,1\^m+1 with Hamming weight ∑ivi=β† _iv_i=β , and let α′:=α′+v⋅2−Bα :=α +v· 2^-B be the result of re-assigning all β†β units of missing mass to distinct components. Clearly α′α is non-negative, sums to one, and its components are rational with common denominator 2B2^B. ∎ Now to put the pieces together. The point is that the gap in the completeness hypothesis is exactly the room the rounding needs. Claim 12 (Sparse witnesses at bounded precision). Let τ≥εgap>0τ≥ _ gap>0 and let Bεgap=⌈log2(2(m+1)3/(εgap2m))⌉∈O(log(1/εgap)+logm)B_ _ gap= _2\! (2(m+1)^3/( _ gap^2m) ) ∈ O( ( 1 _ gap)+ m) as in Algorithm 1. If I(μ)≤τ−εgap _P(μ)≤τ- _ gap for some μ∈Δ(0,1n)μ∈ (\0,1\^n), then there are assignments z=(zj)j=1m+1z=(z_j)_j=1^m+1 and integer weights α†∈ℤ≥0m+1α _≥ 0^m+1 with ∑jαj†=2Bεgap _jα _j=2^B_ _ gap such that μ^≔μz,α†2−Bεgap μ _z,α 2^-B_ _ gap satisfies I(μ^)≤τ _P( μ)≤τ. Proof. By Carathéodory’s theorem, there are z∈(0,1n)m+1z∈(\0,1\^n)^m+1 and α∈Δ[m+1]α∈ [m+1] with μz,α[ϕ]=μ[ϕ] _ _z,α[φ]= _μ[φ], hence I(μz,α)=I(μ)≤τ−εgap _P( _z,α)= _P(μ)≤τ- _ gap. Set δ≔εgap2m/(2(m+1)3)δ _ gap^2m/(2(m+1)^3), so that 2−Bεgap≤δ2^-B_ _ gap≤δ. By Lemma 11, applied at precision BεgapB_ _ gap, there is α^=α†2−Bεgap∈Δ[m+1] α=α 2^-B_ _ gap∈ [m+1] with ‖α−α^‖∞≤2−Bεgap≤δ\|α- α\|_∞≤ 2^-B_ _ gap≤δ, and by Lemma 10 the rounding perturbs the squared inconsistency by at most 2δ(m+1)3/m=εgap22δ(m+1)^3/m= _ gap^2. Therefore I2(μ^)≤(τ−εgap)2+εgap2=τ2−2εgap(τ−εgap)≤τ2, ^2_P( μ)\;≤\;(τ- _ gap)^2+ _ gap^2\;=\;τ^2-2 _ gap(τ- _ gap)\;≤\;τ^2, using τ≥εgapτ≥ _ gap in the last step. ∎ Proof of Proposition 8. Soundness is the soundness paragraph above: the final check of Algorithm 1 is exact, so any accepted certificate exhibits a distribution μz,α _z,α with I(μz,α)≤τ _P( _z,α)≤τ. For completeness, suppose I(μ)≤τ−εgap _P(μ)≤τ- _ gap for some μ; in particular τ≥εgapτ≥ _ gap, since otherwise no such μ exists. The certificate (z,α†)(z,α ) of 12 has weights summing to 2Bεgap2^B_ _ gap, so it passes the first check, and the exact final check passes because I(μ^)≤τ _P( μ)≤τ. Its length is at most (m+1)(n+Bεgap)∈O(m(n+log(m/εgap)))(m+1)(n+B_ _ gap)∈ O(m(n+ ( m _ gap))). Efficiency is the runtime analysis above. ∎ In particular, if we care about numbers only up to the same precision as the problem instance, e.g., to 32-bit fixed point precision (εgap=2−B _ gap=2^-B), then witness weights of length (m+1)(2B+1+3log2(m+1))∈O(mB+mlogm)(m+1)(2B+1+3 _2(m+1))∈ O(mB+m m) suffice. 5.3 Polynomial-precision weights, and no gap (Proposition 9) To decide - Explicit-Consistency rather than its gapped version, the Verifier needs the exact optimal weights for the support, and those are not short. If the claims are represented to 16 bits, and we have a meager m=100m=100 claims, the bound of Lemma 13 below already asks for some 4600 bits per weight; we expect the AI systems and probabilistic models that motivate our interest in the - Explicit-Consistency problem to make many more claims, and for m equal to one million (2 megabytes of data) the figure is above 7×1077× 10^7 bits per weight, against the 105 that suffice at a gap of 2−322^-32. The remedy is not to send them at all. The support determines them, as (4) already suggests and Lemma 13 will show, so the Verifier can solve for them itself, and the polynomial precision is paid in its running time rather than in the certificate. The modified Verifier. Algorithm 1 is changed in one place. The certificate components α1†,…,αk† _1 ,…, _k are replaced by a single integer q. The Verifier constructs Mz≔[2VzVz0]∈ℤ(k+1)×(k+1)and solvesMz[αλ]=[1]M_z bmatrix2V_z TV_z&1\\ 1 T&0 bmatrix ^(k+1)×(k+1) solves M_z bmatrixα\\ λ bmatrix= bmatrix0\\ 1 bmatrix (5) from the residual matrix VzV_z of Algorithm 1, as follows. It rejects unless q is prime and MzM_z is non-singular modulo q; it solves (5) over ℚQ by q-adic lifting Dix 82, rejecting unless the returned (α,λ)(α,λ) satisfies (5) under exact substitution over ℤZ (concretely, writing α=α†/Dα=α /D and λ=λ†/Dλ=λ /D over the returned common denominator D>0D>0, it checks Mz(α†,λ†)=(,D)M_z(α ,λ ) T=(0,D) T over ℤZ); and it rejects unless αj>0 _j>0 for every j∈[k]j∈[k]. It then writes α=α†/Dα=α /D over the returned common denominator D, and runs the last two lines of Algorithm 1 with D in place of 2Bεgap2^B_ _ gap. The gap εgap _ gap plays no part in the modified Verifier: setting BεgapB_ _ gap was its only role. Soundness is the argument of the previous subsection verbatim: the Verifier ends holding a support and weights, so (4) makes its final check exact. Worth noting is that it uses nothing about q. Whatever the Prover supplies, the Verifier accepts only a pair (α,λ)(α,λ) satisfying (5) under its own exact substitution check over ℤZ, the last row of which reads α=11 Tα=1, and only when every αj _j is strictly positive; so the accepted α is a distribution whether or not q was prime and whether or not it divided detMz M_z. The prime bears on completeness and on the running time, never on soundness. For completeness, suppose there exists a distribution μ∈Δ(0,1n)μ∈ (\0,1\^n) with I(μ)≤τ _P(μ)≤τ. By Carathéodory’s Theorem, we know there exists a μ′μ that is supported on only m+1m+1 points with the same value; here, we show that in particular there exists one whose weights are pinned down by the support alone, and are rational numbers with O(mB+mlogm)O(mB+m m) bits. For this, we need the following Lemma. Lemma 13. If m+1≥km+1≥ k and V∈ℤm×kV ^m× k is an integer matrix whose entries are bounded in magnitude by 2B2^B, then the optimization problem minα∈ℝk‖Vα‖22subject toα≥0,∑i=1kαi=1 _α ^k \|Vα \|^2_2 to~~α≥ 0,~ _i=1^k _i=1 (6) admits a rational solution α∗α^* whose components have a common denominator representable in O(mlogm+Bm)O(m m+Bm) bits. Moreover, writing S for the support of such a solution of minimal support, s≔|S|s |S|, and M for the matrix (5) formed from the columns VSV_S: 1. M is non-singular, so that (αS∗,λ)(α^*_S,λ) is the unique solution of M(a,λ)=(,1)M(a,λ) T=(0,1) T; 2. αS∗>0α^*_S>0 entrywise; and 3. |detM|≤(2B(m+2))2(m+2)| M|≤ (2^B(m+2) )^2(m+2). Proof. Let α∈Δ[k]α∈ [k] be a solution to (6) with minimal support S=i∈[k]:αi>0S=\i∈[k]: _i>0\, and let s≔|S|s |S|. We will show that this solution has the desired rational property. Write αS _S for the restriction of α to its support, and VS∈ℤm×sV_S ^m× s for the restriction of V to the corresponding columns. Since αS>0 _S>0 is positive in this subspace, αS∈Δ[s] _S∈ [s] is the solution to the modified problem mina∈ℝs‖VSa‖22subject to∑i∈Sai=1. _a ^s \|V_Sa \|_2^2 to _i∈ Sa_i=1. The stationary point can be found with a single Lagrange multiplier λ corresponding to this one constraint. More precisely, the Lagrangian is given by ℒ(a,λ)=‖VSa‖22+λ(−1+∑iai)L(a,λ)=\|V_S\,a\|_2^2+λ(-1+ _ia_i), and a solution a must satisfy ∇ℒ=0 =0. Since ∇a‖VSa‖22=2VSVSa _a\|V_S\,a\|_2^2=2V_S TV_S\,a, the stationary condition gives us the system of equations 0=∇a,λℒ(a,λ)=[2VSVSa+λa−1]=[2VSVS0][aλ]−[01],0= _\!a,λ\,L(a,λ)= bmatrix2V_S TV_S\,a+ 1\\ 1 Ta-1 bmatrix= bmatrix2V_S TV_S&1\\ 1 T&0 bmatrix bmatrixa\\ λ bmatrix- bmatrix0\\ 1 bmatrix, (7) which is the system (5) formed from VSV_S. Since it’s a linear system of equations with integer coefficients, it has a rational solution. To bound its magnitude, we use the form on the right-hand side of (7). Let M≔[2VSVS0]∈ℤ(s+1)×(s+1)M bmatrix2V_S TV_S&1\\ 1 T&0 bmatrix ^(s+1)×(s+1) be the key matrix on the right. We claim that M is non-singular. In search of contradiction, suppose that My=0My=0 for some nonzero y=(d,γ)∈ℝs+1y=(d,γ) T ^s+1. This means that (a) 0=2VSVSd+γ0=2V_S TV_Sd+ 1 and (b) d=01 Td=0. Left-multiplying equation (a) by d T and substituting equation (b), we find that 0=2dVSVSd+γd= 2dVSVSd= 2‖VSd‖22, 0=2d TV_S TV_Sd+γ d T1\;=\;2d TV_S TV_Sd\;=\;2\|V_Sd\|_2^2, from which it follows that VSd=0V_Sd=0. Plugging this back into equation (a) above, we find that 0=γ0= 1, meaning γ=0γ=0. Since y=(d,γ)≠0y=(d,γ)≠ 0 by assumption, this implies d≠0d≠ 0. Altogether, this means we have a vector d∈ℝsd ^s with the properties d≠0,VSd=0,andd=0,d≠ 0, V_S\,d=0, 1 Td=0, meaning that ‖VS(a+d)‖22=‖VSa‖22\|V_S(a+d)\|_2^2=\|V_S\,a\|_2^2 and (a+d)=a=11 T(a+d)=1 Ta=1. In other words, if a is a solution to the optimization problem, so too is a+tda+td, provided a+td≥0a+td≥ 0. Since d=01 Td=0 and d≠0d≠ 0, some component of d is negative, so t∗≔mini:di<0(−ai/di)t^* _i:d_i<0(-a_i/d_i) is well defined and positive; a+t∗da+t^*d is then non-negative, sums to one, and is zero in some component, so it is a solution to the optimization problem with strictly smaller support, contradicting minimality. Now that we know M∈ℤ(s+1)×(s+1)M ^(s+1)×(s+1) is non-singular, we can apply Cramer’s rule, which tells us that the unique solution (α∗,λ)(α^*,λ) T at component i is equal to (detMi)/(detM)( M_i)/( M), where MiM_i is the matrix obtained by replacing the ithi^th column of M by [0,…,0,1][0,…,0,1] T. Since M and MiM_i have integer components, their determinants are integers, and thus α is a rational number whose common denominator divides |detM|| M|. All that remains is to bound detM M, for which we turn to Hadamard’s inequality Had 93, which states that the determinant of a matrix is at most the product of the L2 norms of its columns. Every entry of the upper-left block of M is twice a sum of m numbers, each a product of two integers of magnitude at most 2B2^B, and is thus at most 2m⋅22B2m· 2^2B in magnitude. The L2 norm of each column is therefore at most 2ms+1⋅22B+12m s+1· 2^2B+1, and thus the common denominator is of the order detM M ≤(2ms+1⋅22B+1)s+1 ≤ (2m s+1· 2^2B+1 )^s+1 ≤(2B(m+2))2(m+2)≤ 22(m+2)(B+⌈log2(m+2)⌉) ≤ (2^B(m+2) )^2(m+2)\;≤\;2^2(m+2)(B+ _2(m+2) ) ∈2O(mlogm+Bm) ∈ 2^O(m m+Bm) since s≤k≤m+1s≤ k≤ m+1. Therefore, it can be represented with O(mlogm+Bm)O(m m+Bm) bits. Finally, the non-singularity of M bounds the support: were s>m+1s>m+1, the s columns of [VS]∈ℝ(m+1)×s bmatrixV_S\\ 1 T bmatrix ^(m+1)× s would be linearly dependent, giving a nonzero d with VSd=0V_Sd=0 and d=01 Td=0, which the argument above has just ruled out. ∎ Let’s now apply Lemma 13 to finish off the proof of completeness. Recall that we are in the case where there exists a distribution μ with I(μ)≤τ _P(μ)≤τ, and that Carathéodory’s theorem guarantees the existence of a witness (z,α)(z,α) of m+1m+1 points. Applying Lemma 13 to V=VzV=V_z and taking S to be the support of a minimal-support optimum α∗α^*, the Carathéodory weights α are feasible for (6), so ‖Vzα∗‖2≤‖Vzα‖2\|V_zα^*\|_2≤\|V_zα\|_2, and (4) turns this into I(μzS,αS∗)≤I(μz,α)=I(μ)≤τ _P( _z_S,α^*_S)≤ _P( _z,α)= _P(μ)≤τ. Its support satisfies s≤k=m+1s≤ k=m+1. The honest Prover sends exactly this support zSz_S. The Verifier forms MzSM_z_S, which is non-singular by clause 1, so the solve returns αS∗α^*_S and nothing else; these weights are strictly positive by clause 2, so the Verifier does not reject; and the final check passes because I(μzS,αS∗)≤τ _P( _z_S,α^*_S)≤τ. The weights themselves are never transmitted, so the certificate is s⋅n≤(m+1)ns· n≤(m+1)n bits of support, together with the prime, which we bound next. It remains to exhibit the prime. Write BM≔2(m+2)(B+⌈log2(m+2)⌉)∈O(mlogm+Bm)B_M 2(m+2)(B+ _2(m+2) )∈ O(m m+Bm), so that clause 3 of Lemma 13 bounds detMzS M_z_S in magnitude by 2BM2^B_M. Being a nonzero integer of magnitude at most 2BM2^B_M, it has at most BMB_M distinct prime divisors, so among the first BM+1B_M+1 primes there is one, call it q, that does not divide it; and by Chebyshev’s bound the (BM+1)(B_M+1)st prime is O(BMlogBM)O(B_M B_M), so q is representable in O(logBM)=O(logm+logB)O( B_M)=O( m+ B) bits.77 7 Concretely, at m equal to one million and B=32B=32, a 3232-bit number suffices. Elimination modulo q then certifies that detMzS≢0 M_z_S ≡ 0, hence that MzSM_z_S is non-singular over ℚQ, and seeds the q-adic lifting of Dix 82, which returns the exact rational solution of (5) in O(m3(B+logm)2)O(m^3(B+ m)^2) bit operations. The certificate is therefore of length (m+1)n+O(logm+logB)∈O(mn+logB)(m+1)n+O( m+ B)∈ O(mn+ B), as claimed. Why the prime is sent. It is not needed for correctness, only for speed, and it is free: at O(logm+logB)O( m+ B) bits it does not affect the certificate length above, and at m equal to one million and B=32B=32 it is a 3131-bit number. Its role is to spare the Verifier the search. A Verifier finding its own good prime would test candidates until one fails to divide detMzS M_z_S, and there may be as many as BMB_M bad ones, each ruled out by an elimination; a Verifier avoiding the question altogether, by fraction-free elimination over ℤZ, would instead carry Θ(m(B+logm)) (m(B+ m))-bit intermediates through Θ(m3) (m^3) operations. Either route costs a factor of m or more over the bound above, and neither changes what the Verifier accepts, since the returned solution is checked exactly in any case. For the runtime, the accounting of the previous subsection applies with BMB_M in place of BεgapB_ _ gap: its inner loop costs O(m2(n+BBM))⊆O(m2n+m3B(B+logm))O(m^2(n+B_M)) O(m^2n+m^3B(B+ m)) and its accumulation costs O(mBM2)=O(m3(B+logm)2)O(mB_M^2)=O(m^3(B+ m)^2), so the final check costs O(m3(B+logm)2+m2n)O(m^3(B+ m)^2+m^2n); forming 2VzVz2V_z TV_z and the exact substitution check cost O(m3(B+logm)2)O(m^3(B+ m)^2) as well, and adding the O(m3(B+logm)2)O(m^3(B+ m)^2) of the solve leaves the total unchanged, giving the O(m3(B+logm)2+m2n)O(m^3(B+ m)^2+m^2n) of Proposition 9. This completes its proof. 6 Hardness of approximating consistency in (deterministic) CPCs In this section we observe that CPCs can be used to express CNF formulas in a straightforward and ‘lossless’ fashion. 88 8 A related reduction has been documented in the theory probabilistic dependency graphs RHS 23, but the one we present here is more direct, and the inapproximability lifts more directly in the normalized ℓ2 _2 inconsistency measure. Consequently, we can use tight inapproximability results for -k Exact-k SAT to automatically obtain inapproximability of - Explicit-Consistency to the same parameters, and Corollary 18 lifts this to NEXP-hardness of - Model-Consistency. The reduction (16) preserves many properties of the source formula, such as bounded variable occurrence, arity,99 9 Formally, the arity of the probabilistic claim (x,y,p)(x,y,p) is equal to k=k′+1k=k +1, where k′k is the number of non-∗ entries in x. The arity of a CPC P is the maximal arity among its claims. and the fraction of violated clauses/claims by any assignment. However, - Explicit-Consistency allows distributions over assignments as “solutions.” To argue that the reduction is gap-preserving, we (tightly) bound I() (P) of the reduced CPCs in terms of the fraction of claims violated by an assignment in Lemma 15. 6.1 Violated claims and inconsistency in deterministic CPCs The CPCs derived from CNFs are deterministic, in the sense that all claims are about events that occur (or do not occur) with certainty. Definition 14 (Deterministic CPC). A CPC P is deterministic if for all (x,y,p)∈(x,y,p) it holds that p∈0,1p∈\0,1\.1010 10 Tedious comment: the precision-B numerator convention p=p†/2Bp=p /2^B with p†∈0,…,2B−1p ∈\0,…,2^B-1\ excludes p=1p=1; for deterministic claims we admit the numerator p†=2Bp =2^B as well, so that p∈0,1p∈\0,1\ is representable at every precision. This adds one numerator value (B+1B+1 bits per claim) and affects no bound. We say that assignment w∈0,1nw∈\0,1\^n violates the claim (x,y,p)∈(x,y,p) if w agrees with the context x, and wy=1−pw_y=1-p. We let Viol(w) _P(w) denote the fraction of claims in P violated by w, Viol(w)≔|P∈:w violates P|||,Viol()≔minw∈0,1nViol(w). _P(w) | \P :w violates P \ ||P|, (P) _w∈\0,1\^n _P(w). Lemma 15. Let P be a deterministic CPC. Then Viol()≤I()≤Viol(). (P)≤ (P)≤ (P). Proof of Lemma 15. Let n be the number of variables of P. First, observe that for any (x,y,p)∈(x,y,p) and any w∈0,1nw∈\0,1\^n, letting δw _w denote the point mass distribution supported on w, |δw(x∩y)−pδw(x)|=1ifw violates (x,y,p)0otherwise.| _w(x∩ y)-p _w(x)|= cases1 \ w violates (x,y,p)\\ 0 . cases (8) Because if w violates (x,y,p)(x,y,p) then, by definition, w agrees with x which means that δw(x)=1 _w(x)=1, but wy=1−pw_y=1-p. By case analysis, this means that δw(x∩y)=1−p _w(x∩ y)=1-p, therefore (δw(x∩y)−pδw(x))2=1( _w(x∩ y)-p _w(x))^2=1. Conversely, if w does not violate (x,y,p)(x,y,p), then there are two possibilities: Either w does not extend x in which case δw(x)=δw(x∩y)=0 _w(x)= _w(x∩ y)=0, or w agrees with x and wy=pw_y=p, in which case δw(x∩y)=p=pδw(x) _w(x∩ y)=p=p _w(x). We now prove the lemma, starting from the leftmost inequality. Let n denote the number of variables of P, and let μ be a distribution over 0,1n\0,1\^n. We will show that I(μ)≥Viol() _P(μ)≥ (P). Let S=w1,…,wsS=\w_1,…,w_s\ denote the support of μ. Let δi≔δwi _i _w_i denote the point mass distribution supported on wiw_i, and so we write μ=∑i=1sαiδiμ= _i=1^s _i _i where αi>0 _i>0 for all i∈[s]i∈[s] and ∑iαi=1 _i _i=1. Then we can write I2(μ) ^2_P(μ) =1m∑(x,y,p)∈|μ(x∩y)−pμ(x)|2. = 1m _(x,y,p) |μ(x∩ y)-pμ(x) |^2. =1m∑(x,y,p)∈(∑i=1sαi|δi(x∩y)−pδi(x)|)2 = 1m _(x,y,p) ( _i=1^s _i | _i(x∩ y)-p _i(x) | )^2 Which, by the Cauchy–Schwartz inequality, is I2(μ) ^2_P(μ) ≥1m⋅1m(∑(x,y,p)∈∑i=1sαi|δi(x∩y)−pδi(x)|)2 ≥ 1m· 1m ( _(x,y,p) _i=1^s _i | _i(x∩ y)-p _i(x) | )^2 =(∑i=1sαi⋅1m∑(x,y,p)∈|δi(x∩y)−pδi(x)|)2, = ( _i=1^s _i· 1m _(x,y,p) | _i(x∩ y)-p _i(x) | )^2, By Equation 8 and definition of Viol() (P) as minwViol(w) _w _P(w) we have I2(μ)≥(∑i=1sαiViol(wi))2≥(Viol()⋅∑i=1sαi)2=Viol()2. ^2_P(μ)≥ ( _i=1^s _i _P(w_i) )^2≥ ( (P)· _i=1^s _i )^2= (P)^2. Taking the square root of both sides gives the lower bound. For the upper bound, let w∈0,1nw∈\0,1\^n, we will show that Viol(w)=I2(δw) _P(w)= ^2_P( _w) and so in particular Viol(w)≥I2() _P(w)≥ ^2(P). By Equation 8 and definition of Viol(w) _P(w) as the fraction of claims violated by w, I2(δw)=1m∑(x,y,p)∈(δw(x∩y)−pδw(x))2=Viol(w), ^2_P( _w)= 1m _(x,y,p) ( _w(x∩ y)-p _w(x))^2= _P(w), using the fact that the summands are Boolean (Equation 8), therefore each summand’s square coincides with its absolute value. ∎ Tightness of Lemma 15. The lower and upper bounds are of course attained for consistent deterministic CPCs, because all quantities are zero. Let us briefly detour to discuss tightness for inconsistent instances. The lower bound can still be an equality: consider a CPC containing just two contradictory claims (∗,y,0),(∗,y,1)\( ,y,0),( ,y,1)\; then Viol()=1/2 (P)=1/2, and I()=(1/4+1/4)=1/2 _P(U)=(1/4+1/4)=1/2 as well for the uniform distribution over its single variable. For the upper bound, we first note that it becomes an equality if and only if the CPC is consistent. To see this, let P be an inconsistent deterministic CPC with ||=m|P|=m claims, and let w∗∈0,1nw ∈\0,1\^n be a maximally satisfying assignment. Take any claim P∈P violated by w∗w , and take wP∈0,1nw_P∈\0,1\^n to be any assignment that satisfies the claim P. Consider the distribution μ that assigns mass (1−1/m)(1-1/m) to w∗w and 1/m1/m mass to wPw_P. Then any claim satisfied by w∗w is violated by μ with probability at most 1/m1/m, but now P is violated by μ with probability (1−1/m)(1-1/m), giving I(μ)2≤Viol(w∗)−1/||2<Viol(w∗)=Viol() _P(μ)^2≤ _P(w )-1/|P|^2< _P(w )= (P) (9) That said, the inequality in Equation 9 (and the upper-bound of Lemma 15 more generally) can approach equality as the number of claims m grows by simply adding more consistent claims: Consider a single-variable CPC mP_m containing a single copy of ∗,y,0\*,y,0\ and m−1m-1 copies of ∗,y,1\*,y,1\. Then Viol()=1/m (P)=1/m, but similarly to the argument before Equation 9, a distribution μ that assigns y=0y=0 with probability 1/m1/m will have I(μ)2=Viol()−1/m2 _P(μ)^2= (P)-1/m^2, so the ratio I(μ)2/Viol()→1 _P(μ)^2/ (P)→ 1 as m→∞m→∞. 6.2 Reduction from -k Exact-k SAT. Let F be an Exact kkCNF formula over n Boolean variables. We let |F||F| denote its number of clauses, and for any assignment w∈0,1nw∈\0,1\^n we let ViolF(w) _F(w) denote the number of clauses violated by w in F. We write Viol(F)=1|F|minw∈0,1nViolF(w). (F)= 1|F| _w∈\0,1\^n _F(w). Claim 16. There is a polynomial-time computable reduction mapping Exact kkCNF formulas F to deterministic CPCs FP_F, such that Viol(F)=Viol(F) (F)= (P_F). Proof. Let F=Fjj=1mF=\F_j\_j=1^m be a Exact kkCNF formula with m clauses over n variables. We write Fj=(j1=b1∨⋯∨jk=bk)F_j=(j_1=b_1 … j_k=b_k) for variables j1,…,jk∈[n]j_1,…,j_k∈[n] and bits b1,…,bk∈0,1b_1,…,b_k∈\0,1\.1111 11 Formally, bi=0b_i=0 indicates that the variable jij_i is negated in the clause, and we assume the j1,…,jkj_1,…,j_k are sorted. For each clause FjF_j, the reduction adds the Probabilistic Claim Pj=(xj,jk,bk)P_j=(x^j,j_k,b_k) where xjij=(1−bi)x^j_j_i=(1-b_i) for each i∈[k−1]i∈[k-1], and the rest of xjx^j’s entries are set to ∗ . The output of the reduction is the instance =Pjj=1mP=\P_j\_j=1^m. Note that |F|=|F||F|=|P_F|, and so to prove the claim it suffices to show that for any assignment w∈0,1nw∈\0,1\^n, the number of clauses of F that w violates equals the number of claims of P that w violates; since |F|=|F||F|=|P_F|, the violated fractions then coincide as well. We will show a correspondance between violated clauses and claims: w violates the clause Fj=(j1=b1∨⋯∨jk=bk)F_j=(j_1=b_1 … j_k=b_k) if and only if wji=1−biw_j_i=1-b_i for all i∈[k]i∈[k]. By construction, this is equivalent to having w extend xjx^j but wjk=1−bkw_j_k=1-b_k, i.e., w violates PjP_j. ∎ Claim 17. For all δ∈(0,2−k)δ∈(0,2^-k) and k≥3k≥ 3, the following promise problem is NP-hard. The instance is a (deterministic) CPC P such that I()≤2−k (P)≤ 2^-k, and the goal is to distinguish • YES: I()=0 (P)=0, from • NO: I()≥2−k−δ (P)≥ 2^-k-δ, Proof. Fix k≥3k≥ 3 and δ∈(0,2−k)δ∈(0,2^-k). Theorems 6.5 and 6.14 of Hås 01 give a polynomial time reduction from any L∈L∈ NP to Exact kkCNF formulas F mapping instances of L to • YES: The set of satisfiable Exact kkCNF formulas F, i.e., Viol(F)=0 (F)=0, • NO: The set of Exact kkCNF formulas F such that Viol(F)≥2−k−δ (F)≥ 2^-k-δ. For each Exact kkCNF F, we apply 16 to obtain the corresponding deterministic CPC FP_F. We first observe that I(F)≤2−k (P_F)≤ 2^-k. This follows from the fact that a clause is violated by a random assignment with probability 2−k2^-k: letting U denote the uniform distribution over 0,1n\0,1\^n, I(F)≤IF()=1|F|∑(xj,jk,bk)∈F((xj∩jk)−bk(xj))2=1|F|⋅|F|⋅2−2k=2−k, (P_F)≤ _P_F(U)= 1|F| _(x^j,j_k,b_k) _F (U(x^j∩ j_k)-b_kU(x^j) )^2= 1|F|·|F|· 2^-2k=2^-k, where the rightmost equality uses the fact that xjx^j has exactly k−1k-1 non-∗ entries. Completeness and soundness of the reduction follow from combining 16 with Lemma 15. If Viol(F)=0 (F)=0 then by 16, Viol(F)=0 (P_F)=0, and so by Lemma 15, I() (P) is sandwiched between zeros. Conversely, if Viol(F)≥2−k−δ (F)≥ 2^-k-δ then by the lower bound of the lemma, I()≥2−k−δ (P)≥ 2^-k-δ. ∎ 6.3 NEXP-completeness of - Model-Consistency Recall the implicit CPC P,QP_P,Q of a predictive model (Definition 6): the exponentially long collection that has, for each query q∈q , Q(q)Q(q) copies of the claim (xq,ωt,P(q)/2B)(x_q, _t,P(q)/2^B), and whose consistency is that of the model (7). With this translation in hand, NEXP-completeness is short to derive. Corollary 18. - Model-Consistency is NEXP-complete (under polynomial-time many-one reductions). Proof. For membership, let V_ NP be the verifier of Proposition 9, and let V_ NEXP be the verifier that, on input (P,Q,τ)(P,Q,τ) and proof π, constructs P,QP_P,Q explicitly—in time 2O(ℓd+B)⋅O(S)2^O( d+B)· O(S), where S bounds the sizes of the circuits P and Q—and accepts if and only if V(P,Q,τ,π)V_ NP(P_P,Q,τ,π) accepts. By 7, (P,Q)(P,Q) is τ-consistent if and only if P,QP_P,Q is, so completeness and soundness are those of Proposition 9. Using the fact that ‖Q‖∈2O(ℓd+B)||Q||∈ 2^O( d+B), Proposition 9 implies that running V_ NP on P,QP_P,Q takes time ‖Q‖3(B+log‖Q‖)2+‖Q‖2n∈2O(ℓd+B)||Q||^3(B+ ||Q||)^2+||Q||^2n∈ 2^O( d+B) with proofs of length O(‖Q‖⋅n+logB)∈2O(ℓd+B)O(||Q||· n+ B)∈ 2^O( d+B), so all together V_ NEXP runs in time exponential in its input length. For hardness, - Model-Consistency is the succinct version of - Explicit-Consistency, so the reduction of 16 applies as a reduction from the SUCCINCT--k Exact-k SAT problem (see, e.g., PY 86; Gol 08). ∎ Remark 19 (A pragmatic aside on implementation). Producing a faithful implementation of the black-box construction underlying Corollary 18 (specification, code, and checking that the two match) is, in the authors’ own experience and despite considerable effort, well beyond the scope of an empirical pilot: we speculate it would occupy a graduate student fluent in the relevant literature for a semester or two: disentangling the Cook–Levin compilation and the BFLS arithmetization layers from one another. The remainder of this paper is dedicated to constructing an Interactive PCP that admits a self-contained specification (Algorithm 6) whose proof oracle is simply a specialized encoding of the witnessing distribution (Section 7); the same hypothetical graduate student should, on our reading, be able to get experiments running on top of Algorithm 6 in a matter of weeks. 7 Reed–μ : a marginal-verifiable distribution encoding The PCP component of our IPCP will be a locally-verifiable encoding of distributions which enables efficient (interactive) verification of marginals. This is essentially an encoding of distributions that enables delegation of marginal computation; we present it as a self-contained “library” consisting of the encoding method (Definition 21), codeword-validity verifier (Algorithm 3) and marginal verifier (Algorithm 5), which may be of independent interest. To keep the exposition self-contained, we open with a standalone motivating story, in the storytelling tradition of Bab 85; Bab 90. All-powerful Merlin (the Prover) holds a distribution μ over 0,1n\0,1\^n, the truth-assignments to n propositions. Each proposition is named by a short address of d=lognd= n bits; picture a sentence king Arthur (the Verifier) could scrawl on one line, a hundred bits or so, so that n=2d≈2100n=2^d≈ 2^100. Merlin’s μ is the verdict of a finite engine, vastly smaller than the 2n2^n worlds it opines on, so it can deem only a modest number m of assignments possible. He describes it by its support: points z1,…,zm∈0,1nz_1,…,z_m∈\0,1\^n with weights μ(z1),…,μ(zm)∈[0,1]μ(z_1),…,μ(z_m)∈[0,1]. (In the application this section serves, Carathéodory pins m=(n)m= poly(n); see Section 5. In this section, m is a free parameter.) Arthur, his computationally bounded sovereign, wants two assurances. First, that μ is a distribution at all: that the weights are nonnegative and that ∑j=1mμ(zj)=1. _j=1^mμ(z_j)=1. Second, he wants to interrogate it. To learn, say, the chance that the first proposition holds and the second fails, Arthur must total the mass of every possible world that agrees: μ(ω1=1,ω2=0)=∑j:zj,1=1,zj,2=0μ(zj).μ( _1=1,\ _2=0)\;=\; _j:z_j,1=1,\ z_j,2=0μ(z_j). Each such question is a sum over Merlin’s m possible worlds, costing Ω(m) (m) to answer by hand. And m is the least of Arthur’s troubles: his entire budget is (d)=(logn) poly(d)= poly( n), so he cannot even tour the n=2dn=2^d propositions, let alone audit a sum over worlds. This section is the remedy. Merlin encodes μ once, as π(μ)π(μ), and hands it over; thereafter, with a few rounds of interaction and his own coin flips, Arthur convinces himself that μ is a genuine distribution in time O(logm+logn)O( m+ n), and verifies any marginal μ(ω1=1,ω2=0)μ( _1=1, _2=0) just as cheaply. More generally, he verifies the marginal on any ℓ propositions in time O(ℓlogm+logn)O( m+ n). The encoding of μ is a Reed–Muller encoding of the support vectors and their weights (in binary); as such, we denote it μ R .1212 12 The notation reads as “Reed–μ ,” a Reed–Muller (RM) encoding of the distribution μ. Before we define it, we first recall the notion of a multilinear extension. Definition 20 (i-linear, multilinear extension). Fix k∈ℕk and i∈[k]i∈[k], we say that a function f:k→f ^k is i-linear if, for all x1,…,xi−1,xi+1,…,xk∈x_1,…,x_i-1,x_i+1,…,x_k , the univariate function f′:→f defined by f′(ξ)≔f(x1,…,ξ,…,xk)f (ξ) f(x_1,…,ξ,…,x_k) is linear. We say that a function f is multilinear if it is i-linear in each of its coordinates. For a function g0:0,1k→0,1g_0 \0,1\^k→\0,1\, its multilinear extension g^:k→ g ^k is defined by g^(x)≔∑x′∈0,1kg0(x′)∏i=1k(xixi′+(1−xi)(1−xi′)) g(x) _x ∈\0,1\^kg_0(x ) _i=1^k (x_ix _i+(1-x_i)(1-x _i) ). It is the only multilinear function agreeing with g0g_0 on the entirety of 0,1k\0,1\^k. Definition 21 (μ R ). Let n,m,B∈ℕn,m,B and let μ be a distribution over 0,1n\0,1\^n. Assume that μ is supported on m points with weights expressible as B-bit precision rationals; that is, there are z1,…,zm∈0,1nz_1,…,z_m∈\0,1\^n, and α1†,…,αm†∈0,…,2B−1α _1,…,α _m∈\0,…,2^B-1\ such that μ is supported on zjz_j with weight μ[zj]=αj†/2Bμ[z_j]=α _j/2^B. For j∈[m],i∈[n]j∈[m],i∈[n] we let zj,iz_j,i denote the iith coordinate of zjz_j. Similarly, for j∈[m]j∈[m] and β∈0,…,B−1β∈\0,…,B-1\ let αj,β†α _j,β denote the β bit of αj†α _j, such that αj†=∑β=0B−12βαj,β†α _j= _β=0^B-12^βα _j,β. We denote Z0:0,1logm×0,1logn→0,1 Z_0 \0,1\ m×\0,1\ n→\0,1\ Z0(j,i)=zj,i Z_0(j,i)=z_j,i A0:0,1logm×0,1logB→0,1 A_0 \0,1\ m×\0,1\ B→\0,1\ A0(j,β)=αj,β† A_0(j,β)=α _j,β For a finite field F, let Z~ Z (resp. A~ A) denote the multilinear extension of Z0Z_0 (resp. A0A_0). A μ(n,m,B) R _F(n,m,B)-encoding of μ is the pair (Z~,A~)( Z, A). We use μ(n,m,B) R _F(n,m,B) to denote the set of all such valid encodings. Namely, (Z,A)∈μ(n,m,B)(Z,A)∈ R _F(n,m,B) if and only if 1. Multilinearity: Both Z and A are multilinear. 2. Booleanity: For any j∈0,1logmj∈\0,1\ m, i∈0,1logni∈\0,1\ n, and β∈0,1logBβ∈\0,1\ B it holds that Z(j,i)\Z(j,i), A(j,β)⊆0,1A(j,β)\ \0,1\. 3. Unit measure: For j∈0,1logmj∈\0,1\ m, let aj†∈0,…,2B−1a _j∈\0,…,2^B-1\ be the integer represented by the B-bit string (A(j,β))β∈0,1logB(A(j,β))_β∈\0,1\ B. Then ∑j∈0,1logmaj†=2B _j∈\0,1\ ma _j=2^B. We note that μ R is not an error-correcting code in the standard sense, because a distribution μ supported on m vectors z1,…,zmz_1,…,z_m may be encoded in one of m!m! ways (one for each ordering of its support vectors). One could require the vectors z1,…,zmz_1,…,z_m to be ordered lexicographically, but then one would also have to test that an alleged codeword respects this order—an added complication which is entirely unnecessary for our purposes. Hereafter when we consider an encoding of μ, we let it be an encoding in an arbitrary order. 7.1 Prerequisites: the sum-check protocol, and four multilinear gadgets We recall the sum-check protocol LFKN 92, modified slightly for convenience. Input: rounds,deg∈ℕ rounds, deg , a finite field F of odd characteristic, and val∈ val . Output: y^∈rounds y rounds and v^∈ v . Verifier: Initialize the running value u←vu← v. 1 for k=1,…,roundsk=1,…, rounds do 2 Prover: Send a1,a2,…,adeg∈a_1,a_2,…,a_ deg . 3 Verifier: Compute a0≔2−1⋅(u−a1−a2−⋯−adeg)a_0 2^-1·(u-a_1-a_2-·s-a_ deg) where 2−12^-1 is over F. Sample y^k∈ y_k uniformly at random and send y^k y_k to the Prover. Update u←∑i=0degaiy^kiu← _i=0 dega_i y_k^i. 4 Verifier: Output v^←u v← u and y^←(y^1,…,y^rounds) y←( y_1,…, y_ rounds). Algorithm 2 (val,rounds,deg) SumCheck_F( val, rounds, deg). Fact 22 (LFKN 92). Let r,d∈ℕr,d , a finite field F of odd characteristic, and v∈v . Let φ∈[Y1,…,Yr] [Y_1,…,Y_r] be an r-variate polynomial that has individual degree at most d in each of its variables. (v^,y^)( v, y) denote the output of (val←v,rounds←r,deg←d) SumCheck_F( val← v, rounds← r, deg← d), noting that this is a random variable determined by the sampled y y. Then, • Completeness. If v=∑y∈0,1rφ(y)v= _y∈\0,1\^r (y) over F then there exists an honest Prover such that v^=φ(y^) v= ( y) with probability 11 over y y. • Soundness. Otherwise, v^=φ(y^) v= ( y) with probability at most rd/||rd/|F|. Furthermore, Algorithm 2 has r many rounds, in which the Prover (resp. Verifier) sends a total of r⋅dr· d (resp. r) field elements. The Verifier makes a total of O(rd)O(rd) field operations. Lastly, y y is distributed marginally uniformly in roundsF rounds. Algorithm 2 is the sum-check protocol of LFKN 92, presented with two cosmetic changes that streamline its use as a subroutine. First, the per-round equality gk(0)+gk(1)=uk−1g_k(0)+g_k(1)=u_k-1 that the standard Verifier checks is instead enforced by construction: In the standard protocol the Prover sends, in round k, an individual degree-d polynomial gk(Y)=∑i=0daiYig_k(Y)= _i=0^da_iY^i, and the Verifier checks gk(0)+gk(1)=uk−1g_k(0)+g_k(1)=u_k-1 before sampling y^k y_k and updating uk←gk(y^k)u_k← g_k( y_k); whereas in Algorithm 2 the Prover sends only the d non-free coefficients a1,…,ada_1,…,a_d, and the Verifier sets the free coefficient to a0←2−1(uk−1−a1−⋯−ad)a_0← 2^-1(u_k-1-a_1-·s-a_d), the unique value for which gk(0)+gk(1)=uk−1g_k(0)+g_k(1)=u_k-1.1313 13 This is the one place odd characteristic of F is used Second, the final test ur=?φ(y^)u_r ?= ( y) that the standard Verifier asserts is deferred: Algorithm 2 outputs the pair (y^,v^)=(y^,ur)( y, v)=( y,u_r) and leaves the comparison v^=?φ(y^) v ?= ( y) to its caller. We find this presentation useful for two reasons: The Verifier of Algorithm 2 never rejects; it only samples randomness and maintains the running value u, so its actions depend on v, r, and d alone and never on φ . And the round polynomials gkg_k never enter the Verifier’s computation: they are objects of the analysis, not of the protocol. We still name the parties Prover and Verifier because, facing forward, each invocation of Algorithm 2 in Section 8.2 will be run by the main protocol’s Verifier. The protocols accompanying μ R below rely on four multilinear polynomials “gadgets.” We collect them here. eq: For t∈ℕt and y^,y′∈t y,y ^t, (y^,y′)≔∏i=1ty^iyi′+(1−y^i)(1−yi′). eq( y,y ) _i=1^t y_iy _i+(1- y_i)(1-y _i). (10) On Boolean y^,y′ y,y it equals 11 if y^=y′ y=y and 00 otherwise, so it is the (unique) multilinear extension of the equality indicator on 0,1t\0,1\^t. vec2int: For β∈logBβ B, (β)=(β1,…,βlogB)≔∏k=1logB1+βk(22k−1−1). vec2int(β)= vec2int( _1,…, _ B) _k=1 B1+ _k(2^2^k-1-1). (11) It is multilinear, and on a Boolean β∈0,1logBβ∈\0,1\ B it equals 22 raised to the integer value of the bit string β (with β1 _1 the least significant bit). These are exactly the coefficients that decode an integer from its binary expansion: ∑β∈0,1logB(β)aβ _β∈\0,1\ B vec2int(β)a_β is the integer with bits (aβ)β(a_β)_β. The Verifier can compute (β^) vec2int( β) in O(logB)O( B) field operations at any β^∈logB β B. weight: For an oracle A:logm+logB→A m+ B and j∈logmj m, write A(j)≔∑β∈0,1logB(β)⋅A(j,β), weight^A(j) _β∈\0,1\ B vec2int(β)· A(j,β), (12) the integer that vec2int decodes from the bits A stores in its j-th row. On a codeword, A holds the weight bits, so A(j)=αj† weight^A(j)=α _j is the integer weight numerator of the j-th support point and A(j)/2B=μ[zj] weight^A(j)/2^B=μ[z_j] its probability mass; for an arbitrary multilinear A it is the same F-linear combination of the rows A(⋅,β)A(·,β), hence multilinear in j. agree: Fix an oracle Z:logm+logn→Z m+ n , points s=(s1,…,sℓ)s=(s_1,…,s_ ) with sk∈logns_k n, and bits b=(b1,…,bℓ)∈ℓb=(b_1,…,b_ ) . For j∈logmj m, b,sZ(j)≔∏k=1ℓbkZ(j,sk)+(1−bk)(1−Z(j,sk)). agree^Z_b,s(j) _k=1 b_kZ(j,s_k)+(1-b_k)(1-Z(j,s_k)). (13) Each factor is the equality indicator between the bit bkb_k and the value Z(j,sk)Z(j,s_k), so b,sZ(j) agree^Z_b,s(j) is just eq of the bit-vector b against the slice-values (Z(j,sk))k=1ℓ(Z(j,s_k))_k=1 : b,sZ(j)=(b,(Z(j,sk))k=1ℓ). agree^Z_b,s(j)= eq(b,(Z(j,s_k))_k=1 ). For multilinear Z the map j↦b,sZ(j)j agree^Z_b,s(j) has individual degree at most ℓ in j, and on a codeword it indicates, at Boolean j, whether the j-th support point satisfies every context literal zj,sk=bkz_j,s_k=b_k. 7.2 Verifying proximity to the code Proximity is measured in relative Hamming distance: for functions f,g:k→f,g ^k , dist(f,g)≔Prx∼k[f(x)≠g(x)]dist(f,g) _x ^k[f(x)≠ g(x)] is the fraction of inputs on which they disagree, and f is δ-far from a set of functions if dist(f,g)≥δdist(f,g)≥δ for every g in the set (otherwise δ-close to it). For the pairs at hand, the worst part governs: the distance between (Z,A)(Z,A) and a codeword (Z~,A~)( Z, A) is maxdist(Z,Z~),dist(A,A~) \dist(Z, Z),dist(A, A)\. Algorithm 3 tests that a pair of oracles (Z,A)(Z,A) is close to a valid codeword: that both Z and A are multilinear, that each is Boolean on the hypercube, and that the masses A encodes sum to one. Fact 23 (BFL 91; FGL+ 96). Let f:k→f ^k . Consider a tester as follows: (1) Sample i∈[k]i∈[k] uniformly at random; (2) Sample three points x,y,z∈kx,y,z ^k that differ only on the iith coordinate, uniformly at random; (3) Accept if and only if f(x),f(y),f(z)f(x),f(y),f(z) agree with an i-linear function. Then, for any δ∈(0,1)δ∈(0,1) such that 6k/||<δ<1/26k/|F|<δ<1/2, 1. Completeness: If f is multilinear, the tester accepts with probability 11. 2. Soundness: If f is δ-far from multilinear in relative Hamming distance, the tester accepts with probability at most 1−δ/k1-δ/k. We note that although FGL+ 96 state the soundness of their tester only for δ≥0.1δ≥ 0.1, 23 follows immediately from their intermediate argument in Lemma 4.3.1.3. Namely, their lemma guarantees rejection with probability at least 3(1−δ)δ/k−3/||3(1-δ)δ/k-3/|F|. We then use the additional assumptions made in 23 to obtain 3(1−δ)δk−3||≥3δ2k−3||≥3δ2k−δ2k=δk, 3(1-δ)δk- 3|F|≥ 3δ2k- 3|F|≥ 3δ2k- δ2k= δk, using first the assumption that δ<1/2δ<1/2, then the assumption that 6k/||<δ6k/|F|<δ. Input: Finite field F, a proximity parameter δ∈(0,1)δ∈(0,1), and a soundness parameter ε∈(0,1) ∈(0,1). Oracle access to Z:logm+logn→Z m+ n and A:logm+logB→A m+ B for n,m,B∈ℕn,m,B . Repeat the multilinearity test of 23 ⌈(logm+logn)maxln(1/ε)/δ, 2/ε⌉ ( m+ n) \ (1/ )/δ,\ 2/ \ times on oracle Z, and ⌈(logm+logB)maxln(1/ε)/δ, 2/ε⌉ ( m+ B) \ (1/ )/δ,\ 2/ \ times on oracle A. Reject if any test rejects. 1 Sample a random y′∈logm+logny m+ n and send it to the Prover. Run (v^,y^)≔(val←0,rounds←logm+logn,deg←3)( v, y) SumCheck_F( val← 0, rounds← m+ n, deg← 3) Assert that v^=?(Z2(y^)−Z(y^))⋅(y^,y′). v ?= (Z^2( y)-Z( y) )· eq( y,y ). (14) 2 Sample a random x′∈logm+logBx m+ B and send it to the Prover. Run (u^,x^)≔(val←0,rounds←logm+logB,deg←3)( u, x) SumCheck_F( val← 0, rounds← m+ B, deg← 3) Assert that u^=?(A2(x^)−A(x^))⋅(x^,x′). u ?= (A^2( x)-A( x) )· eq( x,x ). (15) 3 Run (w^,(j^,β^))≔(val←2B,rounds←logm+logB,deg←2) ( w,( j, β) ) SumCheck_F( val← 2^B, rounds← m+ B, deg← 2); here we mean that w^∈ w is the first output, and (j^,β^)( j, β) is the second output, with j^∈logm j m and β^∈logB β B. Assert that w^=?A(j^,β^)⋅(β^). w ?=A( j, β)· vec2int( β). (16) 4 If any assertion failed, reject. Otherwise, accept. Algorithm 3 Z,A(δ,ε) VerEnc_F^Z,A(δ, ) Claim 24. Suppose F is a prime field with 2B<||2^B<|F|, and Z,A(δ,ε) VerEnc_F^Z,A(δ, ) is run on Z:logm+logn→Z m+ n and A:logm+logB→A m+ B such that m⋅(2B−1)<||,6⋅logm+max(logn,logB)||<δ<12,10⋅logm+max(logn,logB)||≤εm·(2^B-1)<|F|, 6· m+ ( n, B)|F|<δ< 12, 10· m+ ( n, B)|F|≤ (17) Then, • Completeness: If (Z,A)∈μ(n,m,B)(Z,A)∈ R _F(n,m,B), there exists an honest Prover such that the Verifier accepts with probability 1. • Soundness: If min(Z~,A~)∈μ(n,m,B)maxdist(Z,Z~),dist(A,A~)≥δ, _( Z, A)∈ R _F(n,m,B) \dist(Z, Z),dist(A, A)\≥δ, then the Verifier accepts with probability at most ε . Furthermore, the Verifier runs in O((logm+logn+logB)maxlog(1/ε)/δ, 1/ε)O (( m+ n+ B) \ (1/ )/δ,\ 1/ \ ) field operations. Proof. At a high level, the Verifier tests that Z and A are close to multilinear (amplifying this test, by repetition, to soundness ε ), and then SumChecks that each is Boolean on the hypercube (Equations 14 and 15) and that the masses encoded by A sum to one (Equation 16). The three SumChecks are sound by the assumption on the field size, namely, ||≥Ω((logm+max(logn,logB))/ε)|F|≥ (( m+ ( n, B))/ ). We will first show that Equations 14, 15 and 16 establish completeness and soundness under the assumption that Z and A were multilinear, and remove this assumption in the end. Rather than separating completeness and soundness, we will show that each check of the Verifier asserts a necessary property of μ R , and that if all properties are met then (Z,A)∈μ(Z,A)∈ R . Booleanity of a multilinear Z. For any fixed y′∈logm+logny m+ n, consider the polynomial Gy′(y)=(Z2(y)−Z(y))⋅(y,y′).G_y (y)= (Z^2(y)-Z(y) )· eq(y,y ). It is a (logm+logn)( m+ n)-variate polynomial. By Z’s assumed multilinearity, Gy′G_y has individual degree at most 33. Finally, if Z was Boolean on 0,1log(m)+logn\0,1\ (m)+ n then for Boolean-entry y, Z2(y)=Z(y)Z^2(y)=Z(y), therefore for all y′∈logm+logny m+ n ∑y∈0,1logm+logn(Z2(y)−Z(y))(y,y′)=∑y∈0,1logm+logn0⋅(y,y′)=0 _y∈\0,1\ m+ n(Z^2(y)-Z(y)) eq(y,y )= _y∈\0,1\ m+ n0· eq(y,y )=0 Therefore, 22 applied to (0,logm+logn,3) SumCheck(0, m+ n,3) implies that Equation 14 is satisfied with probability 1 if the Prover participates honestly in the protocol. For soundness, suppose that Z is not Boolean on the hypercube. Then there exists y∗∈0,1logm+logny ∈\0,1\ m+ n such that Z2(y∗)−Z(y∗)≠0Z^2(y^*)-Z(y^*)≠ 0. Consider the polynomial F(y′)≔∑y∈0,1logm+logn(Z2(y)−Z(y))(y,y′).F(y ) _y∈\0,1\ m+ n(Z^2(y)-Z(y)) eq(y,y ). We have F(y∗)=Z2(y∗)−Z(y∗)≠0F(y^*)=Z^2(y^*)-Z(y^*)≠ 0, and F has total degree at most logm+logn m+ n, therefore, by the Schwartz–Zippel lemma Sch 80; Zip 79, Pry′∼logm+logn[F(y′)=0]≤logm+logn||. _y m+ n [F(y )=0 ]≤ m+ n|F|. Assuming F(y′)≠0F(y )≠ 0 for the y′y sampled and sent by Verifier, by soundness of SumCheck, the Verifier accepts with probability at most 3⋅(logm+logn)/||3·( m+ n)/|F|. Combining with a union bound, we have that the Verifier accepts Equation 14 with probability at most logm+logn||+3(logm+logn)||=4(logm+logn)||≤25ε, m+ n|F|+ 3( m+ n)|F|= 4( m+ n)|F|≤ 25 , where the last inequality uses 10(logm+logn)/||≤ε10( m+ n)/|F|≤ from Equation 17. Booleanity of a multilinear A. By an identical argument, we have that if A was Boolean on the hypercube then Equation 15 is satisfied with probability 11; else, Equation 15 is satisfied with probability at most 4(logm+logB)/||≤25ε4( m+ B)/|F|≤ 25 . Unit measure of a multilinear A. Assume that A was Boolean on its hypercube (otherwise, see previous case). The argument is similar to the previous one, but simpler, with vec2int (Equation 11) decoding the weight numerators from the bits stored in A. Suppose A encodes probabilities that sum to 1; that is, letting αj†=∑β(β)A(j,β) _j = _β vec2int(β)A(j,β), the assumption is that ∑jαj†=2B _j _j =2^B. Then, ∑j∈0,1logmβ∈0,1logBA(j,β)⋅(β)=∑j∈0,1logmαj†=2B. _ subarraycj∈\0,1\ m\\ β∈\0,1\ B subarrayA(j,β)· vec2int(β)= _j∈\0,1\ mα _j=2^B. The summand on the left hand side above has individual degree at most 22. Thus, 22 applied to (2B,logm+logB,2) SumCheck(2^B, m+ B,2) implies that an honest Prover convinces the Verifier with probability 1. For soundness, suppose A was Boolean on the hypercube but did not have unit measure, ∑j,βA(j,β)(β)≠2B _j,βA(j,β) vec2int(β)≠ 2^B over ℤZ. We claim the inequality holds over F as well; indeed, by Booleanity of A, the following holds over ℤZ, 0≤∑j∈0,1logmβ∈0,1logBA(j,β)(β)≤2logm∑β∈0,1logB(β)=m(2B−1)<||.0≤ _ subarraycj∈\0,1\ m\\ β∈\0,1\ B subarrayA(j,β) vec2int(β)≤ 2 m _β∈\0,1\ B vec2int(β)=m(2^B-1)<|F|. Therefore, 22 implies that Equation 16 holds with probability at most 2(logm+logB)/||≤15ε2( m+ B)/|F|≤ 15 , again by 10(logm+logB)/||≤ε10( m+ B)/|F|≤ of Equation 17. Non-multilinear Z and A. We now remove the assumption that Z and A are multilinear. Let Z~,A~ Z, A be the multilinear polynomials closest to Z,AZ,A, at relative Hamming distances δZ≔dist(Z,Z~) _Z (Z, Z) and δA≔dist(A,A~) _A (A, A), and write R≔⌈(logm+logn)maxln(1/ε)/δ,2/ε⌉R ( m+ n) \ (1/ )/δ,2/ \ for the number of multilinearity repetitions on Z (the count for A is analogous). We are in the soundness case, meaning that (Z,A)(Z,A) is δ-far from every codeword; therefore at least one of the next two situations holds: (i) Z or A is δ-far from multilinear. Say δZ≥δ _Z≥δ, so Z is in particular δ-far from multilinear. Since 6(logm+logn)/||<δ<1/26( m+ n)/|F|<δ<1/2, 23 applies at proximity δ, and each of the R multilinearity tests on Z accepts with probability at most 1−δ/(logm+logn)1-δ/( m+ n); hence they all accept with probability at most (1−δlogm+logn)R≤e−Rδ/(logm+logn)≤e−ln(1/ε)=ε, (1- δ m+ n )^R≤ e^-Rδ/( m+ n)≤ e^- (1/ )= , using R≥(logm+logn)ln(1/ε)/δR≥( m+ n) (1/ )/δ. (i) Both Z and A are δ-close to multilinear, but (Z~,A~)∉μ( Z, A)∉ R . Here δZ,δA<δ _Z, _A<δ, yet Z~ Z or A~ A is non-Boolean, or A~ A is not of unit measure—otherwise (Z,A)(Z,A) would be δ-close to the codeword (Z~,A~)( Z, A), contrary to assumption. We treat the case that Z~ Z is non-Boolean—the other two failures are handled identically by Equations 15 and 16. By the multilinear case above applied to Z~ Z, together with the at-most-δZ _Z chance that the marginally-uniform query into Z for Equation 14 lands where Z≠Z~Z≠ Z, Equation 14 accepts with probability at most 4(logm+logn)/||+δZ4( m+ n)/|F|+ _Z; we split on whether the multilinearity test can see the defect. If δZ≤6(logm+logn)/|| _Z≤ 6( m+ n)/|F|, then Z is below the detection threshold of 23, but Equation 14 alone already suffices: Pr[accept]≤4(logm+logn)||+δZ≤10(logm+logn)||≤ε, [accept]≤ 4( m+ n)|F|+ _Z≤ 10( m+ n)|F|≤ , by Equation 17. Otherwise 6(logm+logn)/||<δZ<δ<1/26( m+ n)/|F|< _Z<δ<1/2, so 23 applies at proximity δZ _Z and the multilinearity test on Z accepts with probability at most (1−δZ/(logm+logn))R≤e−2δZ/ε(1- _Z/( m+ n))^R≤ e^-2 _Z/ , using R≥2(logm+logn)/εR≥ 2( m+ n)/ . Acceptance requires both this test and Equation 14 to pass, on independent randomness, so multiplying and using 4(logm+logn)/||≤25ε4( m+ n)/|F|≤ 25 , Pr[accept]≤e−2δZ/ε(25ε+δZ)=25εe−2δZ/ε+δZe−2δZ/ε≤25ε+ε2e<ε, [accept]≤ e^-2 _Z/ ( 25 + _Z )= 25 e^-2 _Z/ + _Ze^-2 _Z/ ≤ 25 + 2e< , using e−2δZ/ε≤1e^-2 _Z/ ≤ 1 for the first term and maxx≥0xe−2x/ε=ε/(2e) _x≥ 0xe^-2x/ = /(2e) (attained at x=ε/2x= /2) for the second. In every situation the Verifier accepts with probability at most ε , which is the soundness claim. ∎ Remark 25. The field size ||≥m2B|F|≥ m2^B is needed only for the unit-measure check, where the sum-check on Equation 16 verifies the integer identity ∑jαj†=2B _j _j =2^B and the partial sums, which can reach m(2B−1)m(2^B-1), must not wrap around in F. It could be avoided in an IP, by fingerprinting Fre 77: have the Verifier issue a random prime p of size (B,n,logm) poly(B,n, m) and check the identity modulo p. However, the field F is then determined only during the protocol’s runtime, thereby losing the clean conceptual cut of having a distribution encoded as (Z,A)(Z,A). We prefer the cleaner presentation. On a technical level, our full protocol (Algorithm 6) pays an exponential field size regardless, so the saving would not help our overarching goal. 7.3 Verifying a succinctly-specified marginal We give two protocols. The first, VerMarginoid (Algorithm 4), is the one our main construction (the IPCP of Section 8.2) actually calls. It runs on multilinear oracles and verifies ∑jA(j)b,sZ(j) _j weight^A(j) agree^Z_b,s(j) over F for a given b,sb,s. We call this a marginoid rather than a marginal because its context is specified over F: the variable descriptions s1,…,sℓ∈logns_1,…,s_ n and the truth values b1,…,bℓ∈b_1,…,b_ range over the field, so the pair (s,b)(s,b) need not describe any actual event ωsk=bkk\ _s_k=b_k\_k. When s and b are Boolean and (Z,A)(Z,A) is a codeword the marginoid is a genuine marginal mass; in general it is only the marginal-shaped algebraic value that the sum-check manipulates. This is all that Section 8.2 needs. For completeness, and because it may be of independent interest, we then package VerMarginoid into the self-contained primitive VerMarginal (Algorithm 5). It verifies a genuine marginal up to tolerance τ using self-correction: recovering the value of the nearby codeword at a point by querying the given (possibly corrupted) oracle at correlated random points (27). It will not be used downstream in this paper, however. Input: Finite field F, v,b1,…,bℓ∈v,b_1,…,b_ , and s1,…,sℓ∈logns_1,…,s_ n. Oracle access to Z:logm+logn→Z m+ n and A:logm+logB→A m+ B . Run (v^,j^)≔(val←v,rounds←logm,deg←ℓ+1)( v, j) SumCheck_F( val← v, rounds← m, deg← +1) 1 Expect w∈w to be sent from the Prover. Run (w^,β^)≔(val←w,rounds←logB,deg←2)( w, β) SumCheck_F( val← w, rounds← B, deg← 2) 2 Accept if and only if w w =?(β^)⋅A(j^,β^),and ?= vec2int( β)· A( j, β),\ and (18) v v =?w⋅b,sZ(j^). ?=w· agree^Z_b,s( j). (19) Algorithm 4 Z,A(v,s1,b1,…,sℓ,bℓ) VerMarginoid_F^Z,A(v,s_1,b_1,…,s_ ,b_ ) Claim 26. Fix a finite field F, v,b1,…,bℓ∈v,b_1,…,b_ , and s1,…,sℓ∈logns_1,…,s_ n, and suppose VerMarginoid is run with multilinear oracles Z:logm+logn→Z m+ n and A:logm+logB→A m+ B . Recall the gadgets vec2int and b,sZ(j) agree^Z_b,s(j) from Equations 11 and 13. • Completeness: There exists an honest Prover such that if v=∑j∈0,1logmβ∈0,1logB(β)A(j,β)b,sZ(j)v= _ subarraycj∈\0,1\ m\\ β∈\0,1\ B subarray vec2int(β)A(j,β) agree^Z_b,s(j) (20) then the Verifier accepts with probability 1. • Soundness: If Equation 20 does not hold then regardless of the Prover’s messages, the Verifier accepts with probability at most ((ℓ+1)logm+2logB)/||(( +1) m+2 B)/|F|. Furthermore, the Verifier runs in O((ℓ+1)logm+logB)O(( +1) m+ B) field operations, makes ℓ queries to Z and one query to A. The query to A is marginally uniform on logm+logBF m+ B, and each query to Z is marginally uniform in its first logm m coordinates. Proof. We use the shorthand A(j^)=∑β(β)A(j^,β) weight^A( j)= _β vec2int(β)A( j,β) throughout this proof (see Equation 12) At a high level, the first SumCheck reduces the claimed value v to the evaluation A(j^)b,sZ(j^) weight^A( j) agree^Z_b,s( j) at a random j j, and the second reduces the Prover’s alleged value of A(j^) weight^A( j) to a single query to A. We first record the degrees of the two summands, then prove completeness and soundness. Degrees of the two summands. Denote φ(j)≔A(j)b,sZ(j)andψj^(β)≔(β)A(j^,β). (j) weight^A(j) agree^Z_b,s(j) _ j(β) vec2int(β)A( j,β). Because Z is multilinear, for each fixed sks_k the map j↦Z(j,sk)j Z(j,s_k) is multilinear. Therefore, each factor bkZ(j,sk)+(1−bk)(1−Z(j,sk))b_kZ(j,s_k)+(1-b_k)(1-Z(j,s_k)) has individual degree 11 in each coordinate of j, and their product b,sZ(j) agree^Z_b,s(j) has individual degree at most ℓ . Since A weight^A is multilinear in j (Equation 12), the product φ(∙)=A(∙)⋅b,sZ(∙) ( )= weight^A( )· agree^Z_b,s( ) has individual degree at most ℓ+1 +1 in each of its logm m variables. As for ψj _ j: (β)=∏k=1logB(1+βk(22k−1−1)) vec2int(β)= _k=1 B(1+ _k(2^2^k-1-1)) is multilinear in β, and so is A(j^,β)A( j,β) for fixed j j, so ψj _ j has individual degree at most 22 in each of its logB B variables. These are the degree parameters passed to the two invocations of Algorithm 2. Completeness. Assume Equation 20; that is, v=∑j∈0,1logmφ(j)v= _j∈\0,1\ m (j). Run the honest 22 Prover for φ in the first SumCheck (its individual degree is at most ℓ+1 +1, as required); by completeness of 22, v^=φ(j^)=A(j^)b,sZ(j^) v= ( j)= weight^A( j) agree^Z_b,s( j) with probability 11. Next, let the Prover send w≔A(j^)=∑β∈0,1logBψj^(β)w weight^A( j)= _β∈\0,1\ B _ j(β) and answer honestly as per 22 for ψj _ j in the second SumCheck; then w^=ψj^(β^)=(β^)A(j^,β^) w= _ j( β)= vec2int( β)A( j, β) with probability 11, so Equation 18 holds. Finally, v^=A(j^)b,sZ(j^)=w⋅b,sZ(j^) v= weight^A( j) agree^Z_b,s( j)=w· agree^Z_b,s( j), so Equation 19 holds as well, and the Verifier accepts with probability 11. Soundness. Suppose Equation 20 fails; that is, v≠∑j∈0,1logmφ(j)v≠ _j∈\0,1\ m (j). Fix any Prover, and distinguish two events according to the value w it sends: either the Verifier accepts and w=A(j^)w= weight^A( j), or the Verifier accepts and w≠A(j^)w≠ weight^A( j). Suppose the Verifier accepts and w=A(j^)w= weight^A( j). Then Equation 19 is v^=wb,sZ(j^)=A(j^)b,sZ(j^)=φ(j^) v=w agree^Z_b,s( j)= weight^A( j) agree^Z_b,s( j)= ( j). Since v≠∑jφ(j)v≠ _j (j), by soundness of the first SumCheck, the Verifier accepts with probability at most (ℓ+1)logm/||( +1) m/|F|. Now suppose w≠A(j^)w≠ weight^A( j). Then w≠∑βψj^(β)w≠ _β _ j(β), so by soundness of the second SumCheck, Equation 18 holds with probability at most 2logB/||2 B/|F|. By a union bound, the Verifier accepts with probability at most (ℓ+1)logm+2logB||. ( +1) m+2 B|F|. Complexity and smoothness. 1414 14 Smoothness KT 00, i.e. that the Verifier’s oracle queries are (marginally) uniformly distributed over the proof, is a well-studied property of PCPs Par 21; AC 25; BHPT 24; we rely on it repeatedly, as it drives both the self-correction of 27 and the passage from the oracle to a nearby codeword in the soundness proof of Theorem 32. Both follow from 22. The two SumChecks cost O((ℓ+1)logm)O(( +1) m) and O(logB)O( B) field operations, and their outputs j^,β j, β are marginally uniform. To evaluate Equation 19, the Verifier computes b,sZ(j^) agree^Z_b,s( j) directly via the ℓ queries Z(j^,sk)Z( j,s_k); to evaluate Equation 18, it computes (β^) vec2int( β) directly and makes the single query A(j^,β^)A( j, β). ∎ We now package VerMarginoid as the standalone primitive VerMarginal. Given oracles (Z,A)(Z,A) close to a codeword for a distribution μ, it certifies that an alleged value v agrees, within a tolerance τ, with the true marginal mass of a context—the denominator-cleared probability 2Bμ[s1,b1,…,sℓ,bℓ]2^Bμ[s_1,b_1,…,s_ ,b_ ]. The Prover commits to that mass, the Verifier checks it against v by an integer comparison exactly as the tolerance test of VerConsist (Algorithm 6), and the commitment is certified by running VerMarginoid on the self-corrected oracle. Fact 27 (BLR 90). Fix a field F, k≤||−2k≤|F|-2, and f:k→f ^k . Consider the following procedure f(x) SelfCorrect_F^f(x) for input x∈kx ^k: 1. Sample r∈kr ^k uniformly at random. 2. Query f(x+r),f(x+2r),…,f(x+(k+1)r)f(x+r),f(x+2r),…,f(x+(k+1)r). 3. Compute g:→g the unique polynomial of degree at most k such that g(i)=f(x+ir)g(i)=f(x+ir) for all i∈[k+1]i∈[k+1]. 4. Output g(0)g(0). For any δ∈(0,1)δ∈(0,1), if f is δ-close to a multilinear f~:k→ f ^k , then f(x) SelfCorrect_F^f(x) outputs f~(x) f(x) with probability at least 1−(k+1)δ1-(k+1)δ. SelfCorrect makes k+1k+1 marginally uniform queries to f, and runs in time O(k2)O(k^2) field operations.1515 15 More precisely, given precomputed interpolation weights, the running time is O(k)O(k) scalar field operations plus O(k)O(k) vector additions. Input: Finite field F, an alleged value v∈v , a context s1,…,sℓ∈[n]s_1,…,s_ ∈[n] with bits b1,…,bℓ∈0,1b_1,…,b_ ∈\0,1\, and a tolerance τ=τ†/2Bτ=τ /2^B given to precision B by an integer numerator τ†∈0,…,2Bτ ∈\0,…,2^B\. Oracle access to Z:logm+logn→Z m+ n and A:logm+logB→A m+ B that are δ-close to a codeword. Expect v∗∈v from the Prover. Treating v∗v and v as integers in 0,…,||−1\0,…,|F|-1\, reject unless, |v∗−v|<τ†over ℤ. |v -v |<τ $ Z$. (21) 1 Run Z,A(v∗,s1,b1,…,sℓ,bℓ) VerMarginoid_F^Z,A(v ,s_1,b_1,…,s_ ,b_ ), replacing each query Z(j^,sk)Z( j,s_k) with Z(j^,sk) SelfCorrect_F^Z( j,s_k) (27). Accept if and only if it accepts. Algorithm 5 Z,A(v,s1,b1,…,sℓ,bℓ,τ) VerMarginal^Z,A(v,s_1,b_1,…,s_ ,b_ ,τ) In fact, only the sks_k argument to Z needs to be self-corrected, but we self-correct the entire query Z(j^,sk)Z( j,s_k) for simplicity of notation. Corollary 28 (Marginal certification within a tolerance). Fix m,n,B∈ℕm,n,B and a prime field F with logm+logn≤||−2 m+ n≤|F|-2 and 2B<||2^B<|F|. Let π=(Z,A)π=(Z,A) be functions that are δ-close, in relative Hamming distance, to a codeword (Z~,A~)∈μ(n,m,B)( Z, A)∈ R _F(n,m,B) encoding a distribution μ over 0,1n\0,1\^n. Fix a context s1,…,sℓ∈[n]s_1,…,s_ ∈[n] with bits b1,…,bℓ∈0,1b_1,…,b_ ∈\0,1\, an alleged value v∈v , and a tolerance τ=τ†/2Bτ=τ /2^B with integer numerator τ†∈0,…,2Bτ ∈\0,…,2^B\. Then Z,A(v,s1,b1,…,sℓ,bℓ,τ) VerMarginal^Z,A(v,s_1,b_1,…,s_ ,b_ ,τ) satisfies: • Completeness: if π=(Z~,A~)π=( Z, A) is exactly the codeword and |μ[s1,b1,…,sℓ,bℓ]−v/2B|<τ|μ[s_1,b_1,…,s_ ,b_ ]-v/2^B|<τ, there is an honest Prover with which the Verifier accepts with probability 11. • Soundness: if |μ[s1,b1,…,sℓ,bℓ]−v/2B|≥τ|μ[s_1,b_1,…,s_ ,b_ ]-v/2^B|≥τ, then regardless of the Prover’s messages the Verifier accepts with probability O(ℓlogm+logB||+ℓ(logm+logn)δ).O\! ( m+ B|F|\;+\; ( m+ n)δ ). • Complexity: the Verifier makes O(ℓlogm+ℓlogn)O ( m+ n ) marginally-uniform queries to Z and one to A, exchanges O(ℓlogm+logB)O( m+ B) field elements with the Prover, and runs in O(ℓ(logm+logn)2+logB)O ( ( m+ n)^2+ B ) field operations, plus O(log||)O( |F|) bit operations for the integer comparison. Proof. Write μ†≔2Bμ[s1,b1,…,sℓ,bℓ]μ 2^Bμ[s_1,b_1,…,s_ ,b_ ]. Note that, for the μ R -encoding (Z~,A~)( Z, A) of μ, the value certified by 26 (the right-hand side of Equation 20) is ∑jA(j)b,sZ~(j)=∑j:∀kzj,sk=bkαj†=μ†, _j weight^A(j) agree Z_b,s(j)= _j:∀ k\ z_j,s_k=b_kα _j=μ , indeed A(j)=αj† weight^A(j)=α _j is the integer weight of zjz_j (Equation 12), and b,sZ~(j) agree Z_b,s(j) is the Boolean indicator that zj,sk=bkz_j,s_k=b_k for all k (Definitions 21 and 13). Because 0≤μ†≤2B<||0≤μ ≤ 2^B<|F|, the integer comparison Equation 21 against a Prover message claiming μ†μ is unambiguous. Completeness. The honest Prover sends v∗≔μ†v μ . Since |μ†−v|<τ†|μ -v|<τ , Equation 21 holds. On the exact codeword every SelfCorrect returns Z~(j^,sk) Z( j,s_k) with probability 11, so the second step is VerMarginoid on (Z~,A~)( Z, A) with claimed value v∗=μ†v =μ ; by 26 it accepts with probability 11. Soundness. Suppose |μ†−v|≥τ†|μ -v|≥τ and fix any Prover sending some v∗v as its message. If the Verifier accepts then Equation 21 holds, i.e., |v∗−v|<τ†|v -v|<τ . Then v∗≠μ†v ≠μ over F. The second step is therefore VerMarginoid run with claimed value v∗≠μ†v ≠μ and each Z-query self-corrected. By 27 (with k=logm+logn≤||−2k= m+ n≤|F|-2), each of the ℓ self-corrected queries returns Z~(j^,sk) Z( j,s_k) except with probability (logm+logn+1)δ( m+ n+1)δ, and the single A-query is marginally uniform on logm+logBF m+ B (26), agreeing with A~ A except with probability δ. Conditioned on all of these agreements, the run is then exactly VerMarginoid against the multilinear codeword (Z~,A~)( Z, A), whose true value is μ†μ . Since v∗≠μ†v ≠μ , Equation 20 fails and 26 bounds acceptance by ((ℓ+1)logm+2logB)/||(( +1) m+2 B)/|F|. Conclude with a union bound. Complexity. Each SelfCorrect makes logm+logn+1 m+ n+1 marginally-uniform queries and O((logm+logn)2)O(( m+ n)^2) field operations (27), and there are ℓ of them; the integer comparison Equation 21 costs O(log||)O( |F|) bit operations on the lifted representatives, and the remaining cost, including the O(ℓlogm+logB)O( m+ B) field elements of Prover communication, is that of 26. ∎ 8 Verifying consistency of predictive models The main contribution of this section is an explicit polynomial-time Interactive PCP ( IPCP) for - Model-Consistency: a protocol in which the Verifier is given an (alleged) μ R -encoding (Section 7) of a consistent distribution, and uses it to certify consistency of a given predictive model. We note the consequence we do not pursue: Corollary 18 composed with = MIP= NEXP BFL 91 gives that - Model-Consistency admits a MIP, namely, polynomial-time Verifier interacting with two provers.1616 16 Equivalently, a polynomial time Verifier querying an exponential length PCP. We stick with the MIP strawman, but our informal argument would apply to a PCP just the same. One could then hope to augment the training of (P,Q)(P,Q) with the training of two Provers P1,P2P_1,P_2 towards a predictive model that proves its own consistency (see Remark 1). The practical obstacle to such a programme is not (only) the cost of running P1,P2P_1,P_2: they may be worst-case exponential-time, but perhaps more efficient on average and may even be trained for average success by Reinforcement Learning from Verifier Feedback (RLVF) or Transcript Learning (TL) AGPR 25. However, before one trains an honest Prover by RLVF (resp. TL), one needs an implementation of the Verifier (resp. honest Prover) to learn against: code that, on input the witnessing distribution μ underlying (P,Q)(P,Q)’s consistency, produces the messages an honest P1,P2P_1,P_2 would send. Attempting to follow the rationale of Corollary 18, this code is the composition of two generic constructions. The first is the Cook–Levin Coo 71; Lev 73 reduction of (P,Q,τ,V)(P,Q,τ,V_ NEXP) into a succinct CNF formula, which discards the convex-geometric semantics of the Carathéodory witness. The second is the BFLS honest Prover strategy BFLS 91 which runs on top of the succinct CNF. The IPCP we construct in this section is designed towards clearing this obstacle by explicitly describing the Verifier and honest Prover. Namely, the proof oracle is the μ R -encoding of the witnessing distribution, and the SumChecks that reduce the inconsistency inequality to queries on that oracle admit an arguably self-contained, implementable specification (Algorithm 6). We reflect in Section 9 on what was natural about the resulting protocol: how it factors into a model-specific “witness” core and a model-agnostic “proving” overlay, which we hope opens a route to training self-proving predictive models in the spirit of AGPR 25. Definition 29 (Interactive PCP KR 08). An Interactive PCP ( IPCP) is an interactive proof in which the Verifier additionally has oracle access to a proof string π fixed before the interaction begins (the PCP). It is measured by the Verifier runtime; the PCP length, the number of symbols of π; the query complexity, the number of point queries the Verifier makes to π; and the communication exchanged with the Prover. Importantly, the oracle cannot adapt to the interaction, whereas the Prover can; this is what separates an IPCP from an interactive proof, and since a proof oracle is equivalent to non-communicating provers FRS 94, an IPCP is a special case of a multi-prover proof. As elsewhere, we specify only the Verifier, and describe the honest Prover and proof string when proving completeness. 8.1 Setup: from a witnessing distribution to the proof oracle Fix a predictive model (P,Q)(P,Q) with variable description length d, context length ℓ , and precision B. We write n≔2dn 2^d for the number of (implicit) Boolean variables, and recall that P’s probability denominator is 2B2^B. For readability, we omit the subscript from I(P,Q) _(P,Q), writing simply I for the model inconsistency. Queries. Recall from Section 4.2 that a query is a string q=(s1,b1,…,sℓ,bℓ,t)∈q=(s_1,b_1,…,s_ ,b_ ,t) , with ≔0,1ℓ(d+1)+dQ \0,1\ (d+1)+d the query universe, sk∈0,1ds_k∈\0,1\^d the description of the kkth context variable, bk∈0,1b_k∈\0,1\ the corresponding context bit, and t∈0,1dt∈\0,1\^d the target-variable description. For example, q=(s1,0,s5,1,t)q=(s_1,0,s_5,1,t) is asking for the probability that the variable ωt _t is true conditioned on ωs1=0 _s_1=0 and ωs5=1 _s_5=1. We abbreviate ‖Q‖≔‖Q‖1=∑q∈Q(q)\|Q\| \|Q\|_1= _q Q(q), the number of (confidence-weighted) claims implicit in (P,Q)(P,Q); note that ‖Q‖1≤||⋅2B∈2O(ℓd+B)\|Q\|_1≤|Q|· 2^B∈ 2^O( d+B). We now describe what the Prover of a consistent model must do to come up with the proof oracle: find a distribution μ⋆μ consistent with the model (P,Q)(P,Q), sparsify it, and encode the sparse result. Step 1: find any witnessing distribution. Suppose (P,Q)(P,Q) is (τ−εgap)(τ- _ gap)-consistent for some gap εgap>0 _ gap>0: by definition, there is some distribution μ⋆μ over 0,1n\0,1\^n with I(P,Q)(μ⋆)≤τ−εgap _(P,Q)(μ )≤τ- _ gap. Nothing more is assumed of μ⋆μ ; its support may well be all of 0,1n\0,1\^n. Step 2: sparsify. By the Carathéodory step of Section 5 applied to the implicit CPC P,QP_P,Q (Definitions 6 and 7), in the low-precision explicit form of Proposition 8 (gap εgap _ gap), the witness μ⋆μ can be traded for a sparse distribution μz,α _z,α with • support vectors z1,…,zm∈0,1nz_1,…,z_m∈\0,1\^n, with m=‖Q‖1+1m=\|Q\|_1+1, 1717 17 Proposition 8 gives a support of at most this size, and Definition 21 permits the zero-weight padding. We assume, here and throughout, that ‖Q‖1+1\|Q\|_1+1 is a power of two, so that logm m is an integer as Definition 21 requires; the decoupled variant described in Remark 31 removes this assumption. and • weights αj=αj†/2B′ _j=α _j/2^B for integers αj†∈0,…,2B′−1α _j∈\0,…,2^B -1\ with ∑j=1mαj†=2B′ _j=1^mα _j=2^B , where the denominator’s bit-length B′B is the certificate precision BεgapB_ _ gap of Proposition 8 at this m, rounded up to a power of two as Definition 21 requires, so that B′∈O(log‖Q‖+log(1/εgap))⊆O(ℓd+B+log(1/εgap))B ∈ O( \|Q\|+ (1/ _ gap)) O( d+B+ (1/ _ gap)),1818 18 Proposition 8 also permits αj†=2Bεgapα _j=2^B_ _ gap, a point mass, which the range above excludes. Such a witness is brought into range by duplicating its support vector. • such that IP,Q(μz,α)≤τ _P_P,Q( _z,α)≤τ. The sparsification costs the additive εgap _ gap slack in completeness. Throughout the rest of this section we work exclusively with the low-precision witness; Remark 36 explains why the exact witness of Lemma 13 is not used here. Step 3: encode. The Prover encodes μ using μ(n,m,B′) R _F(n,m,B ), for sufficiently large field F. Namely, the proof oracle is the codeword π=(Z,A)π=(Z,A), where as in Definition 21, Z is the multilinear extension of the support-vector table (j,i)↦zj,i(j,i) z_j,i and A that of the weight-bit table (j,β)↦(αj†)β(j,β) (α _j)_β. From this point onward π=(Z,A)π=(Z,A) denotes an alleged μ(n,m,B′) R _F(n,m,B )-codeword—a pair of functions over F of the types prescribed by Definition 21. The predictive model (P,Q)(P,Q) is given as a pair of circuits taking an input query q given as a bit-string. The Verifier in our protocol will eventually want to compute the outputs of these circuits on F-valued queroids q q; this is done by arithmetizing each circuit, i.e., deriving polynomials P^,Q P, Q by replacing Boolean gates by their arithmetic form over F: negation is replaced by a↦1−a 1-a, conjunction by (a,b)↦ab(a,b) ab, and disjunction by (a,b)↦a+b−ab(a,b) a+b-ab. Fact 30 (Naive). Let C be a Boolean circuit with n inputs and S many gates, computing a function 0,1n→0,…,M−1\0,1\^n→\0,…,M-1\ with M<||M<|F|. The polynomial C^∈[X1,…,Xn] C [X_1,…,X_n] is obtained by replacing each Boolean gate with its arithmetic form over F. Then, for any Boolean input x∈0,1nx∈\0,1\^n, C^(x)=C(x) C(x)=C(x), and for any x^∈n x ^n, C^(x^) C( x) is computable in O(S)O(S) field operations. We let P^,Q P, Q denote the polynomials obtained by this naive arithmetization, and let Δ denote an upper bound on their degrees (a scalar, not to be confused with the simplex ΔX X, which always takes a set argument). The protocol presented in this section costs linearly in Δ , which is itself exponential in the circuits’ depth in the worst case; Section 8.3 then shows how doubly-efficient interactive proofs GKR 15; Tha 13 replace the dependency on Δ by one on the depth, and improve the dependency on S. Parameter glossary. Denominators are written as explicit powers of two. We collect, for reference, all symbols used throughout the rest of Section 8: • d: variable description length, so that n≔2dn 2^d is the number of (implicit) Boolean variables. • ℓ : context length, the number of variables conditioned upon in each query. • B: precision of the model (P,Q)(P,Q), formally number of output gates of P and Q. • τ=τ†/2Bτ=τ /2^B: the consistency tolerance from - Model-Consistency, given to precision B with integer numerator τ†τ . • εgap>0 _ gap>0: the slack parameter from the gap variant of - Model-Consistency. • ≔0,1ℓ(d+1)+dQ \0,1\ (d+1)+d: the query universe; each q∈q is parsed as q=(s1,b1,…,sℓ,bℓ,t)q=(s_1,b_1,…,s_ ,b_ ,t). • ‖Q‖1\|Q\|_1: the number of (multiplicity-weighted) claims implicit in (P,Q)(P,Q).1919 19 We may omit the subscript 11 for readability • m=‖Q‖1+1m=\|Q\|_1+1: support size of the sparsified witness. • P,QP_P,Q: the implicit CPC of (P,Q)(P,Q), as defined in Definition 6. • B′B : bit-length of the weights of the sparsified witnessing distribution. • F: the finite field over which all arithmetic and oracles are evaluated; specified in Section 8.2. • π=(Z,A)π=(Z,A): the proof oracle, i.e., the PCP component of the IPCP. With Z:logm×d→Z m×F^d and A:logm×logB′→A m×F B . Remark 31 (Support size m and the length of the proof π). The honest oracle has length m=‖Q‖1+1m=\|Q\|_1+1, the length parameter of the codeword μ(n,m,B′) R _F(n,m,B ), fixed the moment π is given. The Verifier cannot compute ‖Q‖1=∑qQ(q)\|Q\|_1= _qQ(q) on its own (it is a sum over all of Q), but it can read m off π’s type signature, recover ‖Q‖1=m−1\|Q\|_1=m-1, and reject out of hand any oracle whose declared length exceeds the a-priori cap m≤2B||+1m≤ 2^B|Q|+1. The honest length thus depends on the particular input, through ‖Q‖1\|Q\|_1, not only on the input length. Instance-dependent proof length is common in the literature: e.g., the IPCP oracle of KR 08 is polynomial in the witness size, and the interactive oracle proofs of R 24 are made to approach the witness length. The instance-dependence may nonetheless be undesirable in our context, e.g., as it complicates preparing a uniform-length “batch” for feeding into a GPU; one regains uniformity by padding π up to the maximal length O(2ℓd)O(2 d) with further zero-weight dummy support vectors. We prefer the variable length for its granularity, and for the conceptual point it portrays: a more confident model, or one with more implicit claims (a larger ‖Q‖1\|Q\|_1 in either case), requires a longer proof. We also note that m=‖Q‖1+1m=\|Q\|_1+1 tracks the model’s total confidence rather than the true support size of the witness, which a resourceful Prover might make smaller still. A modest modification would enable this efficiency: Instead of identifying ‖Q‖1\|Q\|_1 with m−1m-1, the Verifier reads only the support size m off π’s type signature and asks the Prover for ‖Q‖1\|Q\|_1 as a separate field element; it certifies this alleged value by the ‖Q‖1\|Q\|_1- SumCheck (now seeded at the alleged value), uses the certified ‖Q‖1\|Q\|_1 in the threshold (27) in place of m−1m-1, and checks over ℤZ that m≤2(‖Q‖1+1)m≤ 2(\|Q\|_1+1) (the Carathéodory cap, doubled to absorb padding the support up to a power of two). The honest Prover could then encode the witness at its true support size (at most ‖Q‖1+1\|Q\|_1+1, and often far smaller), and the proof would shrink accordingly. We keep the simpler protocol above, in which the oracle’s length has m=‖Q‖1+1m=\|Q\|_1+1. 8.2 The full protocol and analysis We now formalize the protocol sketched in Section 2.2. Queroids. Recall that a query q∈q is parsed into its components q=(s1,b1,…,sℓ,bℓ,t)q=(s_1,b_1,…,s_ ,b_ ,t), with sk∈0,1ds_k∈\0,1\^d, bk∈0,1b_k∈\0,1\, and t∈0,1dt∈\0,1\^d. The SumChecks below run over F, so they manipulate the F-valued analogue of a query: q^=(s^1,b^1,…,s^ℓ,b^ℓ,t^)wheres^1,…,s^ℓ,t^∈d and b^1,…,b^ℓ∈. q=( s_1, b_1,…, s_ , b_ , t) s_1,…, s_ , t ^d and b_1,…, b_ . (22) We call such an q q a queroid (in the same spirit as the marginoid of Section 7): it has the shape of a query, but its elements are in F, so it may not describe any actual query. A genuine query asks for the mass of an event such as ωs1=b1 _s_1=b_1; once the description s^1 s_1 and the “bit” b^1 b_1 are non-Boolean, no such event exists. Gadgets. The protocol adapts three of the multilinear gadgets of Section 7. The first is b,sZ agree^Z_b,s of Equation 13, modified for covenience: Z(j^,q^)=Z(j^,s^1,b^1,…,s^ℓ,bℓ^,t^)≔∏k=1ℓ(b^kZ^(j^,s^k)+(1−b^k)(1−Z^(j^,s^k))). agree^Z( j, q)= agree^Z( j, s_1, b_1,…, s_ , b_ , t) _k=1 ( b_k Z( j, s_k)+ (1- b_k ) (1- Z( j, s_k) ) ). (23) The only difference is that we promoted b,sb,s from subscript to an argument q=(b,s,t)q=(b,s,t), but the target variable description t is ignored. The second is vec2int of Equation 11, here in its logB′ B -variate form (β^)=∏k=1logB′(1+β^k(22k−1−1)) vec2int( β)= _k=1 B (1+ β_k(2^2^k-1-1) ), which on a Boolean β∈0,1logB′β∈\0,1\ B equals 22 raised to the integer value of β (as a field element). The Verifier evaluates (β^) vec2int( β) in O(logB′)O( B ) field operations at any β^∈logB′ β B .2020 20 The doubly-exponential constants 22k−12^2^k-1 for k≤logB′k≤ B are precomputed once, each by k−1k-1 repeated squarings, for O((logB′)2)O(( B )^2) field operations in total; each subsequent evaluation of vec2int then costs only the O(logB′)O( B ) multiplications of Equation 11. The third is the weight numerator A(j)=∑β∈0,1logB′(β)A(j,β) weight^A(j)= _β∈\0,1\ B vec2int(β)A(j,β) of Equation 12, here at precision B′B : on the codeword π it is the integer weight αj†α _j of the j-th support vector, so that A(j)/2B′ weight^A(j)/2^B is the probability mass placed on that vector. Marginoids. The key quantities that connect the oracle π=(Z,A)π=(Z,A) to the inconsistency are the two (denominator-cleared) marginoids μ†[s^=b^] μ [ s= b] ≔∑j∈0,1logmA(j)Z(j,q^) _j∈\0,1\ m weight^A(j) agree^Z(j, q) (24) μ†[(s^=b^)∩(t^=1)] μ [( s= b)∩( t=1)] ≔∑j∈0,1logmA(j)Z(j,q^)Z(j,t^), _j∈\0,1\ m weight^A(j) agree^Z(j, q)Z(j, t), whose context (s^,b^)( s, b) and target t t are the components of q q, parsed as in Equation 22.2121 21 In μ†[(s=b)∩(t=1)]μ [(s=b)∩(t=1)] we spell the query event as (s=b)∩(t=1)(s=b)∩(t=1); the μ[⋅]μ[·] notation of the preliminaries would abbreviate it as the context event intersected with the target, but spelling out that the target variable is required to be true is clearer here. They are marginoids because q q is over F: on a Boolean query q they are the genuine (denominator-cleared) marginals 2B′μ[s=b]2^B μ[s=b] and 2B′μ[(s=b)∩(t=1)]2^B μ[(s=b)∩(t=1)]. However, for a non-Boolean queroid q q they are only marginal-shaped F-vectors. The quantity the protocol ultimately tests is the denominator-cleared inconsistency I† , I†≔∑q∈Q(q)(2Bμ†[(s=b)∩(t=1)]−P(q)μ†[s=b])2. _q Q(q) (2^Bμ [(s=b)∩(t=1)]-P(q)μ [s=b] )^2. (25) The dagger follows the convention of τ†τ and αj†α _j: I† is the integer obtained from the squared inconsistency by clearing all denominators (with the square superscript omitted for readability). As we soon prove, when π is the μ R -codeword witnessing distribution μ, I† has the closed form I†=22(B+B′)⋅‖Q‖1⋅I(P,Q)(μ)2, =2^2(B+B )·\|Q\|_1· _(P,Q)(μ)^2, (26) so that checking I†≤τ222(B+B′)‖Q‖1 ≤τ^22^2(B+B )\|Q\|_1 is equivalent to I(P,Q)(μ)≤τ _(P,Q)(μ)≤τ. Input: Predictive model (P,Q)(P,Q) with description length d, context length ℓ and precision B, given as arithmetic circuits of degree at most Δ (30); tolerance τ=τ†/2B≥0τ=τ /2^B≥ 0; soundness error εsound>0 _sound>0; and soundness gap εgap>0 _ gap>0. Oracle: π=(Z,A)π=(Z,A), with Z:logm×d→Z m×F^d and A:logm×logB′→A m×F B . Read the dimensions m,B′∈ℕm,B off the signature of the oracle π, and reject unless m≤2B||+1m≤ 2^B|Q|+1, 22(B+B′)(m−1)<||2^2(B+B )(m-1)<|F|, and m(2B′−1)<||m(2^B -1)<|F|. 1 Run π(δ←εsound/8ℓ+12,ε←εsound/4) VerEnc_F^π(δ← _sound8 +12, ← _sound/4), and reject if it rejects. 2 Expect vI∈v_ from the Prover, and reject unless, as integers, vI≤(τ†)222B′⋅(m−1)over ℤ.v_ ≤(τ )^22^2B ·(m-1) Z. (27) 3 Run (v^I,q^) ( v_ , q) ≔(val←vI,rounds←ℓ(d+1)+d,deg←3Δ+2), SumCheck_F( val← v_ ,\ rounds← (d+1)+d,\ deg← 3 +2), (v^m,q^′) ( v_m, q ) ≔(val←m−1,rounds←ℓ(d+1)+d,deg←Δ), SumCheck_F( val← m-1,\ rounds← (d+1)+d,\ deg← ), and parse q^=(s^1,b^1,…,s^ℓ,b^ℓ,t^) q=( s_1, b_1,…, s_ , b_ , t) for s^1,…,s^ℓ,t^∈d s_1,…, s_ , t ^d and b^1,…,b^ℓ∈ b_1,…, b_ . 4 Expect vμ†[s^=b^],vμ†[(s^=b^)∩(t^=1)]∈v_μ [ s= b],v_μ [( s= b)∩( t=1)] from the Prover, and run π(vμ†[s^=b^];s^1,b^1,…,s^ℓ,b^ℓ)and VerMarginoid_F^π(v_μ [ s= b];\ s_1, b_1,…, s_ , b_ ) π(vμ†[(s^=b^)∩(t^=1)],s^1,b^1,…,s^ℓ,b^ℓ,t^,1). VerMarginoid_F^π(v_μ [( s= b)∩( t=1)];\ s_1, b_1,…, s_ , b_ , t,1). 5 Compute the model values P^(q^),Q^(q^),Q^(q^′)∈ P( q), Q( q), Q( q ) directly, by evaluating the circuits P,QP,Q at q q and q^′ q over F (30). 6 Accept if and only if VerEnc and both VerMarginoid accepted, and v^I=?Q^(q^)⋅(2Bvμ†[(s^=b^)∩(t^=1)]−P^(q^)⋅vμ†[s^=b^])2andv^m=?Q^(q^′)over. v_ ?= Q( q)· (2^Bv_μ [( s= b)∩( t=1)]- P( q)· v_μ [ s= b] )^2 v_m ?= Q( q ) \ F. (28) Algorithm 6 π(P,Q,τ,εsound,εgap) VerConsist^π(P,Q;τ, _sound, _ gap) Algorithm 6 is an IPCP in the sense of Definition 29, with the PCP length counted in F-symbols; Theorem 32 below bounds its four complexity measures. Theorem 32 (Explicit IPCP for - Model-Consistency). For every εsound,εgap>0 _sound, _ gap>0, Algorithm 6 is an IPCP Verifier for - Model-Consistency with the following properties. Let (P,Q)(P,Q) be a predictive model whose circuits have size ≤S≤ S, with arithmetizations P^,Q P, Q of degree ≤Δ≤ . Let τ=τ†/2Bτ=τ /2^B be the consistency threshold for τ†∈0,…,2B−1τ ∈\0,…,2^B-1\. Let F be a prime field such that ||≥2O(ℓd+B+log(1/εgap))⋅Δ/εsound|F|≥ 2^O( d+B+ (1/ _ gap))· / _sound. • Completeness. There exist a proof oracle and an honest Prover such that, if (P,Q)(P,Q) is (τ−εgap)(τ- _ gap)-consistent, the Verifier accepts with probability 11. • Soundness. If (P,Q)(P,Q) is not τ-consistent, the Verifier accepts with probability at most εsound _sound, regardless of the proof oracle and the Prover. • Verifier runtime. (ℓ,d,B,log(1/εgap),1/εsound)+O(|P|+|Q|+Δℓd) poly( ,d,B, (1/ _ gap),1/ _sound)+O(|P|+|Q|+ d) field operations. • PCP length and query complexity. The proof oracle consists of ||O(ℓd+B)|F|^O( d+B) symbols of F, of which the Verifier reads (ℓ,d,B,log(1/εgap),log(1/εsound))/εsound poly( ,d,B, (1/ _ gap), (1/ _sound))/ _sound. • Communication. Prover messages altogether have total length (ℓ,d,BCLOSE, poly( ,d,B, OPENlog(1/εgap),log(1/εsound)) (1/ _ gap), (1/ _sound)) +O(Δℓd)+O( d). Corollary 33 (Boolean IPCP). Theorem 32 holds with the proof oracle over the Boolean alphabet, each F-symbol written in binary. The bounds remain asymptotically the same, with a PCP length of 2(ℓ,d,B)⋅(Δεgap⋅εsound)O(ℓd+B)2 poly( ,d,B)· ( _ gap· _sound )^O( d+B) Proof. Evaluating each gate over F in topological order takes O(S)O(S) field operations and returns C^(x^) C( x), where C C is the polynomial in X1,…,XnX_1,…,X_n that the output gate computes. The arithmetic gates agree with the Boolean connectives on 0,1\0,1\ (¬a=1−a a=1-a, a∧b=aba b=ab, a∨b=a+b−aba b=a+b-ab), so C C extends C off the cube; the hypothesis M<||M<|F| guarantees the integer value is read back without reduction. For the degree, induct over the gates: an input and a constant compute polynomials of degree 11 and 00, an addition gate one of degree at most the maximum of its inputs’, and a multiplication gate one of degree at most their sum—which is the syntactic degree, so degC^≤Δ C≤ . Only multiplication gates raise the degree, and each at most doubles it, so along a path of length D it at most doubles D times: Δ≤2D ≤ 2^D; and D≤SD≤ S gives Δ≤2S ≤ 2^S. ∎ Proof of Theorem 32. At a high level, the encoding test VerEnc pins π to a genuine codeword. The two VerMarginoid calls then return true marginoids of the encoded distribution, the three direct circuit evaluations (30) supply the true model values, and the SumChecks certify that the Prover’s vIv_ is the actual inconsistency and that the total mass ‖Q‖1\|Q\|_1 equals its known value m−1m-1. At that point the integer threshold (27) turns “I† exceeds the bound” into a deterministic rejection. Both directions of the proof rest on Equation 26, which we now prove. For any codeword π~=(Z~,A~)∈μ(n,m,B′) π=( Z, A)∈ R _F(n,m,B ) encoding a distribution μ, the two marginoids of Equation 24, computed for π~ π, are, on a Boolean query q=(s1,b1,…,sℓ,bℓ,t)q=(s_1,b_1,…,s_ ,b_ ,t), μ†[s=b] μ [s=b] =∑jA(j)Z(j,q)=2B′μ[s=b], = _j weight^A(j) agree^Z(j,q)=2^B μ[s=b], μ†[(s=b)∩(t=1)] μ [(s=b)∩(t=1)] =∑jA(j)Z(j,q)Z(j,t)=2B′μ[(s=b)∩(t=1)]. = _j weight^A(j) agree^Z(j,q)Z(j,t)=2^B μ[(s=b)∩(t=1)]. Indeed, A(j)=αj† weight^A(j)=α _j is the integer weight (Definition 21), Z(j,q)=[∀kzj,sk=bk] agree^Z(j,q)= 1[∀ k\ z_j,s_k=b_k] indicates the context, and Z(j,t)=zj,tZ(j,t)=z_j,t. Substituting into Equation 25 and pulling out 2B+B′2^B+B , 2Bμ†[(s=b)∩(t=1)]−P(q)μ†[s=b] 2^Bμ [(s=b)∩(t=1)]-P(q)μ [s=b] =2B+B′(μ[(s=b)∩(t=1)]−P(q)2Bμ[s=b]), =2^B+B (μ[(s=b)∩(t=1)]- P(q)2^Bμ[s=b] ), thereforeI† =22(B+B′)‖Q‖1I(μ)2, =2^2(B+B )\|Q\|_1 (μ)^2, which is Equation 26. Therefore, the check in Equation 27 holds if and only if I(μ)≤τ (μ)≤τ. Before we turn to completeness and soundness, we argue that the field F is large enough to avoid wraparounds. By 12, whenever (P,Q)(P,Q) is (τ−εgap)(τ- _ gap)-consistent there is a witness μ with I(μ)≤τ (μ)≤τ, supported on z1,…,zmz_1,…,z_m with integer weights summing to 2B′2^B where B′∈O(logm+log(1/εgap))B ∈ O( m+ (1/ _ gap)). The honest proof oracle is exactly the codeword π=μ(n,m,B′)π= R _F(n,m,B ) of this μ (Definition 21). (If a single point of μ carries weight 2B′2^B , which Definition 21 cannot store in B′B bits, the Prover lists that point twice in z with the mass split evenly; the support is a multiset, so this encodes the same distribution with every stored weight in 0,…,2B′−1\0,…,2^B -1\.) Write M≔2B+ℓ(d+1)+dM 2^B+ (d+1)+d; as observed in Remark 31, ‖Q‖1≤M\|Q\|_1≤ M for any confidence circuit Q. By assumption, ||>22(B+B′)M≥22(B+B′)‖Q‖1.|F|>2^2(B+B )M≥ 2^2(B+B )\|Q\|_1. (29) Since I(μ)≤1 (μ)≤ 1 for every distribution μ, the true inconsistency of any encoded μ satisfies I†=22(B+B′)‖Q‖1I(μ)2≤22(B+B′)‖Q‖1≤22(B+B′)M<||, =2^2(B+B )\|Q\|_1 (μ)^2≤ 2^2(B+B )\|Q\|_1≤ 2^2(B+B )M<|F|, and likewise ‖Q‖1≤M<||\|Q\|_1≤ M<|F|. Therefore, whenever vIv_ equals I† over F and the ‖Q‖1\|Q\|_1- SumCheck has pinned the mass to m−1m-1, their integer lifts in (27) are exactly I† and ‖Q‖1=m−1\|Q\|_1=m-1, no wraparounds. For an adversarial oracle the same holds with the declared dimensions: the dimension check of Algorithm 6 enforces 22(B+B′)(m−1)<||2^2(B+B )(m-1)<|F| and m(2B′−1)<||m(2^B -1)<|F| for the (m,B′)(m,B ) read off π’s signature, so the lifted comparison in (27) is wraparound-free for any oracle the Prover supplies, once the ‖Q‖1\|Q\|_1- SumCheck has pinned the mass to m−1m-1 (as in the case analysis below); the honest oracle passes the check by Equation 29. Throughout the analysis below, each cited bound (22, 24 and 26) holds for every fixed claimed value and every Prover strategy, over the sub-protocol’s own fresh coins; conditioning on the transcript prefix that fixes that value and averaging therefore preserves each bound, so the failure events may be union-bounded even though the Prover chooses vμ†[s^=b^],vμ†[(s^=b^)∩(t^=1)]v_μ [ s= b],v_μ [( s= b)∩( t=1)] only after q q is public. Completeness. Suppose (P,Q)(P,Q) is (τ−εgap)(τ- _ gap)-consistent, and let μ be the aforementioned sparse distribution so I(μ)≤τ (μ)≤τ. The proof oracle is the codeword π (whose dimensions pass the check of Algorithm 6, by m≤M+1m≤ M+1 and Equation 29), and the honest Prover sends vI=22(B+B′)‖Q‖1I(μ)2v_ =2^2(B+B )\|Q\|_1 (μ)^2 and the true marginoids vμ†[s^=b^]=μ†[s^=b^]v_μ [ s= b]=μ [ s= b] and vμ†[(s^=b^)∩(t^=1)]=μ†[(s^=b^)∩(t^=1)]v_μ [( s= b)∩( t=1)]=μ [( s= b)∩( t=1)] (the total mass ‖Q‖1=m−1\|Q\|_1=m-1 is determined by π’s length, not sent), and plays the honest strategies of 24 and 26. The threshold (27) then holds over ℤZ: the lifts are exactly I† and ‖Q‖1\|Q\|_1 (by Equation 29, as recorded above), and I†=22B22B′‖Q‖1I(μ)2≤(τ†)222B′‖Q‖1 =2^2B2^2B \|Q\|_1 (μ)^2≤(τ )^22^2B \|Q\|_1 since I(μ)≤τ=τ†/2B (μ)≤τ=τ /2^B. VerEnc accepts because π is a genuine codeword; each VerMarginoid accepts with probability 11 because vμ†[s^=b^],vμ†[(s^=b^)∩(t^=1)]v_μ [ s= b],v_μ [( s= b)∩( t=1)] satisfy Equation 20; and the model values P^(q^),Q^(q^),Q^(q^′) P( q), Q( q), Q( q ) are the Verifier’s own evaluations of the circuits (30). Finally, both equalities of (28) hold by construction: the I† - SumCheck runs on the polynomial q↦Q^(q)(2Bμ†[(s=b)∩(t=1)]−P^(q)μ†[s=b])2q Q(q) (2^Bμ [(s=b)∩(t=1)]- P(q)μ [s=b] )^2, so its output is that polynomial at q q, v^I=Q^(q^)(2Bμ†[(s^=b^)∩(t^=1)]−P^(q^)μ†[s^=b^])2=Q^(q^)(2Bvμ†[(s^=b^)∩(t^=1)]−P^(q^)vμ†[s^=b^])2, v_ = Q( q) (2^Bμ [( s= b)∩( t=1)]- P( q)μ [ s= b] )^2= Q( q) (2^Bv_μ [( s= b)∩( t=1)]- P( q)v_μ [ s= b] )^2, likewise v^m=Q^(q^′) v_m= Q( q ), since the ‖Q‖1\|Q\|_1- SumCheck runs on Q Q, which agrees with Q on Q (30). Therefore, the Verifier accepts with probability 11. Soundness. Now suppose (P,Q)(P,Q) is not τ-consistent. Fix any proof oracle π and any Prover; we bound the acceptance probability by cases. Let δ=εsound/8ℓ+12δ= _sound8 +12. If π is δ-far from all μ R codewords, then by 24 (with soundness parameter εsound/4 _sound/4) VerEnc accepts with probability at most εsound/4 _sound/4. Otherwise π is δ-close to a codeword π~=(Z~,A~)∈μ π=( Z, A)∈ R encoding a genuine distribution μ~ μ. The rest of the protocol reads the oracle at 2ℓ+32 +3 points, each uniform over its oracle’s domain: the A-reads by 26, and the Z-reads (j^,s^k),(j^,t^)( j, s_k),( j, t) because s^k,t s_k, t are coins of the I† - SumCheck, independent of the fresh j j. By a union bound, all of these reads agree with π~ π except with probability (2ℓ+3)δ≤εsound/4(2 +3)δ≤ _sound/4. Condition on all queries landing in the agreement region; every subprotocol now behaves as if run on π~ π. Now, • If vμ†[s^=b^]≠2B′μ~[s=b]v_μ [ s= b]≠ 2^B μ[s=b], the corresponding VerMarginoid accepts with probability at most (ℓ+1)logm+2logB′|| ( +1) m+2 B |F| by 26. Similarly for vμ†[(s^=b^)∩(t^=1)]=2B′μ~[(s=b)∩(t=1)]v_μ [( s= b)∩( t=1)]=2^B μ[(s=b)∩(t=1)], but with ℓ+2 +2 instead of ℓ+1 +1 in the numerator. • If vI≠I†v_ ≠ , the corresponding SumCheck in Equation 28 passes with probability at most (3Δ+2)log||/||(3 +2) |Q|/|F|. Here we use the assumption that P P and Q Q have degree at most Δ and that the marginoids are multilinear in q. • If m≠‖Q‖1+1m≠\|Q\|_1+1, the corresponding SumCheck in Equation 28 passes with probability at most Δlog||/|| |Q|/|F|. Here we similarly use the degree bound on P P and Q Q. If instead all the above equalities hold, then by the assumption on |||F| and Equation 26, I†>(τ†)222B′‖Q‖1 >(τ )^22^2B \|Q\|_1 over ℤZ, so the threshold check fails and the Verifier rejects. Collecting these bounds, the Verifier accepts with probability at most Pr[accept]≤εsound4+εsound4+(2ℓ+3)logm+4logB′+(4Δ+2)log||||. [ accept]≤ _sound4+ _sound4+ (2 +3) m+4 B +(4 +2) |Q||F|. The preceding bound gives Pr[accept]≤εsound [ accept]≤ _sound as soon as |||F| exceeds twice its numerator divided by εsound _sound. It remains to confirm that this, and the field hypotheses (17) of the encoding test (24, at soundness parameter εsound/4 _sound/4), hold for a field of the theorem’s size—on top of the wraparound bound (29) assumed above. The encoding test’s no-wrap condition m(2B′−1)<||m(2^B -1)<|F| is itself implied by (29), and every remaining condition is polynomial in the model parameters, Δ , and 1/εsound1/ _sound. Each is monotone in m, so the Verifier certifies them at the a-priori cap m≤M+1m≤ M+1 (Remark 31), never needing the true support size. As (29) is 2O(ℓd+B)(1/εgap)2^O( d+B) poly(1/ _ gap) and dominates, the theorem’s field size ||≥2O(ℓd+B)(1/εgap)⋅Δ/εsound|F|≥ 2^O( d+B) poly(1/ _ gap)· / _sound satisfies them all. The four complexity measures. The PCP length is the size of the oracle π=(Z,A)π=(Z,A): it consists of ||logm+d+||logm+logB′|F| m+d+|F| m+ B symbols (Definition 21), exponential in ℓ,d,B,log(1/εgap) ,d,B, (1/ _ gap), and log(1/εsound) (1/ _sound). The other three measures are additive over the sub-protocols; the table below collects their contributions, writing b≔logm+d+logB′=O(ℓd+B)b m+d+ B =O( d+B) and recalling δ=εsound/(4(2ℓ+3))δ= _sound/(4(2 +3)), log||=ℓ(d+1)+d |Q|= (d+1)+d, and log||=O(ℓd+B+log(1/εgap)+log(1/εsound)) |F|=O( d+B+ (1/ _ gap)+ (1/ _sound)) bits per element. oracle queriescommunication (-elts)Verifier opsblog(1/εsound)/δblog(1/εsound)blog(1/εsound)/δ(×2)ℓlogm+logB′ℓlogm+logB′Direct s(×2)0Δlog||Δlog||model evaluations(×3)00|P|+|Q| array[]l c&oracle queries&communication (F-elts)&Verifier ops\\ VerEnc&b (1/ _sound)/δ&b (1/ _sound)&b (1/ _sound)/δ\\ VerMarginoid\ (× 2)& & m+ B & m+ B \\ Direct SumChecks\ (× 2)&0& |Q|& |Q|\\ model evaluations\ (× 3)&0&0&|P|+|Q|\\ array all entries O(⋅)O(·). Only VerEnc and the two VerMarginoid read the oracle, VerEnc dominating; the query total is O(ℓ(ℓd+B+log(1/εgap))log(1/εsound)/εsound)O ( ( d+B+ (1/ _ gap)) (1/ _sound)/ _sound ). Summing the communication column and converting at log|| |F| bits per element gives Δ⋅(ℓ,d,B,log(1/εgap),log(1/εsound)) · poly( ,d,B, (1/ _ gap), (1/ _sound)), its only circuit-dependent term being the direct SumChecks. And at (log||) poly( |F|) per field operation, the Verifier runs in O(|P|+|Q|)(log||)+Δ⋅(ℓ,d,B,log(1/εgap),1/εsound)O(|P|+|Q|) poly( |F|)+ · poly( ,d,B, (1/ _ gap),1/ _sound), its only circuit-dependent term being the three circuit evaluations. ∎ Remark 34 (On the 1/εsound1/ _sound in the query complexity). The 1/εsound1/ _sound in the query complexity enters through the proximity parameter δ=εsound/(4(2ℓ+3))δ= _sound/(4(2 +3)) of the encoding test (24); we wonder whether it can be brought down to log(1/εsound) poly (1/ _sound). For example, one could encode the witness not by its multilinear extension but by an extension of higher individual degree (though perhaps lower total degree), admitting a more query-efficient proximity test; the higher individual degree would propagate into the SumChecks and hence into the field size. We have not attempted this direction beyond this sketch. Remark 35 (A single evaluation point). The two direct SumChecks of Algorithm 6 range over the same universe Q, and their soundness does not require independent randomness: the union bound in the proof of Theorem 32 sums the two error events whatever their joint distribution. The Verifier may therefore run both SumChecks on a single stream of coins, making q^′=q q = q: the final checks (28) then evaluate the model at one queroid (the value Q^(q^) Q( q) serves both equalities), and the three VerifyMLE calls of Theorem 38 become two. The one requirement is that each round’s two messages be committed before that round’s coin is revealed. Running the SumChecks in lockstep (both round-k polynomials, then the coin) satisfies it with a single Prover, and the protocol remains an IPCP, so Section 8.3 and the compilers of Remark 40 still apply. Running them sequentially with one Prover does not: having seen the first transcript, the Prover knows every coin of the second SumCheck in advance, and can choose its final round’s coefficients so that the residual claim lands exactly on Q^(q^) Q( q), passing on a false claim with probability 1−O(1/||)1-O(1/|F|). Sequential order is sound again when the ‖Q‖1\|Q\|_1- SumCheck is played by a prover isolated from the first transcript: formally a second prover, and in the self-proving instantiation one further context reset (Remark 1). Remark 36 (The gap and the exact-witness instantiation). Running Algorithm 6 with the exact rational witness of Lemma 13 (no gap) preserves completeness and soundness, but the threshold τ222(B+B′)‖Q‖1τ^22^2(B+B )\|Q\|_1 has bit-length 2O(ℓd+B)2^O( d+B), so the field required by the proof of Theorem 32 becomes single-exponentially large. The IPCP statement above does not apply to this instantiation. This does not contradict Corollary 18: that corollary obtains its polynomial-time Verifier by Cook–Levin arithmetization of the NP verifier underlying Proposition 9, foregoing Carathéodory structure entirely. Theorem 32 should be read as an explicit but (slightly) weaker counterpart of Corollary 18. Nor can the support-only design of Proposition 9 be imported here to dispense with the gap, though in the explicit setting it costs no completeness slack at all. Its Verifier cannot even write down the linear system it would solve, the side of which is m=‖Q‖1+1=2Θ(ℓd)m=\|Q\|_1+1=2 ( d), and delegating the solve to the Prover does not help: that design relocates the weights’ computation, not their precision. By Lemma 13 the exact weights are ratios of determinants of Θ(m(B+logm)) (m(B+ m)) bits, and whatever carries them, oracle or messages, forces log|| |F| of that order. It would also owe a local check of positivity for exponentially many weights, which μ R _F (Definition 21) gets for free from its unsigned representation; and delegating a generic computation is the move Corollary 18 already makes in full, which Remark 19 is our reason for not making. 8.3 Improved efficiency with delegation of computation The dependence on the degree Δ in Theorem 32, exponential in the circuit depth in the worst case, stems from a single design choice: the Verifier reads each model value P^(q^),Q^(q^),Q^(q^′) P( q), Q( q), Q( q ) by evaluating the circuit as the high-degree polynomial it computes. The standard machinery of delegation of computation removes it. We replace each direct evaluation by a call to VerifyMLE (37), now letting PMLE,QMLEP_MLE,Q_MLE denote the multilinear extensions of P,QP,Q: rather than evaluate the circuit itself, the Verifier receives an alleged value from the Prover and has VerifyMLE certify it through interaction. This is the same move, from a quantity the Verifier computes to one a sub-protocol certifies, as the passage from VerMarginoid to VerMarginal in Section 7. The fact underlying VerifyMLE is a doubly-efficient interactive proof for circuit evaluation: it delegates the evaluation to the Prover, at a cost scaling with the circuit’s depth D rather than its degree. Fact 37 (Tha 13). Let C be a layered arithmetic circuit over a field F with n inputs, depth D, and size S, computing a function 0,1n→0,…,M−1\0,1\^n→\0,…,M-1\ for M<||M<|F|, and let CMLE:n→C_MLE ^n be its multilinear extension.2222 22 We emphasize that CMLEC_MLE is the multilinear extension of the function computed by C, not the polynomial C C of 30; the two agree only on 0,1n\0,1\^n. The primitive below, with these exact costs, is obtained by running the protocol of Tha 13 on the wide circuit made of 2n2^n parallel copies of C, the wwth hardwired to input w: the multilinear extension of its output layer is CMLEC_MLE, and its width enters the costs only through its logarithm, n+logSn+ S. There is a Verifier (C,x^,y) VerifyMLE_F(C, x,y) such that, for any x^∈n x ^n and y^∈ y , • Completeness: there is an honest Prover for which, if y^=CMLE(x^) y=C_MLE( x), the Verifier accepts with probability 11. • Soundness: if y^≠CMLE(x^) y≠ C_MLE( x), the Verifier accepts with probability O(D(n+logS)/||)O(D(n+ S)/|F|), regardless of the Prover. • Complexity: the communication is O(D(n+logS))O(D(n+ S)) field elements and the Verifier runs in O(S+D(n+logS))O(S+D(n+ S)) field operations. The S term shrinks to S polylogS if C is logspace-uniform. Theorem 38 (Explicit IPCP for - Model-Consistency, with model delegation). Let (P,Q)(P,Q) be a predictive model whose circuits are layered, each with depth ≤D≤ D and size ≤S≤ S. Run Algorithm 6 with the direct circuit evaluations replaced by the calls (P,q^,PMLE(q^)) VerifyMLE_F(P, q,P_MLE( q)), (Q,q^,QMLE(q^)) VerifyMLE_F(Q, q,Q_MLE( q)), and (Q,q^′,QMLE(q^′)) VerifyMLE_F(Q, q ,Q_MLE( q )) of 37, and the two direct SumChecks at degrees 55 and 11. The result is an IPCP Verifier for - Model-Consistency with completeness and soundness as in Theorem 32, with PCP length and query complexity unchanged, and with the following bounds, polynomial in the depth D in place of the degree Δ , over any prime field with ||≥2O(ℓd+B+log(1/εgap))⋅(ℓ,d,B,D,logS)/εsound|F|≥ 2^O( d+B+ (1/ _ gap))· poly( ,d,B,D, S)/ _sound: • Verifier runtime. (ℓ,d,B,log(1/εgap),1/εsound) poly( ,d,B, (1/ _ gap),1/ _sound), plus the three VerifyMLE calls, O(|P|+|Q|+D(ℓd+logS))O(|P|+|Q|+D( d+ S)) field operations. • Communication. (ℓ,d,B,log(1/εgap),log(1/εsound)) poly( ,d,B, (1/ _ gap), (1/ _sound)), plus the three VerifyMLE transcripts, O(D(ℓd+logS))O(D( d+ S)) field elements. Proof. The substitution changes the protocol in three places; everywhere else the analysis of Theorem 32 applies verbatim. Model values. The values PMLE(q^),QMLE(q^),QMLE(q^′)P_MLE( q),Q_MLE( q),Q_MLE( q ) are now supplied by the Prover and certified by VerifyMLE rather than computed by the Verifier. By 37, with input length n=log||=ℓ(d+1)+dn= |Q|= (d+1)+d, each call is complete on the true value and, on a false value, accepts with probability O(D(log||+logS)/||)O(D( |Q|+ S)/|F|). In the soundness union bound this replaces the zero error of direct evaluation with O(D(log||+logS)/||)O(D( |Q|+ S)/|F|) from the three VerifyMLE calls, restoring the bound of the GKR-based protocol. SumCheck degrees. With PMLE,QMLEP_MLE,Q_MLE multilinear the I† -summand QMLE(q)(2Bμ†[(s=b)∩(t=1)]−PMLE(q)μ†[s=b])2Q_MLE(q)(2^Bμ [(s=b)∩(t=1)]-P_MLE(q)μ [s=b])^2 has individual q-degree degQMLE+2(degPMLE+1)=5 Q_MLE+2( P_MLE+1)=5 and the ‖Q‖1\|Q\|_1-summand QMLE(q)Q_MLE(q) degree 11 (the marginoids being multilinear in q as before). The two direct SumChecks thus contribute 6log||/||6 |Q|/|F| to the soundness bound and O(log||)O( |Q|) field elements each to the communication, and the degree Δ disappears from every bound. The field size (29) and the wraparound argument are unchanged (they never involved Δ ), so collecting the soundness terms gives the stated ||≥2O(ℓd+B+log(1/εgap))⋅(ℓ,d,B,D,logS)/εsound|F|≥ 2^O( d+B+ (1/ _ gap))· poly( ,d,B,D, S)/ _sound, dominated as before by the wraparound term. Verifier work and communication. The Verifier no longer evaluates P,QP,Q; its circuit-dependent cost is the three VerifyMLE calls, each O(S+D(ℓd+logS))O(S+D( d+ S)) field operations and O(D(ℓd+logS))O(D( d+ S)) communication by 37, hence O(|P|+|Q|+D(ℓd+logS))O(|P|+|Q|+D( d+ S)) and O(D(ℓd+logS))O(D( d+ S)) in total. The per-call S term is the cost of evaluating the layered circuit once, as 37 requires. A circuit that is not already layered is first layered: this preserves the depth D and increases the size to at most O(SD)O(SD), so the |P|+|Q||P|+|Q| term grows to (|P|+|Q|)D(|P|+|Q|)D, while log(SD)=O(logS) (SD)=O( S) (as D≤SD≤ S) leaves the field size and communication unchanged. ∎ Since D≤SD≤ S, every bound above is polynomial in the model size for circuits of any depth, removing the constant- or logarithmic-depth restriction under which Theorem 32 is polynomial. And by the argument of Corollary 33, Theorem 38 too holds with the proof oracle over the Boolean alphabet, with Δ replaced by (ℓ,d,B,D,logS) poly( ,d,B,D, S) in the PCP length. Remark 39 (Verifier efficiency for uniform models). The only Verifier costs in Theorem 38 that depend on the size of (P,Q)(P,Q) are reading the input circuits and the three VerifyMLE calls. If the model is instead given succinctly, as a logspace-uniform layered circuit family accessed through its description, then the uniform clause of 37 brings each VerifyMLE call to (D,ℓd,logS) poly(D, d, S) field operations, and the Verifier runs in (ℓ,d,B,D,logS,log(1/εgap),1/εsound) poly( ,d,B,D, S, (1/ _ gap),1/ _sound) time overall—polylogarithmic in the circuit size. The honest Prover remains exponential-time (it writes the proof oracle), so this is Verifier-side efficiency only, in the spirit of doubly-efficient interactive proofs GKR 15. Remark 40 (Succinct arguments for - Model-Consistency). The delegated Verifier of Theorem 38 runs in polynomial time, reads its oracle at polynomially many points, and exchanges polynomially many bits, so standard compilers turn the protocol into a succinct argument for - Model-Consistency at no asymptotic cost. Two apply, each trading an assumption for a guarantee: • Collision-resistant hashing yields a public-coin interactive argument (Kil 92): the Prover commits the oracle by a single Merkle tree, and the interaction runs in the clear. The oracle is exponentially long, but the honest Prover is already exponential-time (it writes π), so the commitment costs nothing asymptotically, as in the universal arguments of BG 02. • A random oracle yields a non-interactive argument (Mic 00): apply the Fiat–Shamir transform to the resulting public-coin interactive oracle proof (BCS 16). Two caveats attach. Negligible soundness is obtained by parallel repetition before the interactive compilation; repetition does not survive the Fiat–Shamir transform (a cheating prover grinds the hash round by round), so the non-interactive route instead requires round-by-round soundness, which our protocol is expected to acquire once its plain oracle reads are replaced by self-corrected ones (27); we do not prove this here. The knowledge guarantee is only the weak, bit-by-bit one of BG 02, an exponentially long witness being too large to extract outright. Here “succinct” means (|x|,λ) poly(|x|,λ) communication and Verifier time (polynomial in the instance, not polylogarithmic), which, unlike the base Theorem 32, holds for circuits of any depth by Theorem 38. A user can thus certify a model’s consistency against a (|x|,λ) poly(|x|,λ) certificate, at the price of computational rather than unconditional soundness. 9 Conclusions and open problems We gave an explicit Interactive PCP for deciding whether a predictive model (P,Q)(P,Q) is consistent up to an ℓ2 _2 threshold, with a Verifier whose only access to the model is a few point evaluations of its circuits, together with a few queries to a proof oracle encoding a witnessing distribution (Theorem 32). We close with what we find natural about the construction, and with the questions it leaves open. A “natural” factorization. Against an honest Prover, every object of Algorithm 6 carries a meaning: the oracle (Z,A)(Z,A) is a Reed–Muller encoding of a witnessing distribution μ, the SumChecks express the inconsistency and the threshold ‖Q‖1\|Q\|_1 as marginals of μ, and VerEnc pins the encoding’s validity to fixed constants, the way a checksum does. The protocol thus factors into a model-specific, semantically probabilistic witness core and a model-agnostic proving overlay. Following the pipeline of Section 8.1, the route from a trained model to one that proves its own consistency then partitions into stages of decreasing “magic”: learning (P,Q)(P,Q), finding a witnessing distribution, sparsifying it, and finally a purely classical proving overlay (the encoding and the SumChecks) that could itself be replaced by a learned component, towards an end-to-end Self-Proving model in the spirit of AGPR 25. The two roles the IPCP requires, a stateless oracle and a stateful Prover, come “for free” from a single model that controls its context (Remark 1). We leave a formal account of this factorization, and its consequences for learnability, to future work. An exact Prover for an approximate statement. The statement our protocol proves is approximate by design: the Verifier certifies consistency up to the threshold τ, promising acceptance only when the model is (τ−εgap)(τ- _ gap)-consistent. The honest Prover enjoys none of this slack. To run Algorithm 6 it must compute the inconsistency attained by its witness exactly: I† (Equation 25) is a sum over all of Q, an integer of O(ℓd+B+log(1/εgap))O( d+B+ (1/ _ gap)) bits, and the Prover commits to it as vIv_ before the SumChecks begin, each round of which then demands an exact partial sum of the same kind. A Prover that commits to anything else, say an estimate of I† from sampled queries, is caught by the final check (28) exactly as a cheating Prover would be (22); the tolerance enters only once, as the integer comparison (27) of the exact committed value against the threshold. (The single-exponential field of Theorem 32 is the same exactness on the Verifier’s side: F must carry I† at full precision, without wraparound.) So although we never ask whether the model is consistent exactly, we do ask the Prover for its inconsistency exactly, and the benefit of verifying approximate consistency is lost on the one party that computes: a Prover that estimates rather than sums, as a learned Prover would, has no accepting strategy. The remedy, we believe, is a SumCheck in which approximation is native. The sum-check protocol for approximate computations of BDG+ 26 proves exactly such claims, ∑xg(x)≈H _xg(x)≈ H with g low-degree over the reals, its Verifier accepting Prover messages that are themselves only approximately consistent. Whether our protocol can be soundly instantiated over it, so that the honest Prover need only estimate its witness’s inconsistency to within the gap, is a main question we leave open. Further directions. • Other loss functions. The squared ℓ2 _2 measure is what turns the witness’s stationarity conditions into a linear system (Section 5); the SumCheck protocol accommodates the higher-degree summand of an ℓp _p measure directly, while the witness analysis would have to be redone for integer p>2p>2. More interestingly, one could consider the cross-entropy loss whose non-polynomial summand puts it beyond the arithmetization route taken here. • Zero-knowledge. In the explicit setting the queries reveal the user’s inputs, so a variant that hides them is desirable; the encoding-and- SumCheck machinery is standard enough that known zero-knowledge techniques plausibly apply. • Succinctness and delegation. These are separate axes: Remark 40 compiles the IPCP into a (|x|,λ) poly(|x|,λ)-size argument, while Section 8.3 removes the depth dependence of the model evaluations. Neither subsumes the other. AI Use Disclosure We used AI tools for research assistance, including brainstorming, identifying relevant references, suggesting potentially useful theorems or high-level organizational skeletons, and double-checking our work. All material in the paper was written and verified by the authors. Acknowledgements We are grateful to Avishay Tal for important comments and contributions to earlier versions of this work. OP thanks Thomas Bourgeat, Alessandro Chiesa, Lénaïc Chizat, Nicolas Flammarion, Tal Herman, Viktor Kunčak, Nicholas Spooner, Justin Thaler, Thomas Vidick and Guy Weissenberg for helpful comments. References AC (25) Josh Alman and Lijie Chen. Efficient construction of rigid matrices using an np oracle. SIAM Journal on Computing, 54(4):FOCS19–102, 2025. AGPR (25) Noga Amit, Shafi Goldwasser, Orr Paradise, and Guy N Rothblum. A theory for worst-case vs. average-case guarantees for llms. In The Thirty-ninth Annual Conference on Neural Information Processing Systems (NeurIPS), 2025. AS (98) Sanjeev Arora and Shmuel Safra. Probabilistic checking of proofs: A new characterization of NP. J. ACM, 45(1):70–122, 1998. AZWG (21) Cem Anil, Guodong Zhang, Yuhuai Wu, and Roger B. Grosse. Learning to give checkable answers with prover-verifier games. CoRR, abs/2108.12099, 2021. Bab (85) László Babai. Trading group theory for randomness. In Robert Sedgewick, editor, Proceedings of the 17th Annual ACM Symposium on Theory of Computing, May 6-8, 1985, Providence, Rhode Island, USA, pages 421–429. ACM, 1985. Bab (90) László Babai. E-mail and the unexpected power of interaction. In Proceedings: Fifth Annual Structure in Complexity Theory Conference, Universitat Politècnica de Catalunya, Barcelona, Spain, July 8-11, 1990, pages 30–44. IEEE Computer Society, 1990. Bar (15) Siddharth Barman. Approximating nash equilibria and dense bipartite subgraphs via an approximate version of caratheodory’s theorem. In Rocco A. Servedio and Ronitt Rubinfeld, editors, Proceedings of the Forty-Seventh Annual ACM on Symposium on Theory of Computing, STOC 2015, Portland, OR, USA, June 14-17, 2015, pages 361–369. ACM, 2015. BBH+ (12) Boaz Barak, Fernando G. S. L. Brandão, Aram W. Harrow, Jonathan A. Kelner, David Steurer, and Yuan Zhou. Hypercontractivity, sum-of-squares proofs, and their applications. In Howard J. Karloff and Toniann Pitassi, editors, Proceedings of the 44th Symposium on Theory of Computing Conference, STOC 2012, New York, NY, USA, May 19 - 22, 2012, pages 307–326. ACM, 2012. BC (18) Rishiraj Bhattacharyya and Sourav Chakraborty. Property testing of joint distributions using conditional samples. ACM Trans. Comput. Theory, 10(4):16:1–16:20, 2018. BCF+ (25) Yoshua Bengio, Michael Cohen, Damiano Fornasiere, Joumana Ghosn, Pietro Greiner, Matt MacDermott, Sören Mindermann, Adam Oberman, Jesse Richardson, Oliver Richardson, Marc-Antoine Rondeau, Pierre-Luc St-Charles, and David Williams-King. Superintelligent agents pose catastrophic risks: Can scientist ai offer a safer path?, 2025. BCP+ (25) Yoshua Bengio, Stephen Clare, Carina Prunkl, Shalaleh Rismani, Maksym Andriushchenko, Ben Bucknall, Philip Fox, Tiancheng Hu, Cameron Jones, Sam Manning, et al. International ai safety report 2025: first key update: capabilities and risk implications. arXiv preprint arXiv:2510.13653, 2025. BCS (16) Eli Ben-Sasson, Alessandro Chiesa, and Nicholas Spooner. Interactive oracle proofs. In Martin Hirt and Adam D. Smith, editors, Theory of Cryptography - 14th International Conference, TCC 2016-B, Beijing, China, October 31 - November 3, 2016, Proceedings, Part I, Lecture Notes in Computer Science, pages 31–60, 2016. BDG+ (26) Dor Bitan, Zachary DeStefano, Shafi Goldwasser, Yuval Ishai, Yael Tauman Kalai, and Justin Thaler. Sum-check protocol for approximate computations. In Joan Daemen and Emmanuel Thomé, editors, Advances in Cryptology - EUROCRYPT 2026 - 45th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Rome, Italy, May 10-14, 2026, Proceedings, Part VII, volume 16547 of Lecture Notes in Computer Science, pages 209–238. Springer, 2026. BFL (91) László Babai, Lance Fortnow, and Carsten Lund. Non-deterministic exponential time has two-prover interactive protocols. Comput. Complex., 1:3–40, 1991. BFLS (91) László Babai, Lance Fortnow, Leonid A. Levin, and Mario Szegedy. Checking computations in polylogarithmic time. In Cris Koutsougeras and Jeffrey Scott Vitter, editors, Proceedings of the 23rd Annual ACM Symposium on Theory of Computing, May 5-8, 1991, New Orleans, Louisiana, USA, pages 21–31. ACM, 1991. BFR+ (00) Tugkan Batu, Lance Fortnow, Ronitt Rubinfeld, Warren D. Smith, and Patrick White. Testing that distributions are close. In 41st Annual Symposium on Foundations of Computer Science, FOCS 2000, Redondo Beach, California, USA, November 12-14, 2000, pages 259–269. IEEE Computer Society, 2000. BG (02) Boaz Barak and Oded Goldreich. Universal arguments and their applications. Proceedings 17th IEEE Annual Conference on Computational Complexity, pages 194–203, 2002. BHPT (24) Amey Bhangale, Prahladh Harsha, Orr Paradise, and Avishay Tal. Rigid matrices from rectangular pcps. SIAM Journal on Computing, 53(2):480–523, 2024. BIM+ (26) Jonah Brown-Cohen, Geoffrey Irving, Simon C. Marshall, Ilan Newman, Georgios Piliouras, and Mario Szegedy. Debate is efficient with your time. CoRR, abs/2602.08630, 2026. BIP (24) Jonah Brown-Cohen, Geoffrey Irving, and Georgios Piliouras. Scalable AI safety via doubly-efficient debate. In Ruslan Salakhutdinov, Zico Kolter, Katherine A. Heller, Adrian Weller, Nuria Oliver, Jonathan Scarlett, and Felix Berkenkamp, editors, Forty-first International Conference on Machine Learning, ICML 2024, Vienna, Austria, July 21-27, 2024, Proceedings of Machine Learning Research, pages 4585–4602. PMLR / OpenReview.net, 2024. BIP (25) Jonah Brown-Cohen, Geoffrey Irving, and Georgios Piliouras. Avoiding obfuscation with prover-estimator debate. CoRR, abs/2506.13609, 2025. BLD+ (23) Yoshua Bengio, Salem Lahlou, Tristan Deleu, Edward J Hu, Mo Tiwari, and Emmanuel Bengio. Gflownet foundations. Journal of Machine Learning Research, 24(210):1–55, 2023. BLM+ (25) Edoardo Botta, Yuchen Li, Aashay Mehta, Jordan T. Ash, Cyril Zhang, and Andrej Risteski. On the query complexity of verifier-assisted language generation. In Aarti Singh, Maryam Fazel, Daniel Hsu, Simon Lacoste-Julien, Felix Berkenkamp, Tegan Maharaj, Kiri Wagstaff, and Jerry Zhu, editors, Forty-second International Conference on Machine Learning, ICML 2025, Vancouver, BC, Canada, July 13-19, 2025, Proceedings of Machine Learning Research. PMLR / OpenReview.net, 2025. BLR (90) Manuel Blum, Michael Luby, and Ronitt Rubinfeld. Self-testing/correcting with applications to numerical problems. In Symposium on the Theory of Computing, 1990. Boo (54) George Boole. An Investigation of the Laws of Thought, on Which Are Founded the Mathematical Theories of Logic and Probabilities. Walton and Maberly, London, 1854. BRG+ (26) Yoshua Bengio, Oliver Richardson, Tomáš Gavenčiak, Michael Cohen, Rory Svarc, Damiano Fornasiere, Gael Gendron, David Hyland, Aton Kamanda, Adam Oberman, Francis Rhys Ward, Anna Gavenčiak, Jacob Livingston Slosser, Vincent Mai, Iulian Serban, and Joumana Ghosn. Safety from honesty in a disinterested ai predictor, 2026. BS (14) Boaz Barak and David Steurer. Sum-of-squares proofs and the quest toward optimal algorithms. CoRR, abs/1404.5236, 2014. Can (22) Clément L. Canonne. Topics and techniques in distribution testing: A biased but representative sample. Found. Trends Commun. Inf. Theory, 19(6):1032–1198, 2022. Car (07) Constantin Carathéodory. Über den variabilitätsbereich der koeffizienten von potenzreihen, die gegebene werte nicht annehmen. Mathematische Annalen, 64(1):95–115, 1907. CCK+ (21) Clément L. Canonne, Xi Chen, Gautam Kamath, Amit Levi, and Erik Waingarten. Random restrictions of high dimensional distributions and uniformity testing with subcube conditioning. In Dániel Marx, editor, Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms, SODA 2021, Virtual Conference, January 10 - 13, 2021, pages 321–336. SIAM, 2021. CCR+ (25) Deeparnab Chakrabarty, Xi Chen, Simeon Ristic, C. Seshadhri, and Erik Waingarten. Monotonicity testing of high-dimensional distributions with subcube conditioning. In Michal Koucký and Nikhil Bansal, editors, Proceedings of the 57th Annual ACM Symposium on Theory of Computing, STOC 2025, Prague, Czechia, June 23-27, 2025, pages 1019–1030. ACM, 2025. CFLS (93) Anne Condon, Joan Feigenbaum, Carsten Lund, and Peter W. Shor. Probabilistically checkable debate systems and approximation algorithms for pspace-hard functions. In S. Rao Kosaraju, David S. Johnson, and Alok Aggarwal, editors, Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, May 16-18, 1993, San Diego, CA, USA, pages 305–314. ACM, 1993. CFS (86) William J. Cook, Jean Fonlupt, and Alexander Schrijver. An integer analogue of carathéodory’s theorem. J. Comb. Theory B, 40(1):63–70, 1986. CFS (17) Alessandro Chiesa, Michael A. Forbes, and Nicholas Spooner. A zero knowledge sumcheck and its applications. Electron. Colloquium Comput. Complex., TR17, 2017. CG (18) Alessandro Chiesa and Tom Gur. Proofs of proximity for distribution testing. In Anna R. Karlin, editor, 9th Innovations in Theoretical Computer Science Conference, ITCS 2018, Cambridge, MA, USA, January 11-14, 2018, LIPIcs, pages 53:1–53:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Chv (83) Vasek Chvatal. Linear Programming. W. H. Freeman and Company, San Francisco, 1983. Page 145. CM (24) Xi Chen and Cassandra Marcussen. Uniformity testing over hypergrids with subcube conditioning. In David P. Woodruff, editor, Proceedings of the 2024 ACM-SIAM Symposium on Discrete Algorithms, SODA 2024, Alexandria, VA, USA, January 7-10, 2024, pages 4338–4370. SIAM, 2024. Coo (71) Stephen A. Cook. The complexity of theorem-proving procedures. In Michael A. Harrison, Ranan B. Banerji, and Jeffrey D. Ullman, editors, Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, May 3-5, 1971, Shaker Heights, Ohio, USA, pages 151–158. ACM, 1971. CRS (15) Clément L. Canonne, Dana Ron, and Rocco A. Servedio. Testing probability distributions using conditional samples. SIAM J. Comput., 44(3):540–616, 2015. dF (37) Bruno de Finetti. La prévision : ses lois logiques, ses sources subjectives. Annales de l’Institut Henri Poincaré, 7(1):1–68, 1937. English translation in Kyburg and Smokler, eds., Studies in Subjective Probability, Wiley, 1964. DFPT (18) Glauber De Bona, Marcelo Finger, Nico Potyka, and Matthias Thimm. Inconsistency measurement in probabilistic logic. In John Grant and Maria Vanina Martinez, editors, Measuring Inconsistency in Information, volume 73 of Studies in Logic, pages 235–269. College Publications, 2018. Dix (82) John D. Dixon. Exact solution of linear equations using P-adic expansions. Numerische Mathematik, 40(1):137–141, 1982. DLT+ (24) Yilun Du, Shuang Li, Antonio Torralba, Joshua B. Tenenbaum, and Igor Mordatch. Improving factuality and reasoning in language models through multiagent debate. In Ruslan Salakhutdinov, Zico Kolter, Katherine A. Heller, Adrian Weller, Nuria Oliver, Jonathan Scarlett, and Felix Berkenkamp, editors, Forty-first International Conference on Machine Learning, ICML 2024, Vienna, Austria, July 21-27, 2024, Proceedings of Machine Learning Research, pages 11733–11763. PMLR / OpenReview.net, 2024. ES (06) Friedrich Eisenbrand and Gennady Shmonin. Carathéodory bounds for integer cones. Oper. Res. Lett., 34(5):564–568, 2006. FGL+ (96) Uriel Feige, Shafi Goldwasser, László Lovász, Shmuel Safra, and Mario Szegedy. Interactive proofs and the hardness of approximating cliques. J. ACM, 43(2):268–292, 1996. FHM (90) Ronald Fagin, Joseph Y. Halpern, and Nimrod Megiddo. A logic for reasoning about probabilities. Inf. Comput., 87(1/2):78–128, 1990. FK (97) Uriel Feige and Joe Kilian. Making games short (extended abstract). In Frank Thomson Leighton and Peter W. Shor, editors, Proceedings of the Twenty-Ninth Annual ACM Symposium on the Theory of Computing, El Paso, Texas, USA, May 4-6, 1997, pages 506–516. ACM, 1997. Fre (77) Rusins Freivalds. Probabilistic machines can use less running time. In Bruce Gilchrist, editor, Information Processing, Proceedings of the 7th IFIP Congress 1977, Toronto, Canada, August 8-12, 1977, pages 839–842. North-Holland, 1977. FRG+ (26) Damiano Fornasiere, Oliver Richardson, Gaël Gendron, Iulian Serban, and Yoshua Bengio. The scientist ai: Safe by design, by not desiring, 2026. FRS (94) Lance Fortnow, John Rompel, and Michael Sipser. On the power of multi-prover interactive protocols. Theor. Comput. Sci., 134(2):545–557, 1994. GGR (98) Oded Goldreich, Shafi Goldwasser, and Dana Ron. Property testing and its connection to learning and approximation. J. ACM, 45(4):653–750, 1998. GHMS (23) Surbhi Goel, Steve Hanneke, Shay Moran, and Abhishek Shetty. Adversarial resilience in sequential prediction via abstention. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine, editors, Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 - 16, 2023, 2023. GHR (25) Oded Goldreich, Tal Herman, and Guy N. Rothblum. Interactive proof systems for FARNESS. Electron. Colloquium Comput. Complex., TR25, 2025. GJK+ (24) Tom Gur, Mohammad Mahdi Jahanara, Mohammad Mahdi Khodabandeh, Ninad Rajgopal, Bahar Salamatian, and Igor Shinkar. On the power of interactive proofs for learning. In Bojan Mohar, Igor Shinkar, and Ryan O’Donnell, editors, Proceedings of the 56th Annual ACM Symposium on Theory of Computing, STOC 2024, Vancouver, BC, Canada, June 24-28, 2024, pages 1063–1070. ACM, 2024. (55) Shafi Goldwasser, Adam Tauman Kalai, Yael Kalai, and Omar Montasser. Beyond perturbations: Learning guarantees with arbitrary adversarial test examples. In Hugo Larochelle, Marc’Aurelio Ranzato, Raia Hadsell, Maria-Florina Balcan, and Hsuan-Tien Lin, editors, Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual, 2020. (56) Shafi Goldwasser, Adam Tauman Kalai, Yael Tauman Kalai, and Omar Montasser. Identifying unpredictable test examples with worst-case guarantees. In Information Theory and Applications Workshop, ITA 2020, San Diego, CA, USA, February 2-7, 2020, pages 1–14. IEEE, 2020. GKP (88) George F. Georgakopoulos, Dimitris J. Kavvadias, and Christos H. Papadimitriou. Probabilistic satisfiability. J. Complex., 4(1):1–11, 1988. GKR (15) Shafi Goldwasser, Yael Tauman Kalai, and Guy N. Rothblum. Delegating computation: Interactive proofs for muggles. J. ACM, 62(4):27:1–27:64, 2015. GMR (89) Shafi Goldwasser, Silvio Micali, and Charles Rackoff. The knowledge complexity of interactive proof systems. SIAM J. Comput., 18(1):186–208, 1989. Gol (08) Oded Goldreich. Computational complexity - a conceptual perspective. Cambridge University Press, 2008. GR (00) Oded Goldreich and Dana Ron. On testing expansion in bounded-degree graphs. Electron. Colloquium Comput. Complex., TR00, 2000. GRSY (21) Shafi Goldwasser, Guy N. Rothblum, Jonathan Shafer, and Amir Yehudayoff. Interactive proofs for verifying machine learning. In James R. Lee, editor, 12th Innovations in Theoretical Computer Science Conference, ITCS 2021, Virtual Conference, January 6-8, 2021, LIPIcs, pages 41:1–41:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. HA (25) Lewis Hammond and Sam Adam-Day. Neural interactive proofs. In The Thirteenth International Conference on Learning Representations, ICLR 2025, Singapore, April 24-28, 2025. OpenReview.net, 2025. Had (93) Jacques Hadamard. Résolution d’une question relative aux déterminants. Bull. des sciences math., 2:240–246, 1893. Hås (01) Johan Håstad. Some optimal inapproximability results. J. ACM, 48(4):798–859, 2001. Her (24) Tal Herman. Public coin interactive proofs for label-invariant distribution properties. In Amit Kumar and Noga Ron-Zewi, editors, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques, APPROX/RANDOM 2024, London School of Economics, London, UK, August 28-30, 2024, LIPIcs, pages 72:1–72:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. HR (22) Tal Herman and Guy N. Rothblum. Verifying the unseen: interactive proofs for label-invariant distribution properties. In Stefano Leonardi and Anupam Gupta, editors, STOC ’22: 54th Annual ACM SIGACT Symposium on Theory of Computing, Rome, Italy, June 20 - 24, 2022, pages 1208–1219. ACM, 2022. HR (23) Tal Herman and Guy N. Rothblum. Doubley-efficient interactive proofs for distribution properties. In 64th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2023, Santa Cruz, CA, USA, November 6-9, 2023, pages 743–751. IEEE, 2023. (69) Tal Herman and Guy N. Rothblum. How to verify any (reasonable) distribution property: Computationally sound argument systems for distributions. In The Thirteenth International Conference on Learning Representations, ICLR 2025, Singapore, April 24-28, 2025. OpenReview.net, 2025. (70) Tal Herman and Guy N. Rothblum. Proving natural distribution properties is harder than testing them. In 66th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2025, Sydney, Australia, December 14-17, 2025, pages 2003–2016. IEEE, 2025. ICA (18) Geoffrey Irving, Paul Christiano, and Dario Amodei. Ai safety via debate. arXiv preprint arXiv:1805.00899, 2018. JLKK (19) Jisoo Jeong, Seungeui Lee, Jeesoo Kim, and Nojun Kwak. Consistency-based semi-supervised learning for object detection. Advances in neural information processing systems, 32, 2019. KCE+ (24) Jan Hendrik Kirchner, Yining Chen, Harri Edwards, Jan Leike, Nat McAleese, and Yuri Burda. Prover-verifier games improve legibility of LLM outputs. CoRR, abs/2407.13692, 2024. Key (21) John Maynard Keynes. A Treatise on Probability. Macmillan, London, 1921. Kil (92) Joe Kilian. A note on efficient zero-knowledge proofs and arguments (extended abstract). In S. Rao Kosaraju, Mike Fellows, Avi Wigderson, and John A. Ellis, editors, Proceedings of the 24th Annual ACM Symposium on Theory of Computing, May 4-6, 1992, Victoria, British Columbia, Canada, pages 723–732. ACM, 1992. KJPJ (20) Jongmok Kim, Jooyoung Jang, Hyunwoo Park, and SeongAh Jeong. Structured consistency loss for semi-supervised semantic segmentation. arXiv preprint arXiv:2001.04647, 2020. (77) Adam Kalai and Varun Kanade. Towards optimally abstaining from prediction with OOD test examples. In Marc’Aurelio Ranzato, Alina Beygelzimer, Yann N. Dauphin, Percy Liang, and Jennifer Wortman Vaughan, editors, Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NeurIPS 2021, December 6-14, 2021, virtual, pages 12774–12785, 2021. (78) Adam Tauman Kalai and Varun Kanade. Efficient learning with arbitrary covariate shift. In Vitaly Feldman, Katrina Ligett, and Sivan Sabato, editors, Algorithmic Learning Theory, 16-19 March 2021, Virtual Conference, Worldwide, Proceedings of Machine Learning Research, pages 850–864. PMLR, 2021. KM (94) Daphne Koller and Nimrod Megiddo. Constructing small sample spaces satisfying given constraints. SIAM J. Discret. Math., 7(2):260–274, 1994. KN (95) Joe Kilian and Moni Naor. On the complexity of statistical reasoning (extended abtract). In Third Israel Symposium on Theory of Computing and Systems, ISTCS 1995, Tel Aviv, Israel, January 4-6, 1995, Proceedings, pages 209–217. IEEE Computer Society, 1995. Kol (50) A.N. Kolmogorov. Foundations of the theory of probability. Chelsea Publishing Company, 1950. KR (08) Yael Tauman Kalai and Ran Raz. Interactive PCP. In Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir, and Igor Walukiewicz, editors, Automata, Languages and Programming, 35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part I - Track B: Logic, Semantics, and Theory of Programming & Track C: Security and Cryptography Foundations, volume 5126 of Lecture Notes in Computer Science, pages 536–547. Springer, 2008. KT (00) Jonathan Katz and Luca Trevisan. On the efficiency of local decoding procedures for error-correcting codes. In Proceedings of the thirty-second annual ACM symposium on Theory of computing, pages 80–86, 2000. Las (01) Jean B. Lasserre. Global optimization with polynomials and the problem of moments. SIAM J. Optim., 11(3):796–817, 2001. Lev (73) Leonid A. Levin. Universal sequential search problems. Problems of Information Transmission, 9(3):115–116, 1973. Russian original: Problemy Peredachi Informatsii. LFKN (92) Carsten Lund, Lance Fortnow, Howard J. Karloff, and Noam Nisan. Algebraic methods for interactive proof systems. J. ACM, 39(4):859–868, 1992. Luk (01) Thomas Lukasiewicz. Probabilistic logic programming with conditional constraints. ACM Trans. Comput. Log., 2(3):289–339, 2001. Mei (13) Or Meir. Ip = pspace using error-correcting codes. SIAM Journal on Computing, 42(1):380–403, 2013. Mic (00) Silvio Micali. Computationally sound proofs. SIAM J. Comput., 30(4):1253–1298, 2000. MLVW (17) Vahab S. Mirrokni, Renato Paes Leme, Adrian Vladu, and Sam Chiu-wai Wong. Tight bounds for approximate carathéodory and beyond. In Doina Precup and Yee Whye Teh, editors, Proceedings of the 34th International Conference on Machine Learning, ICML 2017, Sydney, NSW, Australia, 6-11 August 2017, volume 70 of Proceedings of Machine Learning Research, pages 2440–2448. PMLR, 2017. MS (23) Saachi Mutreja and Jonathan Shafer. PAC verification of statistical algorithms. In Gergely Neu and Lorenzo Rosasco, editors, The Thirty Sixth Annual Conference on Learning Theory, COLT 2023, 12-15 July 2023, Bangalore, India, Proceedings of Machine Learning Research, pages 5021–5043. PMLR, 2023. Nes (00) Yurii Nesterov. Squared functional systems and optimization problems. In High performance optimization, pages 405–440. Springer, 2000. Nil (86) Nils J. Nilsson. Probabilistic logic. Artif. Intell., 28(1):71–87, 1986. Par (03) Pablo A. Parrilo. Semidefinite programming relaxations for semialgebraic problems. Math. Program., 96(2):293–320, 2003. Par (21) Orr Paradise. Smooth and strong pcps. computational complexity, 30(1):1, 2021. POC+ (23) Joon Sung Park, Joseph C. O’Brien, Carrie Jun Cai, Meredith Ringel Morris, Percy Liang, and Michael S. Bernstein. Generative agents: Interactive simulacra of human behavior. In Sean Follmer, Jeff Han, Jürgen Steimle, and Nathalie Henry Riche, editors, Proceedings of the 36th Annual ACM Symposium on User Interface Software and Technology, UIST 2023, San Francisco, CA, USA, 29 October 2023- 1 November 2023, pages 2:1–2:22. ACM, 2023. Pot (14) Nico Potyka. Linear programs for measuring inconsistency in probabilistic logics. In Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning (KR 2014), pages 568–577, 2014. PS (20) Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. CoRR, abs/2009.03393, 2020. PT (14) Nico Potyka and Matthias Thimm. Consolidation of probabilistic knowledge bases by inconsistency minimization. In Proceedings of the 21st European Conference on Artificial Intelligence (ECAI 2014), pages 729–734. IOS Press, 2014. PY (86) Christos H. Papadimitriou and Mihalis Yannakakis. A note on succinct representations of graphs. Inf. Control., 71(3):181–185, 1986. Ram (31) Frank P. Ramsey. Truth and probability. In R. B. Braithwaite, editor, The Foundations of Mathematics and Other Logical Essays, pages 156–198. Kegan Paul, Trench, Trubner & Co., London, 1931. RH (21) Oliver Richardson and Joseph Y. Halpern. Probabilistic dependency graphs. In Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, Thirty-Third Conference on Innovative Applications of Artificial Intelligence, IAAI 2021, The Eleventh Symposium on Educational Advances in Artificial Intelligence, EAAI 2021, Virtual Event, February 2-9, 2021, pages 12174–12181. AAAI Press, 2021. RHS (23) Oliver E. Richardson, Joseph Y. Halpern, and Christopher De Sa. Inference for probabilistic dependency graphs. In Robin J. Evans and Ilya Shpitser, editors, Uncertainty in Artificial Intelligence, UAI 2023, July 31 - 4 August 2023, Pittsburgh, PA, USA, volume 216 of Proceedings of Machine Learning Research, pages 1741–1751. PMLR, 2023. Ric (22) Oliver E. Richardson. Loss as the inconsistency of a probabilistic dependency graph: Choose your model, not your loss function. In Gustau Camps-Valls, Francisco J. R. Ruiz, and Isabel Valera, editors, International Conference on Artificial Intelligence and Statistics, AISTATS 2022, 28-30 March 2022, Virtual Event, volume 151 of Proceedings of Machine Learning Research, pages 2706–2735. PMLR, 2022. Ric (24) Oliver Ethan Richardson. A Unified Theory of Probabilistic Modeling, Dependence, and Inconsistency. Cornell University, 2024. R (24) Noga Ron-Zewi and Ron Rothblum. Local proofs approaching the witness length. J. ACM, 71(3):18, 2024. RS (96) Ronitt Rubinfeld and Madhu Sudan. Robust characterizations of polynomials with applications to program testing. SIAM J. Comput., 25(2):252–271, 1996. RSS+ (25) Dhruv Rohatgi, Abhishek Shetty, Donya Saless, Yuchen Li, Ankur Moitra, Andrej Risteski, and Dylan J. Foster. Taming imperfect process verifiers: A sampling perspective on backtracking. CoRR, abs/2510.03149, 2025. RSS+ (26) Oliver E. Richardson, Mandana Suso Samiei, Mehran Shakerinava, Joseph D. Viviano, Abdessamad El Kabid, Ali Parviz, and Yoshua Bengio. Local inconsistency resolution: The interplay between attention and control in probabilistic models. In International Conference on Artificial Intelligence and Statistics (AISTATS), 2026. Sch (80) Jacob T. Schwartz. Fast probabilistic algorithms for verification of polynomial identities. J. ACM, 27(4):701–717, 1980. Seb (90) András Sebö. Hilbert bases, caratheodory’s theorem and combinatorial optimization. In Ravi Kannan and William R. Pulleyblank, editors, Proceedings of the 1st Integer Programming and Combinatorial Optimization Conference, Waterloo, Ontorio, Canada, May 28-30 1990, pages 431–455. University of Waterloo Press, 1990. Tha (13) Justin Thaler. Time-optimal interactive proofs for circuit evaluation. In Ran Canetti and Juan A. Garay, editors, Advances in Cryptology - CRYPTO 2013 - 33rd Annual Cryptology Conference, Santa Barbara, CA, USA, August 18-22, 2013. Proceedings, Part I, Lecture Notes in Computer Science, pages 71–89. Springer, 2013. WST+ (24) Stephan Wäldchen, Kartikey Sharma, Berkant Turan, Max Zimmer, and Sebastian Pokutta. Interpretability guarantees with merlin-arthur classifiers. In Sanjoy Dasgupta, Stephan Mandt, and Yingzhen Li, editors, International Conference on Artificial Intelligence and Statistics, 2-4 May 2024, Palau de Congressos, Valencia, Spain, volume 238 of Proceedings of Machine Learning Research, pages 1963–1971. PMLR, 2024. XN (18) S. Xu and King Ngi Ngan. Hierarchical parsing net: Semantic scene parsing from global scene to objects. IEEE Transactions on Multimedia, 20(10):2653–2664, 2018. ZG (24) Jian-Qiao Zhu and Tom Griffiths. Incoherent probability judgments in large language models. In Larissa K. Samuelson, Stefan Frank, Mariya Toneva, Allyson Mackey, and Eliot Hazeltine, editors, Proceedings of the 46th Annual Meeting of the Cognitive Science Society, CogSci 2024, Rotterdam, The Netherlands, July 24-27, 2024. cognitivesciencesociety.org, 2024. Zip (79) Richard Zippel. Probabilistic algorithms for sparse polynomials. In Edward W. Ng, editor, Symbolic and Algebraic Computation, EUROSAM ’79, An International Symposiumon Symbolic and Algebraic Computation, Marseille, France, June 1979, Proceedings, volume 72 of Lecture Notes in Computer Science, pages 216–226. Springer, 1979. ZPIE (17) Jun-Yan Zhu, Taesung Park, Phillip Isola, and Alexei A. Efros. Unpaired image-to-image translation using cycle-consistent adversarial networks. In IEEE International Conference on Computer Vision, ICCV 2017, Venice, Italy, October 22-29, 2017, pages 2242–2251. IEEE Computer Society, 2017.