RAG 的分块方案几乎都只在一份静态语料上比较，可知识库里的文档一直在改。每个块单独编码成向量，一次编辑如果让块边界移动，边界两侧的块就成了新的编码输入，哪怕里面的字一个没改。这篇 6 页的短文专门测量这笔更新成本：作者取 120 对相邻版本的中英文维基百科条目，规定只有块的完整编码输入和旧版本逐字节相同才复用旧向量，用冻结的 BGE-M3 编码器比较三种分块方式。在三种方法都跑通的 116 篇条目上，不重叠的固定长度切块要重算新版本 57–68% 的编码输入，段落优先的递归切块 38–56%，内容定义切块（CDC）43–54%；而在 2048 token 的检索预算下，三者的证据召回率在同一种语言内相差不到 2 个百分点。固定长度切块在插入点之后整体平移，后面的窗口没有一个能和旧版本对上，这是它重算最多的原因。递归切块和 CDC 谁更省，则会随块长参数变化而互换。

1. 为什么要测更新成本

一个英文条目只改了 0.13% 的文字，固定长度切块重算了 49% 的编码输入，段落优先切块只重算了 8%。这个例子来自论文的数据集，它说明编辑量和重算量可以差得很远，差距由切块规则决定。

对一个持续更新的知识库，重算量直接对应编码计算量和向量索引的写入量。以往的分块评测只比检索质量，两个检索质量相当的方案，更新成本可以差很多：本文英文条目上，固定长度切块的平均重算比例是段落优先切块的 1.5 倍（57% 对 38%）。作者想回答三个问题：三种分块方式各要重算多少；重算多少由编辑大小、编辑位置还是切点规则决定；重算少的方案是不是检索质量也更差。

2. 测量方法

复用规则很严格：一个块的完整编码输入（文本加编码器的特殊 token）必须和旧版本里某个块的输入逐字节相同，才能复用旧向量，差一个字符就算新输入。缓存只包含同一篇文档的上一个版本，不跨文档匹配。重算比例的定义是：
$$R_c=\frac{{\sum }_{x\in M_c}T(x)}{{\sum }_{x\in U_c(D_{\mathrm{new}})}T(x)}$$
其中 $U_c(D_{\mathrm{new}})$ 是分块方法 $c$ 在新版本上产生的所有不重复编码输入，$M_c$ 是其中在旧版本缓存里找不到的那部分，$T(x)$ 是块 $x$ 的输入 token 数。$R_c=0$ 表示全部复用，$R_c=1$ 表示全部重算。作者还做了一个空编辑对照：同一个版本切两次，$R_c$ 必须是 0，否则算流水线故障。

三种分块方式都只看当前版本和固定参数，不看旧版本的切法：

• 固定长度切块：按 token 贪心切出最多 304 个 token 的不重叠窗口。
• 递归切块：一段文字超过 400 token 的目标长度就切开，优先在空行处切，其次是换行，再次是句末标点，都不行才退回固定窗口，然后把小单元贪心地拼到不超过目标长度。
• CDC：用 Steadlith 实现，对词序列计算 Rabin 滚动指纹，指纹满足条件的位置就是切点，块长限制在 176 到 352 token 之间。这种方法原本用于文件系统去重，切点只取决于附近的内容，所以文件前面插入字节不会让后面的切点移动。

三种方法的块长参数事先调过，让中位块长接近（实际最大比值 1.17）。

检索质量这样测：每篇条目配两个问题，共 240 个问题，人工在每个版本上标出能回答问题的字符区间。检索时把一批条目放进同一个候选池，按点积排序，把整块按名次放进 2048 token 的预算，预算内的块覆盖了一组完整证据就记召回为 1。

3. 实验

3.1 主结果：固定长度切块重算最多，召回率差别很小

这组实验回答三种方法各要重算多少、检索质量是否有差别。做法是在 116 篇三种方法都跑通的条目上，用固定参数统计平均重算比例和证据召回率（论文 Table I）：

按篇配对比较，递归切块比固定长度少重算 12.7 个百分点（中文，95% 区间 −19.7 到 −6.2）和 19.6 个百分点（英文）；CDC 比固定长度少 14.4 和 14.7 个百分点。召回率的配对差在 −1.9 到 +0.9 个百分点之间，区间都包含或贴着 0。作者明确说，这些区间不能排除召回率下降，也不能证明两者等价，所以不按召回率给方法排名。

中文上递归切块的优势比英文小，原因在切点规则：中文句末标点后面通常没有空格，过长的中文段落切不到句子边界，只能退回固定窗口。

编辑越小，差距越明显。28 篇小编辑（编辑量不超过 5%）的英文条目上，固定长度平均重算 46%，递归 25%，CDC 27%；23 篇小编辑中文条目上是 62%、45% 和 36%。编辑量超过 50% 时，三者都要重算六到九成。

3.2 编辑位置：为什么固定长度切块重算这么多

这组实验检验“边界平移”是不是重算的主要来源。做法是只改一个变量：同样 1% 的插入，放在文章开头、中间或结尾，其余不变。结果：固定长度切块从文首插入时的 100% 降到文末插入时的约 12%，因为插入点之后的每个窗口都向后平移了插入的长度，下游没有一个块能复用。递归切块和 CDC 在三个位置都低于 30%，段落分界和内容指纹切点在编辑后很快重新对齐。

作者还做了一个逐字核对：重算的输入里，有多少文字其实原样存在于旧版本中。英文条目上，固定长度切块重算的 token 有 50% 是旧版本里原样有的文字，CDC 是 33%，递归切块是 12%（中文分别是 47%、45%、37%）。这部分文字一个字没改，只是被切到了不同的块里，所以重算它们完全是切点规则造成的。

3.3 递归切块和 CDC 谁更省，取决于参数

这组实验检验两种内容感知方法的排序是否稳定。做法是不重新调参，把每种方法的目标块长在 256 到 496 token 之间取 6 档，在中位块长比值不超过 1.15 的配对设置下比较。结果：CDC 减递归的重算差在英文上从 −2.4 到 +6.2 个百分点，中文上从 −0.7 到 +5.5，两种语言里都出现正负翻转。例如英文上把递归切块的目标长度从 400 提到 448，重算比例从 37.9% 升到 46.2%，同样 448 的 CDC 是 43.8%。原因是递归切块会把多个小段落拼成一块，一处编辑改变某段长度后，后面几段的拼法可能跟着变，目标长度越大，这种连锁变化传得越远。固定长度切块在所有设置下都是重算最多的。

作者在 arXivEdits 论文修订数据上又核对了一次成本：固定长度、递归和 CDC 的平均重算比例分别是 94.5%、81.4% 和 80.2%，固定长度仍然最高。这个数据集的文本抽取噪声没有量化，所以只作为成本的旁证。

3.4 重叠窗口不是解法

常见的补救办法是让相邻固定窗口重叠 32 或 64 个 token。结果是重算比例和不重叠时相差不到 1.3 个百分点，编码输入总量多了 10–26%，英文召回率还降了 3.0 和 3.9 个百分点，因为重复的文字占用了 2048 token 的检索预算。

4. 局限

作者列出的局限：只有维基百科一个来源；240 个问题的标注没有多人独立裁决，作者自己抽查 60 个标签，有 57 个一致；三种方法的中位块长比值是 1.17，超过了预设的 1.15；只用了一个编码器；同类方法 KARA 没有运行。CDC 在 4 篇中文条目上失败，原因是 CDC 按空格分词，一长串没有空格的中文被当成一个 403–550 token 的单元，超过了 352 的上限。

另外两点需要注意。第一，116 篇里有 105 篇三种方法都找回了全部证据，召回率普遍在 95% 以上，接近天花板，这个检索设置区分不出方法间的细小质量差别。第二，重算比例衡量的是编码输入量，没有换算成延迟或费用；如果编码在整个更新流程里只占小头，比如索引重建或审核更贵，这几十个百分点的差距在总成本里会被摊薄。

5. 实践意义

一是知识库如果频繁小幅修改，不要用不重叠的固定长度切块。换成段落优先的递归切块，英文条目的平均重算比例从 57% 降到 38%，小编辑条目从 46% 降到 25%，检索召回率基本不变。前提是用逐字节相同的输入做缓存键，只要文本没变就复用向量。

二是评测分块方案时，把重算比例和检索质量一起报告，并在自己的块长参数下实测。递归切块和 CDC 的排序会随参数翻转，论文里任何一个排名都不能直接搬用。中文语料要注意切点规则是否依赖空格，否则递归切块会退回固定窗口，CDC 会直接失败。

Mathlib 是 Lean 证明助手的数学库，里面收录了大量定理和定义，写证明的人和编码智能体都要先在里面搜到合适的定理。真实的搜索查询很短：人写的查询中位长度 16 个 token，智能体写的 15 个；而以往检索器训练用的定理自然语言复述，中位长度是 82 个 token。短查询会省略很多意图，同一句话可能对应好几条相近的定理。Lean Finder V2 从两头解决这个问题。模型一侧，作者用强化学习训练一个查询生成器，专门为每条定理写当前检索器排不准、但意思仍然对得上的短查询，用这些查询训练检索器，再用新检索器给生成器打分，交替两轮，共得到 60 多万对查询和定理。输入一侧，作者用 GEPA 自动优化一个改写提示词，在检索前把用户的短查询改写得更明确。在 810 条人写短查询组成的 MathlibQR 上，Lean Finder V2 的 Recall@10 是 0.893，此前最好的检索加重排系统是 0.780。消融实验里，只奖励“难”、不检查查询和定理是否一致时，排名最靠前的几项指标反而低于不用合成数据，因为生成器会学到写偏题的查询来制造难度。

1. 短查询为什么难搜

论文举了一个例子：目标是 Mathlib 里“常函数是偶函数”这条定理。用完整描述去搜（写明类型、函数形式和 f(−x)=f(x)），目标排第 1；换成同义的短查询“常函数在输入取负时不变”，目标掉到第 7，因为短查询没有点出 Mathlib 使用的“偶函数”这个概念。这类查询在实际使用中很常见，作者统计了 2 万条人写查询和 10 万条智能体查询，长度分布都集中在 15 个 token 左右。以往的检索器在定理的长复述上训练，学会的是逐条匹配详细描述，遇到短查询就分不清几条相近的候选。

2. 方法

2.1 初始检索器

检索器从 Qwen3-Embedding-8B 出发，用对比学习微调：每个查询和它对应的定理是正样本，同一批里的其他定理是负样本。Mathlib 里很多定理彼此相近，作者把余弦相似度比正样本还高出一个阈值 $m$ 的候选从负样本里去掉，避免把其实也对的定理当成错的去惩罚。初始训练数据是已有的长复述和合成查询，这一步得到第 0 轮检索器。

2.2 用强化学习生成难查询

查询生成器是 Qwen3-4B，用 GRPO 训练（一种按同组采样结果的相对好坏更新策略的强化学习方法）。每条定理生成一个短查询，奖励是：
$$r=\max \{0,j(q,d)\cdot f_{\mathrm{rank}}(k)-{\lambda }_{\mathrm{len}}{p}_{\mathrm{len}}(L)\}$$
其中 $q$ 是生成的查询，$d$ 是定理，$k$ 是当前检索器给目标定理的排名，$L$ 是查询长度。三项的作用分别是：

• 一致性 $j(q,d)$：由 GPT-OSS-120B 判断查询和定理说的是不是同一件事，不一致记 0，整条奖励归零。
• 难度 $f_{\mathrm{rank}}(k)$：目标定理排进前 5 名，说明查询太容易，记 0；排在 5 到 30 名之间，奖励随排名按对数增长；排在 30 到 100 名之间记满分 1；掉出前 100 名记 0，因为这多半是查询写错了，而不是检索器的弱点。
• 长度惩罚：查询超过 40 个 token 开始扣分，到 50 个 token 扣满，扣分系数 ${\lambda }_{\mathrm{len}}=0.15$。阈值依据是真实查询的长度分布：人写和智能体查询的 90 分位数是 37 和 28 个 token。

训练时还混入一部分监督微调，目标是反映人和智能体搜索习惯的真实风格查询，混合比例随训练逐步降低：训练初期先用监督信号把生成器的写法固定在真实查询附近，后期再主要按强化学习奖励更新。每轮生成器训练完，作者用它为 Mathlib 定理生成 30 多万条查询，和原有长复述数据一起重新训练检索器；新检索器再提供下一轮的排名奖励。一共交替两轮。

2.3 检索前改写查询

输入一侧用 GEPA 优化改写提示词。GEPA 是一种自动改提示词的方法：用候选提示词改写一小批查询，看固定的 Lean Finder V2 检索器把目标定理排到第几，根据排名和文字反馈修改提示词，只保留有改进的版本。改写和提示词优化都用 DeepSeek-V4.1-Flash 完成，优化用的查询来自 2.2 节生成的合成数据，不用测试集。

3. 实验

3.1 主结果：短查询上大幅领先，长查询上不退步

这组实验检验 Lean Finder V2 在短查询上是否超过已有系统，同时在长查询上不变差。短查询测试集是 MathlibQR，810 条人写短查询；长查询测试集是 2,526 条完整描述。作者保证测试集里的目标定理和相关查询没有在任何阶段进入训练。对比系统包括：LeanExplore（1.09 亿参数的检索器）；LeanSearch V2，同样基于 Qwen3-Embedding-8B，可外加一个 8B 重排模型；TheoremGraph；前作 Lean Finder（7B）；以及让 Claude Code（Sonnet 5）自己搜索文档。下表摘自论文 Table 1（MathlibQR）：

Lean Finder V2 只用一个检索器，所有指标都高于带 8B 重排的 LeanSearch V2。两者的检索器起点相同，都是 Qwen3-Embedding-8B，所以差距主要来自训练数据。从第 0 轮到最终版本，nDCG@1 从 0.463 升到 0.558，这段提升完全来自对抗生成的短查询，因为第 0 轮只用了已有的长复述数据。Claude Code 的 nDCG@1 也有 0.527，作者认为原因是 Sonnet 5 熟悉 Mathlib 的命名习惯，还能反复搜索文档。

在长查询测试集上，Lean Finder V2 的 nDCG@10 是 0.749、Recall@10 是 0.919，前作 Lean Finder 是 0.742 和 0.914（论文 Table 2），加入大量短查询训练没有损害长查询检索。

3.2 真实无标注查询

这组实验检验在没有标准答案的真实查询上，Lean Finder V2 是否仍然更好。作者取 200 条真实的人写和智能体查询，把五个系统的检索结果打乱顺序、隐去系统名，让 GPT-5.6 Sol 和 Claude Opus 5 分别按有用程度给五个系统排名。两个裁判都把 Lean Finder V2 排第一：平均名次 1.980 和 1.945，分别在 35% 和 38% 的查询上排第 1；LeanSearch V2 对应是 26% 和 32%。两个裁判的判断有 89% 一致。

3.3 查询改写

这组实验检验检索前改写能否再提升。检索器固定为 Lean Finder V2，每种改写方法各生成三次。GEPA 优化后的提示词把 nDCG@1 从不改写的 0.558 提到 0.588（三次标准差 0.004）；同一提示词优化前的初始版本只有 0.532，比不改写还差；LeanSearch 和 LeanDex 两种已有改写方法分别是 0.475 和 0.520。Recall@100 本来已经是 0.973，所以改写的作用主要是把正确定理从候选里挪到最前面几名。再加上作者自训的 8B 重排模型，nDCG@1 到 0.610。

3.4 下游证明

这组实验检验检索变好能否帮到实际写证明。FATE-H 是 100 道较难的形式化代数题，让 Claude Code 在相同提示和预算下分别配不同的搜索工具，跑三次取平均通过率（只算能编译、没有 sorry 占位的证明）：不配搜索工具 34.0%，配 LeanExplore 27.3%，配 Lean Finder 30.7%，配 LeanSearch V2 36.0%，配 Lean Finder V2 39.3%。配较弱的搜索工具反而比不配更差，说明检索结果不准时会把智能体引向错误的定理。

3.5 消融：难度和一致性缺一不可

这组实验检验奖励的两部分是否都必要。做法是第一轮生成器只换奖励，其余设置不变（论文 Table 7，MathlibQR）：

• 只奖励难度：nDCG@1 0.453，低于第 0 轮的 0.463。
• 只奖励一致性：nDCG@1 0.463，和第 0 轮持平，Recall@10 从 0.760 升到 0.780。
• 两者都要：nDCG@1 0.520，Recall@10 0.842。

只奖励难度时，生成器可以靠写偏题的查询让排名变差，这类查询训练出来的检索器反而学到错误的对应。只奖励一致性时，查询对检索器来说太容易，提供的新信息有限。

第二轮的消融回答“是不是多采样就够了”：每条定理同样共采样两条查询、优化步数相同，第二轮改用冻结的基础模型生成查询，nDCG@1 是 0.469；用真实查询做监督微调的生成器是 0.473；继续用第一轮训练好、不再更新的强化学习生成器是 0.515；针对新检索器再训练一轮生成器是 0.558（论文 Table 9）。生成器要跟着检索器的弱点一起更新，第二轮才有明显收益。

4. 局限

论文没有单独的局限章节。可以补充两点。第一，MathlibQR 只有 810 条查询，真实查询评测依赖大模型裁判，两个裁判一致率 89%，但没有人工复核的排名结果。第二，奖励里的一致性判断由 GPT-OSS-120B 完成，判断标准直接决定什么样的“难”被保留，论文没有报告这个判断的错误率，判断偏宽松时偏题查询仍会混进训练数据。

5. 实践意义

一是给专业领域训练检索器时，先统计真实查询的长度和写法，再按这个分布构造训练数据。本文的数据显示，同一个 8B 检索器只是把训练数据从长复述换成贴近真实长度的短查询，就超过了带重排的系统。

二是用强化学习合成难样本时，难度奖励必须配一致性检查，并设置排名上限，掉出前 100 名不给奖励。本文的消融直接说明，只追求难度会让合成数据变成噪声。