验证与迁移：精确信息前沿及调用代价

验证器只能接受或拒绝整个答案，这种粗粒度的反馈在信息效率上存在先天局限。一篇来自 arXiv 的论文《Verification with Transfer: Exact Information Frontiers and Their Price in Calls》用信息论工具给出了一个精确的「信息前沿」，并系统量化了通过源任务迁移来降低验证代价的可行边界。

问题起点：整答案验证的信息瓶颈

在 k 位答案的均匀先验下，若验证器只能对完整答案给出通过/拒绝的二元反馈，要实现零错误验证，最坏情况下需要 2^k - 1 次验证。这一结论直接点明了「整答案验证」的根本困境：当答案空间稍大，暴力验证在信息上就变得不可承受。

论文将「迁移」视为突破这一瓶颈的自然手段——求解相关的源任务，再将其结果用于目标验证。迁移有两种典型编排：像课程学习那样先把所有源任务全部解决，或把源调用与验证交错进行。两种编排在信息上的优劣，此前缺乏精确刻画。

信息前沿：一个列表率失真函数

论文的核心贡献是给出了精确验证器下、任意源调用与 n 次验证交错协议要达到成功概率 s 所需的「最小因果信息」——它是一个列表率失真函数（list rate-distortion function）。这个函数给出了一个下界：在任意验证之前先做一次观测即可达到该前沿，且该前沿下界了期望二元源调用次数。

对设计良好的源，唯一答案场景下该界可以被逼近到 1 + log₂5 次调用以内；一般情形下差距只是一个对数项，但论文指出不存在可加的常数项界。这一结果将「迁移能省多少」从一个经验问题提升为可计算的信息论量。

率失真函数（rate-distortion function） 是香农信息论中的核心工具，描述在允许一定失真水平 D 的前提下，为表示一个信源所需的最小信息率 R(D)。经典形式针对有损压缩：给定信源分布和失真度量，R(D) 刻画了压缩率与重建质量之间不可逾越的权衡曲线。本文将其推广到「列表」形式——输出不再是一个重建点，而是一个候选列表，成功与否取决于正确答案是否落在列表中。这一改动直接匹配了验证场景：验证器不必精确重建答案，只需判断某个候选是否被接受。列表率失真函数因此天然刻画了「在 n 次二元验证反馈下，要达到成功概率 s 所需的最小因果信息量」，成为量化验证信息代价的精确标尺。

交错还是先源：精确与噪声验证器下的分岔

在精确验证器与固定源的设定下，论文证明了一个反直觉的结论：把所有调用都挪到第一次验证之前，能保持所有关于调用次数的硬上限。换言之，交错执行并不能突破硬上限，尽管它在期望调用次数上可能节省无限多。

但这一图景在噪声验证器下完全改变。论文显示，源优先协议在信息量与误差上可能损失无界因子。这说明「先跑源任务」这一课程式直觉在噪声验证场景下并不安全，验证器的噪声特性会实质性改变最优迁移策略的结构。

硬上限（hard bound）与期望次数 的区分是理解本节反直觉结论的关键。硬上限指协议在最坏情况下消耗的调用次数上界，即对任何源实现和任何答案都必须满足的保证；期望次数则是对随机源取平均后的调用数。交错执行之所以能在期望次数上「节省无限多」，是因为它可以在部分验证反馈显示答案已排除后提前终止，避免为已无效的假设继续调用源。但当要求对所有输入都给出确定性保证时，交错的提前终止优势消失——因为最坏情况下必须为所有可能性做好准备，而这等价于把所有调用一次性前置。噪声验证器则破坏了「一次先验观测即可对齐前沿」的前提，因为单次源信息在噪声下可能被误读，源优先协议无法通过后续验证反馈纠正，导致信息与误差的无界损失。

线性源库：闭式解与可计算预算轮廓

针对 F₂ 上的线性源库，论文给出了最优精度的闭式表达。进一步，经过多项式时间归约，预算轮廓可以在 2^{O(h²)}·poly(J, k+h) 时间内计算，其中 J 为源数量、h 为干扰维度。

在这一结构下，硬上限约束下的零误差验证有一个清晰的会计解释：超出「四舍五入后的信息价格」的调用次数，恰好等于花在干扰维度上的调用。这把「干扰维度」从一个抽象参数变成了可度量的调用开销。

F₂ 上的线性源库 指源任务的解空间取二元域 F₂（即 {0,1} 上的模 2 运算），且各源之间的关系由线性代数结构约束。选择 F₂ 的优势在于：答案位可视为向量，源调用等价于对某些位施加线性约束（如 XOR），验证则可视为检验某向量是否满足一批线性方程。这一设定下，信息前沿退化为关于向量空间维数的线性代数问题，从而允许写出闭式解。「干扰维度」h 指源库中与目标答案无关但仍占据调用预算的自由度——它们不帮助判定目标，却消耗调用次数。多项式时间归约表明，预算轮廓的计算复杂度主要由 h 主导，呈 2^{O(h²)} 增长，这意味着只要干扰维度受控，预算计算对源数量 J 和目标位数 k 都是多项式可处理的。

机器验证与实证校准

论文所有带编号的结果，除关于规划者的两个条款外，均在 Lean 4 中机器验证，前提是引用两个已发表结果。这种形式化程度在信息论与验证交叉领域较为少见，为结论提供了较强的可信度。

论文还把信息前沿当作一把「尺子」用于实证：在固定训练预算下，一个小型 Transformer 在潜维度为 5 时使用了全部交付比特，而在潜维度为 11 时则完全不用。另一项在训练前记录预测的测试表明，目标比特的低 XOR 度并不足以保证这些比特会被使用。这两项观察提示，模型对交付信息的利用能力与潜维度、目标函数结构之间存在非平凡的耦合。

Lean 4 是一种交互式定理证明器，同时也可作为函数式编程语言使用。在 Lean 4 中形式化数学结论，意味着每一条定理都被展开为机器可检查的证明项，任何逻辑跳步或隐含假设都会被编译器拒绝。本文作者将信息论结论——包括前沿函数的下界、交错协议的硬上限保持性、线性源库的闭式解等——编码为 Lean 4 定理，仅依赖两个已发表结果作为外部公理。这种做法的价值在于：信息论证明常涉及概率与极限的细腻操作，人工审阅易漏掉边界条件，机器验证则提供近乎零容错的保障。在信息论与验证交叉领域，如此大规模的形式化尚属罕见，为结论的可靠性设定了高标准。

结语

这项工作把「验证—迁移」系统的信息代价与调用代价放在同一框架下精确刻画，给出了前沿函数、下界、闭式解与可计算预算轮廓，并以 Lean 4 形式化加固。对设计验证协议、课程式训练流程以及评估模型「是否真的在用交付信息」的研究者而言，这套工具提供了一把可操作的标尺。