KV 缓存：证明复用，检查位置与窗口

前置与本章要闭合的问题

第一章只说明缓存能减少重复工作，尚未证明复用后的函数相同。本章以前缀固定、权重固定、推理模式关闭 dropout 为前提，研究普通因果解码器。每层的键和值分别记为 $K^{(l)}$、$V^{(l)}$，层号 $l=1,\ldots,N$。键和值不是原始词元，也不是最终隐藏状态，而是该层输入经归一化与线性投影得到的张量。不同层不能共用一份缓存，修改权重后也不能继续使用修改前的缓存。

项目复制了本地 Transformer 实战的模型实现到 vendor 内部，下载目录可以独立运行。模型接口为 forward(tokens, targets=None, past_key_values=None, use_cache=False)，输出字典包含 logits、loss、past_key_values。tokens 是形状为 $[B,T]$ 的整数编号，返回 logits 为 $[B,T,V]$。缓存是每层一对 K、V 构成的元组，每个张量形状为 $[B,h,L,d_h]$，其中 $L$ 为旧前缀长度、$h$ 为头数、$d_h=d/h$。外部调用者必须维持这份缓存的前缀身份。

逐层证明旧位置为何不变

从输入层开始，旧位置的词元与绝对位置编号不变，所以其嵌入不变。假设某层输入在所有旧位置均与原前缀计算相同，逐位置的归一化以及 Q、K、V 投影也相同。对旧查询位置 $i$，因果 mask 只允许键位置 $j\leq i$，新追加的词元不在其可见集合内。因此打分、softmax 和加权结果与原计算相同；逐位置前馈和残差也不改变此结论。按层归纳，所有旧位置在全部层的 K、V 均可复用。证明依赖因果可见集合，并不适用于能看未来的双向注意力。

新查询仍必须计算。令旧前缀长 $L$，新块长 $S$，新块局部查询编号为 $r=0,\ldots,S-1$，其全局位置是 $L+r$。拼接后的键位置编号为 $j=0,\ldots,L+S-1$，合法条件为 $j\leq L+r$。因此新块第一行能看全部旧键和自己的键，不能看新块后面的键。若直接创建一个从零开始的 $S$ 行下三角矩阵，会错误地屏蔽旧前缀中的多数位置。单词元测试往往掩盖此类多块索引错误，所以测试必须包含长度大于一的新块。

完整算例一：两旧词元后追加两词元

设旧前缀长二、新块长二，拼接键共有四个。新块第一行全局位置二，其可见键为零、一、二；第二行全局位置三，四个键均可见。若所有合法打分都为零，第一行概率是三项各三分之一，第二行是四项各四分之一。取值向量的一个分量依次为一、二、三、四，则两个输出分别为二与二点五。错误的局部下三角只会给出一与一点五。此算例不依赖随机权重，能直接定位 mask 偏移，而非只观察一个很小的最终误差。

import math
old, new = 2, 2
values = [1.,2.,3.,4.]
outputs=[]
for r in range(new):
    legal=[j for j in range(old+new) if j<=old+r]
    outputs.append(sum(values[j] for j in legal)/len(legal))
assert outputs==[2.,2.5]
wrong=[sum(values[:r+1])/(r+1) for r in range(new)]
assert wrong==[1.,1.5] and wrong!=outputs
print(outputs, wrong)

数值等价检查要对齐输出切片。把完整序列分为四、一、七、十二个词元逐块输入时，第二次调用只返回当前一词元的 logits；参考端却计算前五词元。应比较参考的第四到第四位置，而不是比较两个张量的末端之外的区域。项目 chunks 按累计 cursor 和 stop 取参考切片，逐块比较全部新位置，再返回最大绝对误差。固定双精度、批量二、总长二十四的实测最大误差为 $2.22\times10^{-16}$，属于浮点重排量级，不要求逐比特相等。

from lab import make_model,tokens,chunks
model=make_model()
error,past=chunks(model,tokens(24,2),[4,1,7,12])
assert error<1e-10
assert len(past)==2 and past[0][0].shape==(2,4,24,8)
print(error)

缓存身份不是张量形状

结构检查可以发现头数、层数、设备或长度不一致，却无法识别同样长度的错误内容。将另一段两词元前缀产生的缓存接到当前第三词元，形状完全合法，但条件概率已经变成另一段历史。项目 test_wrong_prefix_negative_control 明确要求这种替换导致可检测差异，防止一个“根本没用缓存”的伪实现也通过正例。实际服务应把请求身份、模型版本、位置策略和前缀内容的对应关系保存在调度状态中；缓存张量自身不包含可校验的原始文本身份。

缓存的批维也有身份语义。若批次第一行完成，第二行的缓存移到第一行，新请求加入第二行，就必须同步移动每层 K、V、已处理长度及请求编号。只重排 tokens 会把其他人的历史接到当前请求。项目不实现真实多请求张量调度，第四章只做离散模拟，因此不会把模拟器称为支持可变长度缓存的服务端。把能力边界写清楚，也是对缓存正确性证明的保护：证明只覆盖调用者实际维持的前缀关系。

完整算例二：窗口满后为什么不能只删最左边

本模型使用长度 $C$ 的可学习绝对位置嵌入，允许位置零到 $C-1$。取 $C=4$，处理词元 a、b、c、d 后缓存长四。下一步参考协议把窗口变成 b、c、d、e，四者重新占位置零、一、二、三。旧缓存中 b 曾位于一，它的输入位置向量与新协议中的位置零不同；更深层的 b、c、d 还混合过已离开窗口的 a。删掉 a 的 K、V 既没有重算位置，也没有消除历史混合，因此通常不等于重建窗口。

项目采用保守而明确的处理：窗口未满时正常增量；已满后每一步取最近 $C$ 个输入，从位置零重新前向并建立新缓存。长度十三、窗口八时，在第九至第十三步共重建五次，缓存路径与每步窗口参考的最大误差实测为 $1.67\times10^{-16}$。这是一种定义清楚的截断上下文函数，不等于无限上下文模型，也不具有窗口满后恒定单查询的成本优势。超过窗口直接传入模型会抛出异常，实验台没有悄悄绕过位置上界。

第二类独立检查是协议检查：除数值正例，还验证溢出确实拒绝、错误前缀确实失败、重建次数与长度差一致。改变一个未来词元不应影响此前位置输出，这是因果性的另一种性质测试；它比只比较两套可能共享同一 mask 错误的实现更独立。本课的十项测试覆盖主要缓存边界，但没有穷尽所有批次重排和设备情形。GPU、可变长度真实批处理以及 RoPE 的窗口策略应另建参考与测试，不能沿用绝对位置的证明结论而不检查前提。

误差阈值与存储实现也属于契约

本实验使用双精度和绝对、相对容差各 $10^{-10}$，因为小模型主要用来检查结构，而不是模拟常见半精度吞吐。绝对误差限制接近零的分量，尺度较大时相对误差限制比例；仅用相对误差会在参考接近零时不稳定。若迁移到半精度，归约顺序、舍入和内核都可能改变误差，应先估计合理范围并保持故障负对照的可分离性，不能看到失败后随意把阈值放大到通过。缓存数学等价是实数层面的推导，有限精度相近是额外的实验结论。

还有一种独立边界是缓存如何增长。当前教学实现通过拼接旧 K、V 与新 K、V 得到更长张量，逻辑上避免旧投影，却可能每步复制旧缓存。单步复制随长度增加，累计复制量也会增长。预分配连续缓冲区或分页寻址可以改变这些存储开销，但同时增加容量、索引、回收和批次身份管理的证明义务。因此本项目不将“存在缓存”写成“已实现最优缓存分配器”，也不把逻辑元素数量直接当作进程峰值内存。第三章只把实际持有张量与公式逐项对齐。

最后检查输出的条件关系：固定后续输入轨迹会让缓存与参考始终看到同一串词元，适合隔离执行误差。若各自采样，一处很小的分布差异可能抽到不同词元，之后前缀已经不同，再比较末尾 logits 就失去了等价问题的共同输入。生成体验测试可以保留，但必须另记种子、采样规则、并列处理和停止原因；它不能替代此处的强制相同前缀测试。

练习与项目增量

本章项目增量是 chunks 与 rolling 两条参考路径及负对照测试。后继空间账本使用实际返回的每层缓存，不从模型名字猜容量；后继计时只在相同输入和窗口内比较，并先通过本章误差阈值。这样“更快”建立在同一函数之上，而量化章节将故意改变函数，并使用另一套近似质量标准。