带迁移的验证：精确信息前沿及其调用代价
Verification with Transfer: Exact Information Frontiers and Their Price in Calls
浏览论文内容
中文总结 AI 辅助
该研究探讨带迁移的验证的精确信息前沿与调用代价，提出列表率失真函数等理论，在F₂线性库中给出闭式解，结果经Lean 4机器验证，为Transformer训练提供标尺。
中文摘要 AI 辅助
接受或拒绝完整答案的验证器作用有限：在对k位答案的均匀先验下，零错误需要2^k-1次验证。常用的解决方法是求解相关的源任务，要么全部先求解（如课程学习），要么与验证交错进行。我们从信息和调用两方面对该解决方法进行定价。对于精确验证器，源调用与n次验证的任何交错操作要以概率s成功所需的最小因果信息是列表率失真函数，该函数在任何验证前进行一次观测即可达到。它对二进制源调用的期望次数给出了下界，对于唯一答案，设计的源在1+log₂5次调用内即可达到该下界；对于一般情况，需在对数项内达到，无法用加性常数满足。对于精确验证器和固定源，将所有调用移到第一次验证前可保留所有调用的硬上限，尽管交错可节省无限多的期望调用；对于噪声验证器，源优先协议会在信息和错误方面损失无限多的因子。对于有限域F₂上的线性库，最优精度有闭式形式，经过多项式时间归约后，预算曲线可在时间2^{O(h²)}poly(J,k+h)内计算，其中J为源数量，h为干扰维度。在这些库中，对于硬上限下的零错误，超出向上取整信息价格的调用恰好是用于干扰的调用。除了关于规划器的两个条款外，所有编号结果均在Lean 4中进行了机器验证，假设两个已发表结果成立。作为标尺，该前沿显示，在固定训练预算内，小型Transformer在潜在维度5处使用所有传递的位，在潜在维度11处不使用任何位；在训练前记录预测的测试中，目标位的低异或度不足以用于其使用。
英文摘要
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.
