{"id":"9308b216-ea38-4ee8-a721-83f3a6beb78d","arxiv_id":"2608.11181","paper_version":1,"verdict":"REJECT","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"high","formal_verification":"none","parameter_count":0,"one_line_summary":"Places approximate probabilistic consistency of explicit claims in NP with short certificates, and gives an interactive PCP for circuit-specified predictors, but the main protocol's soundness proof has an unproven step.","lead":"The paper gives new complexity-theoretic results for checking whether a probabilistic predictor's many conditional-probability answers can all hold under one distribution. It shows the explicit version has short proof certificates, and it builds an interactive proof for the circuit-specified version, though the proof of the main soundness claim has a gap.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 32 soundness is unproven: closeness to a Reed-Muller codeword does not imply the oracle is multilinear, and conditioning on point reads cannot restore the degree bounds on which the SumCheck soundness relies.","rationale":"The reader's weakest_assumption is exactly the gap I find: the soundness argument passes from proximity to exactness without accounting for the degree hypotheses in the SumCheck and VerMarginoid lemmas. The paper's own text supports this reading: Algorithm 5 (VerMarginal) is the self-correcting wrapper and is explicitly not used downstream, while Algorithm 6 calls VerMarginoid. The central claim, Theorem 32, depends on this step. The explicit-consistency results in Section 5 and the NEXP-hardness corollary appear to rest on independent arguments and are not affected; nevertheless the headline IPCP is the paper's main contribution, and an unproven soundness step warrants rejection. I therefore keep the reader's REJECT verdict; the path to correction is to replace plain oracle reads with self-corrected ones and rework the SumCheck soundness, or to prove a robust SumCheck for functions close to low-degree.","tokens_in":57406,"tokens_out":7651,"duration_ms":72009,"concrete_test":"Independently re-derive the soundness of Theorem 32 for an oracle that is δ-close to, but not equal to, a valid Rµ codeword. Concretely, set Z = eZ + η·1_{q*} for a single point q* outside the queried points, and write out the Inc†-SumCheck summand F(q) = Q̂(q)·(2^B·μ†[(s=b)∩(t=1)] − P̂(q)·μ†[s=b])^2. Compute the individual degree of F as a function of q; if it exceeds 3Δ+2, or if the two VerMarginoid polynomials exceed ℓ+1, then Fact 22's soundness bound is inapplicable. Then simulate Algorithm 6 on a small instance (ℓ=1, d=1, B=1) with a malicious Prover that sends round polynomials matching F's high-degree extension; if acceptance probability exceeds ε_sound, the concern lands.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The soundness proof of Theorem 32 (Section 8.2, paragraph beginning \"Otherwise π is δ-close to a codeword...\") reduces to the assertion that once all Verifier oracle reads land in the agreement region of a δ-close Reed-Muller codeword, every sub-protocol behaves as if the oracle were exactly that codeword. This is not established. Claim 26, the soundness bound used for VerMarginoid (Algorithm 4), assumes the oracles Z and A are themselves multilinear; Fact 22, used for both SumChecks, assumes the summand has individual degree at most 3Δ+2 (resp. Δ). These degree bounds are global properties of the oracle. A function that agrees with a multilinear function at finitely many queried points can be arbitrary elsewhere, and the resulting summands can have much higher degree. For instance, agree_Z(j,q) is a product of ℓ factors each containing Z(j,s_k), so a single non-multilinear perturbation can add monomials of degree larger than ℓ in the q variables. Conditioning on point queries cannot restore the missing degree bound. The paper defines VerMarginal with self-correction (Algorithm 5, Fact 27) but explicitly says it will not be used downstream, and Algorithm 6 runs the unsupported VerMarginoid in Step 5. Thus the soundness of the main IPCP is unproven.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies whether a circuit-specified probabilistic predictor's conditional-probability claims can be jointly consistent and whether that consistency can be verified efficiently. For explicitly given collections of m probabilistic claims, it proves that ℓ2-approximate consistency has witnesses supported on O(m) points with polynomial-bit rational weights (Prop. 9) and a gapped low-precision variant (Prop. 8), giving NP membership and near-linear certificates. It also proves hardness of approximation for explicit consistency and NEXP-completeness for the succinct model-consistency problem. The main contribution is an interactive PCP (Thm 32) in which a polynomial-time verifier uses a Reed–Muller-like encoding of a sparse witness distribution, sumcheck sub-protocols, and a proximity test to certify model consistency; Theorem 38 delegates circuit evaluations to obtain depth-efficient verifier bounds.","tokens_in":77,"tokens_out":11504,"duration_ms":229238,"significance":"The explicit-consistency results are carefully argued and appear technically sound: the Carathéodory sparsification, the exact rational solve, the determinant bounds, and the prime-certificate trick are convincing and give a meaningful improvement in certificate length. The paper is also commendably explicit about the Reed–µller encoding library and about its limitations, e.g., Remark 36 and Remark 40. If the IPCP soundness were established, Theorem 32 would be a significant first probabilistically checkable proof system for model consistency. However, as detailed below, the soundness proof of the main theorem has a load-bearing gap, so the headline result is not currently proven.","major_comments":[{"comment":"The paragraph beginning \"Otherwise π is δ-close to a codeword\" assumes that once the Verifier's oracle reads land in the agreement region, \"every subprotocol now behaves as if run\" on the nearby codeword. This is not established. Claim 26 and Fact 22 require the oracles to be multilinear, or the summand to have bounded individual degree; a function that agrees with a multilinear function on finitely many queried points can be arbitrary elsewhere, and the degree bound is a global property of the oracle. Algorithm 6 Step 5 calls VerMarginoid, not the self-correcting VerMarginal of Algorithm 5, so conditioning on point queries cannot restore the missing degree bound. Consequently the soundness of Theorem 32, and of Theorem 38 which inherits the same Step 5 and the same analysis, is unproven. Since Theorem 32 is the headline contribution, this is a load-bearing gap.","section":"§8.2, proof of Theorem 32 (soundness case)"},{"comment":"The same issue appears in the proof of Claim 24. In situation (ii), the proof transfers the multilinear-case bound to a δ-close oracle by adding the probability that the SumCheck's final query lands where Z differs from its closest multilinear polynomial Z̃. But SumCheck soundness for the polynomial Z̃ does not apply to an interactive transcript produced by a Prover who sees the actual non-multilinear Z. Relative Hamming closeness does not control the value or degree of Z²−Z off the agreement set, and the final query being an agreement point does not constrain the earlier Prover messages. Thus the soundness bound for VerEnc is not established as written.","section":"§7.2, Claim 24 (non-multilinear case)"}],"minor_comments":[{"comment":"The phrase \"every subprotocol now behaves as if run oneπ\" appears garbled; it should read \"as if run on the nearby codeword eπ\" or similar.","section":"§8.2, proof of Theorem 32"},{"comment":"The illustrative statement that at m=10^6 and B=32 \"a 32-bit number suffices\" for the auxiliary prime is not derived; since the prime length is O(log B_M)=O(log m + log B), a short explanation of the constant would help the reader check the example.","section":"§5.3"},{"comment":"The statement of Claim 17 says the promise problem is NP-hard for all δ∈(0,2^{-k}) and k≥3, but the proof uses the inapproximability results of Håstad, which are typically stated for Exact-kSAT with k≥3 and a specific gap; please clarify that the reduction inherits the exact parameter range of the cited theorems.","section":"§6.2, Claim 17"}],"recommendation":"major_revision","confidential_remarks":"The soundness gap in Theorem 32 is serious and directly affects the paper's central claim. However, the paper already contains the necessary repair tool: VerMarginal with self-correction in Algorithm 5 and Corollary 28. Replacing the VerMarginoid calls in Algorithm 6 with self-corrected variants, or otherwise proving that δ-closeness suffices despite the missing degree bounds, appears to be a feasible revision within the manuscript's scope. For that reason I recommend major revision rather than rejection. The explicit-consistency results in Section 5 are, in my reading, sound and could form a useful standalone contribution if the IPCP part remains unresolved."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The explicit-consistency part is solid and genuinely useful. Proposition 9's certificate-length bound O(mn + log B) for ℓ2 approximate consistency is a real extension of the classical small-model theorems, and the prime-based non-singularity trick is neat. The modeling of consistency via the (P,Q) circuits and the Reed–µller encoding primitive are thoughtful contributions that could be reused by others. If the paper only claimed the NP result and the NEXP-completeness corollary, it would be in good shape.\n\nThe problem is Theorem 32, the headline IPCP. The soundness proof for the case where the oracle is δ-close to a valid codeword does not hold as written. It argues that once all verifier reads land in the agreement region, each sub-protocol behaves as if the oracle were the exact codeword. That is not enough. The soundness of SumCheck (Fact 22) and of VerMarginoid (Claim 26) depends on the summand being a low-degree polynomial in a global sense. A function that merely agrees with a multilinear function at the queried points can have arbitrarily high degree elsewhere, and the summands built from it can carry extra monomials. Conditioning on the queried points cannot restore the degree bound. The paper even defines VerMarginal with self-correction and then says it will not be used downstream; Algorithm 6 runs the unsupported VerMarginoid instead. So the soundness of the main protocol is unproven.\n\nI want to be clear that this is a load-bearing flaw, not a cosmetic one. The main result of the paper is this IPCP, and without the missing soundness argument the construction could be vulnerable to a cheating prover who exploits the non-multilinear tail. That said, the flaw looks fixable: replacing VerMarginoid with VerMarginal (or otherwise self-correcting the oracle reads) would give the required multilinearity with high probability, at a modest cost in query complexity. The authors already have the machinery in the paper.\n\nThis is a paper worth a serious referee. The NP result and the framing are genuinely new, and the IPCP idea is promising even if the proof is currently incomplete. I would recommend sending it to peer review with a clear message to the authors: fix the soundness proof of Theorem 32, most likely by integrating self-correction, and resubmit. I would not cite the IPCP result in its current form, but I would cite the explicit consistency results if I needed them.","headline":"Good NP result, but the main IPCP theorem has a real soundness gap that looks fixable only with self-correction.","tokens_in":123,"tokens_out":2836,"would_cite":false,"duration_ms":57816,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q15","68Q17","03B48"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper constructs an interactive PCP in which a polynomial-time verifier certifies approximate consistency of a circuit-specified probabilistic model by evaluating the model at a few points and reading a few locations of an…","keywords":["probabilistic consistency","interactive PCP","Reed–Muller encoding","sum-check protocol","Carathéodory theorem","NP certificate","predictive model verification","probabilistic claims"],"falsifier":"Take a small explicit model $(P,Q)$ whose consistency is witnessed by a known distribution $\\mu$, write its exact Reed–µller codeword, then corrupt the oracle on a $\\delta$-fraction of coordinates chosen so that every point the verifier's specific random coins select falls in the corrupted set; run Algorithm 6 with a prover claiming a marginal different from $\\mu$'s. If the verifier accepts with probability greater than $\\varepsilon_{\\mathrm{sound}}$ (or if VerMarginoid accepts a false marginal beyond the bound of Claim 26), the closeness-to-codeword substitution in the proof of Theorem 32 is false.","tokens_in":57196,"feed_emoji":"✅","tokens_out":18336,"duration_ms":140152,"temperature":0.7,"pith_summary":"This paper asks whether a probabilistic predictor that implicitly makes exponentially many conditional-probability claims can be certified as self-consistent in polynomial time. The central result is an interactive PCP: given circuits $(P,Q)$ describing the predictor, a polynomial-time verifier evaluates the circuits at a few points, reads a few locations of an exponentially long proof oracle, and interacts with a single untrusted prover to certify approximate consistency up to a tunable additive gap. En route, the paper shows that approximate $\\ell^2$-consistency of $m$ explicit claims lies in NP with $O(mn + \\log B)$-bit certificates, and that a small completeness-soundness gap reduces the certificate to low-precision weights of length $O(m(n + \\log(m/\\varepsilon_{\\mathrm{gap}})))$. If correct, the result turns consistency of a predictive model into a property that can be checked efficiently rather than only estimated by sampling, which matters for AI systems whose safety rests on honest probabilistic claims.","feed_headline":"Certify a predictor's probabilities with a few point reads","feed_subtitle":"Exponentially many conditional-probability claims reduce to a few circuit evaluations plus a short proof oracle.","key_machinery":"The construction is carried by four mechanisms. The Carathéodory witness replaces any distribution by one supported on $m+1$ points with identical $\\ell^2$ constraint residuals, and the squared $\\ell^2$ norm makes the optimal weights on a fixed support the solution of the linear system (5), whose coefficients are bounded via Hadamard's inequality so that the weights have polynomial bit-length. The proof oracle is the Reed–µller encoding, a Reed–Muller (multilinear-extension) code of the support vectors and the binary bits of the weights, which is locally testable and lets the verifier compute marginals through the gadgets $agree$ and $vec2int$. The encoding check (VerEnc) combines a multilinearity test with sum-checks certifying Booleanity and unit measure; the marginal check (VerMarginoid) verifies a field-valued marginal by reducing it to a random point via the SumCheck protocol. Finally, the SumCheck protocol reduces the two exponential sums defining $\\mathrm{Inc}^2$ and $\\|Q\\|_1$ to single point evaluations of the arithmetic circuits $\\hat P, \\hat Q$ and of the oracle.","core_discovery":"On the paper's own terms, the main theorem is that Model-Consistency---given circuits $P$ and $Q$ over a query universe of size $2^{\\ell(d+1)+d}$, is there a distribution $\\mu$ over $n = 2^d$ Boolean variables with $\\mathrm{Inc}_{P,Q}(\\mu) \\le \\tau$---admits a polynomial-time interactive PCP. The verifier's protocol (Algorithm 6) runs one encoding-proximity test, two sum-checks, two marginal checks, and three direct circuit evaluations; it reads only $\\mathrm{poly}(\\ell, d, B, \\log(1/\\varepsilon_{\\mathrm{gap}}), 1/\\varepsilon_{\\mathrm{sound}})$ symbols of an oracle of length $|F|^{O(\\ell d + B)}$ and exchanges polynomially many field elements with a single untrusted prover. The oracle encodes a sparse witnessing distribution, whose existence comes from a Carathéodory argument: any consistent collection of $m$ claims has a witness supported on $m+1$ points, and the paper proves the weights can be taken rational with polynomially many bits (Proposition 8 gives logarithmic-precision weights at the cost of an additive gap; Proposition 9 places the exact version in NP with certificate length $O(mn + \\log B)$, the verifier solving for the weights itself). The completeness guarantee requires the model to be $(\\tau - \\varepsilon_{\\mathrm{gap}})$-consistent, and soundness rejects every model with inconsistency above $\\tau$ except with probability $\\varepsilon_{\\mathrm{sound}}$.","pith_inferences":["The soundness proof's step from 'δ-close to a codeword' to 'behave as the exact codeword' is the spot to test: if it fails, the protocol may still be sound with the self-corrected marginal verifier VerMarginal substituted for VerMarginoid, at a modest cost in queries.","The $\\ell^2$ norm is doing double duty: squaring makes the witness's stationarity conditions linear, so switching to an $\\ell^p$ or entropy-based inconsistency measure would require a new witness bit-complexity analysis.","Because the honest prover must commit to the exact inconsistency value, a learned prover that only estimates would have no accepting strategy; the paper's own suggestion of an approximate sum-check is a concrete place to look for a version that tolerates estimated provers.","A natural experiment is to instantiate Algorithm 6 on a toy model with the explicit honest-prover strategies and check empirically whether a trained circuit can play both oracle and prover roles through context resets."],"forward_implications":["Consistency of a circuit-specified predictor becomes verifiable in polynomial time up to an additive gap, with the verifier evaluating the model circuits at only a few points.","The NP certificate for $m$ explicit claims is of length $O(mn + \\log B)$; introducing a small completeness-soundness gap shortens the stored weights to $O(\\log(m/\\varepsilon_{\\mathrm{gap}}))$ bits each, which is what allows the witness to be written into the proof oracle.","If sound, the protocol guarantees that no untrusted prover can make an inconsistent model appear consistent except with probability $\\varepsilon_{\\mathrm{sound}}$, despite the verifier reading only a few oracle locations.","The Reed–µller library (validity check and marginal verification) is presented as a self-contained primitive that can verify marginals of distributions for purposes beyond consistency checking.","Delegating the circuit evaluations (Theorem 38) replaces the degree dependence with a depth dependence, so the verifier's runtime becomes polynomial in the model size; for uniformly presented circuits it becomes polylogarithmic in the circuit size."],"supporting_citations":[{"why":"Supplies Carathéodory's theorem, which bounds the support of the witnessing distribution by $m+1$ points.","marker":"[Car07]"},{"why":"Supplies the SumCheck protocol that reduces the huge sums over queries to single point checks.","marker":"[LFKN92]"},{"why":"Establishes the two-prover framework and the multilinearity-testing machinery underlying the encoding check.","marker":"[BFL91]"},{"why":"Provides the specific multilinearity tester (Fact 23) with the soundness parameters used by VerEnc.","marker":"[FGL+96]"},{"why":"Defines the Interactive PCP model, the proof-system framework the main protocol is stated in.","marker":"[KR08]"},{"why":"Provides the $q$-adic lifting that lets the NP verifier solve the exact weight linear system efficiently.","marker":"[Dix82]"},{"why":"Supplies the doubly-efficient interactive proof for circuit evaluation used in the delegated version of the protocol.","marker":"[Tha13]"}],"fun_headline_variants":["Interactive PCP verifies probabilistic consistency in polynomial time","Few circuit reads certify exponentially many probability claims","Sparse witness + interactive proof checks predictor self-consistency","Polynomial-time verifier for probabilistic claim consistency"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The soundness proof of the main theorem assumes that a proof oracle which differs from a valid encoding on only a $\\delta$-fraction of points can be treated as that exact encoding whenever the verifier's random reads avoid the differing points; the cited soundness lemmas do not prove this, because they assume the oracle is already the exact polynomial that is linear in each coordinate.","fun_headline_variants_meta":{"raw":{"variants":["Interactive PCP verifies probabilistic consistency in polynomial time","Few circuit reads certify exponentially many probability claims","Sparse witness + interactive proof checks predictor self-consistency","Polynomial-time verifier for probabilistic claim consistency"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000452,"raw_usage":{"total_tokens":2409,"prompt_tokens":1210,"completion_tokens":1199,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":826,"completion_tokens_details":{"reasoning_tokens":1137}},"tokens_in":826,"tokens_out":1199,"duration_ms":8241,"temperature":1.0,"reasoning_tokens":1137,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T04:33:39.489830+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a small explicit model $(P,Q)$ whose consistency is witnessed by a known distribution $\\mu$, write its exact Reed–µller codeword, then corrupt the oracle on a $\\delta$-fraction of coordinates chosen so that every point the verifier's specific random coins select falls in the corrupted set; run Algorithm 6 with a prover claiming a marginal different from $\\mu$'s. If the verifier accepts with probability greater than $\\varepsilon_{\\mathrm{sound}}$ (or if VerMarginoid accepts a false marginal beyond the bound of Claim 26), the closeness-to-codeword substitution in the proof of Theorem 32 is false.","supporting_citations":[],"review_version":1}