Verification with Transfer: Exact Information Frontiers and Their Price in Calls

arXiv:2610.12211v1 Announce Type: new Abstract: A verifier that accepts or rejects whole answers reveals little: under a flat prior over $k$-bit answers, zero error needs $2^k-1$ verifications. The usual remedy is to solve related source tasks, either all first, as a curriculum does, or interleaved with verification. We price this remedy in information and in calls. With an exact verifier, the least causal information that any interleaving of source calls and $n$ verifications needs to succeed with probability $s$ is a list rate-distortion function, attained by one observation before any verification. It lower-bounds the expected number of binary source calls, which designed sources meet within $1+\log_25$ calls for unique answers and within a logarithmic term in general, where no additive constant suffices. With an exact verifier and fixed sources, moving every call before the first verification preserves all hard caps on calls, although interleaving can save unboundedly many expected calls; under a noisy verifier, source-first protocols can lose unbounded factors in information and in error. For linear banks over $\mathbb{F}_2$, optimal accuracy has a closed form, and after a polynomial-time reduction the budget profile is computable in time $2^{O(h^2)}\operatorname{poly}(J,k+h)$ for $J$ sources and nuisance dimension $h$. In these banks, for zero error under a hard cap, the calls beyond the rounded-up information price are exactly those spent on nuisance. Every numbered result apart from two clauses about the planner is machine-checked in Lean 4, assuming two published results. Used as a ruler, the frontier shows a small transformer using all delivered bits at latent dimension $5$ and none at $11$ within fixed training budgets; in a test with predictions recorded before training, low XOR degree of the target bits did not suffice for their use.

Abstract:A verifier that accepts or rejects whole answers reveals little: under a flat prior over $k$-bit answers, zero error needs $2^k-1$ verifications. The usual remedy is to solve related source tasks, either all first, as a curriculum does, or interleaved with verification. We price this remedy in information and in calls. With an exact verifier, the least causal information that any interleaving of source calls and $n$ verifications needs to succeed with probability $s$ is a list rate-distortion function, attained by one observation before any verification. It lower-bounds the expected number of binary source calls, which designed sources meet within $1+\log_25$ calls for unique answers and within a logarithmic term in general, where no additive constant suffices. With an exact verifier and fixed sources, moving every call before the first verification preserves all hard caps on calls, although interleaving can save unboundedly many expected calls; under a noisy verifier, source-first protocols can lose unbounded factors in information and in error. For linear banks over $\mathbb{F}_2$, optimal accuracy has a closed form, and after a polynomial-time reduction the budget profile is computable in time $2^{O(h^2)}\operatorname{poly}(J,k+h)$ for $J$ sources and nuisance dimension $h$. In these banks, for zero error under a hard cap, the calls beyond the rounded-up information price are exactly those spent on nuisance. Every numbered result apart from two clauses about the planner is machine-checked in Lean 4, assuming two published results. Used as a ruler, the frontier shows a small transformer using all delivered bits at latent dimension $5$ and none at $11$ within fixed training budgets; in a test with predictions recorded before training, low XOR degree of the target bits did not suffice for their use.

46 pages, of which 8 pages main text. The Lean 4 formalization is in the ancillary files

Machine Learning (cs.LG); Cryptography and Security (cs.CR); Information Theory (cs.IT); Machine Learning (stat.ML)

arXiv:2610.12211 [cs.LG]

(or arXiv:2610.12211v1 [cs.LG] for this version)

https://doi.org/10.48550/arXiv.2610.12211 Focus to learn more arXiv-issued DOI via DataCite (pending registration)

lean/VerificationTransfer.lean

lean/VerificationTransfer/AlmostSure.lean

lean/VerificationTransfer/Attain.lean

lean/VerificationTransfer/Basic.lean

lean/VerificationTransfer/Benchmark.lean

lean/VerificationTransfer/Calls.lean

lean/VerificationTransfer/CallsAlphabets.lean

lean/VerificationTransfer/CallsUnique.lean

lean/VerificationTransfer/Coding.lean

lean/VerificationTransfer/Converse.lean

lean/VerificationTransfer/Cor11Bank.lean

lean/VerificationTransfer/Duality.lean

lean/VerificationTransfer/FixedSources.lean

lean/VerificationTransfer/Frontier.lean

lean/VerificationTransfer/FrontierExamples.lean

lean/VerificationTransfer/Graph.lean

lean/VerificationTransfer/Interleave.lean

lean/VerificationTransfer/Linear.lean

lean/VerificationTransfer/LinearExtras.lean

lean/VerificationTransfer/Model.lean

lean/VerificationTransfer/NoisyConverse.lean

lean/VerificationTransfer/NoisySep.lean

lean/VerificationTransfer/Paper.lean

lean/VerificationTransfer/Prelim.lean

lean/VerificationTransfer/RankLaw.lean

lean/VerificationTransfer/Remaining.lean

lean/VerificationTransfer/SFRL.lean

lean/VerificationTransfer/ZeroError.lean

lean/axioms_report.txt

lean/lake-manifest.json

lean/lakefile.toml

lean/scripts/AxiomsReport.lean

(31 additional files not shown) You must enabled JavaScript to view entire file list.

arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.

Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.

Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.

aiqbench analysis

Verification with Transfer: Exact Information Frontiers and Their Price in Calls

Related coverage