Skip to content

Checking Leakage Witnesses versus Certifying Bounded Non-Leakage

Sep 2026 · 0 citations
Computer Science

Abstract

When a language-model audit finds no leak, what is needed to certify non-leakage? We study guarantees over a declared prompt domain under an executable leakage criterion and decoding rule. For general bounded polynomial-time evaluators, a supplied leaking execution is polynomial-time checkable, while leak existence is \NP-complete and deterministic certification is \coNP-complete. Exact stochastic certification is $\coNP^{\PP}$-complete at every fixed rational cutoff in $(0,1)$. Restricting the computation can change these bounds. For example, certification is in \coNP\ when all randomness is a terminal draw from an efficiently computed finite probability table. Attention models admit polynomial-time certification when local dependency windows of logarithmic length precede one global head, given deterministic decoding, fixed vocabulary, exact rational weighted means, a direct binary affine readout and finite-automaton prompt domains. A construction with two global layers instead makes certification \coNP-complete over template domains, with one head per layer, polynomial width, logarithmic precision and an inverse-polynomial logit margin. Planted-secret experiments measure what finite audits miss relative to complete references. Among 30 secret--model-state pairs that leak under greedy single-prompt execution on their secret's 4,096-prompt domain, uniformly selecting 256 recorded evaluations per pair misses every leak for an expected $41.06\%$ of these pairs. Batched and single-prompt checks disagree on one complete-domain decision among all 48 fine-tuned pairs, while a same-order repeat reproduces every single-prompt output. These results distinguish computational conditions for certification from the coverage and execution conditions needed to interpret a negative audit.

View source

Similar papers

Preprint Sep 2026

Efficient Branch-and-Bound Testing and Verification of zkVMs

ZEBRA is a fully automated verification and bug-detection framework that reduces zkVM verification to a solution-set cardinality problem over a canonical trace space, where redundancies such as null-row padding and non-deterministic permutations are eliminated prior to counting.

Hideaki Takahashi, Suman Jana, Junfeng Yang · 0 citations
Open access Sep 2026

An engineering reading of the bounded halting problem and observable properties of a universal machine

The halting problem asks whether a program eventually halts, with unrestricted resources. Engineering systems instead certify bounded halting: given a program, an input, and a step budget T, decide whether the program halts within T steps. This paper studies two of its uses. First, it defines an exact finite-budget pro...

Sergey I. Salishev · 0 citations
Preprint Sep 2026

Fresh-Challenge VDF Attestations for Model-Relative Response Latency

Can a finite verifier obtain public, model-relative evidence about response latency for sequential computation? Verifiable delay functions (VDFs) make this possible in principle: evaluation requires T sequential steps, whereas verification is efficient in the security parameter and polylogarithmic in the numerical valu...

Ansar Yesmukhanov, Aruzhan Tlessova · 0 citations
#artificial intelligence Book Open access Sep 2026

Semantic Prefix Oracles for LLM Decoding: Contracts and Differential Validation

Constrained decoding can enforce regular or context-free output formats, but many program-generation failures are semantic: scope, typing, and declaration effects depend on context. We present semantic grammar specifications, a declarative formalism that attaches such constraints to a context-free surface and executes...

Paul Kronlund-Drouault · 0 citations
Preprint Sep 2026

Scaling Zero Knowledge UNSAT Verification via Normalized Chaining

Proofs of UNSAT are a standard primitive in formal verification and software assurance. In many real-world settings, the proof itself encodes proprietary or security-sensitive information, making public disclosure undesirable. Zero-knowledge certification of UNSAT addresses this tension: it enables a prover to convince...

A. Karthikeyan, E. Kharitonov, Kuldeep S. Meel et al. · 0 citations

Related blog posts

MIT News · Artificial Intelligence Sep 24, 2026

Estimating suicide risk from text

A new language-processing tool could help identify the highest-risk individuals from natural language, enabling swifter interventions.

We use cookies to run the site and, with your consent, for analytics and to show ads. See our Cookie Policy.