SkillEffect: 内存受限代理工具的检查下降

# SkillEffect：面向内存受限智能体工具的受检降级运行时  
来源：https://arxiv.org/html/2608.17007  

###### 摘要  
智能体技能可指定工具使用的流程规范和资源要求，语言模型将其实例化为具体程序。然而，当模型将这些指导转化为现有工具接口的代码时，即使语义正确的程序也可能加载整个输入并超出单次工具调用的可用内存。我们提出SkillEffect，一种具有可恢复源关系、受审计的有界实现和注册输出后置条件的受检降级运行时。在授予执行权限前，独立检查器会根据提交的程序和不可变输入重建每个提议的降级方案。每个关系插件提供源识别器、输入事实提取器、有界中间表示构造器、区域约束函数和后置条件；通用运行时则提供受检选择、有界虚拟机执行、原子容量租赁和分阶段发布。SkillEffect的通用性体现在架构层面而非自动实现：每个支持的计算都需要经过审计的关系插件，而调度、资源控制、执行和发布机制则由所有插件共享。在六类算子中，有界访问显著降低了峰值内存，并在外部固定上限下提高了任务完成率。六个插件在五种执行模式（从流式归约到有界堆Top-kk）下实例化了相同的契约。XLSX引导研究和Top-kk扩展表明，新的关系和新的保留状态模式复用了相同的信任边界，且检查器接受了所有评估的合法配置并拒绝了所有对抗性提案。这些结果共同表明，一种受检降级架构可在智能体工具调度中强制执行异构的注册内存关系。  

## 1 引言  
可复用智能体技能日益向语言模型提供过程知识：应调用哪些工具、哪些字段重要、如何处理大型输入以及如何验证结果[5,21,28]。相同的过程可编译为截然不同的物理执行。调用`read_csv`的计划会物化整个表；惰性扫描可在有界空间内对表进行投影、过滤和聚合。加载整个科学矩阵与仅打开其元数据（即使两者回答相同查询）也存在差异。在服务器级预算下，这种差异是性能问题；在100 MiB工具阶段限制下，则可能决定工具调用能否完成。仅凭技能推荐是不够的：在我们的外部smolagents测试中，当未提供资源反馈时，所有16个原本有效的工具调用均选择立即访问模式。这种选择直接产生服务影响。智能体平台在隔离沙箱中执行多次工具调用，每次调用的内存预留既决定故障隔离，也影响主机可承载的会话数量。严格的分配已是常规基础设施设置，而非论文特定的思想实验：Modal Functions和沙箱默认请求128 MiB并可设置显式硬限制；E2B提供从512 MiB起的沙箱内存配置，付费计划允许CPU/RAM自定义；Cloudflare Workers将每个隔离器限制为128 MB；AWS Lambda的默认和最小设置均为128 MB[19,10,6,1]。Daytona的集群模型为每个用户、任务或智能体分配一个沙箱；资源按沙箱预留，运行集群从组织级计算池中分配[8]。这些服务共同确立了128–512 MB级分配和限制作为常规沙箱/无服务器容量区间。为立即最坏情况预留会浪费该容量；接受乐观计划则可能在模型已消耗令牌和延迟后终止轨迹。因此，有效的控制点在于待处理调度：在模型具体化其计划之后，但在工具进程消耗租户配额之前。  

图1：SkillEffect信任边界示意，以两百万行Polars S2关系为例。338.6/69.5 MiB峰值为配对宽松容量算子测量值；96 MiB为相同输入的开发限制，而非外部扫荡层级。构建者的降级方案不受信任。独立检查器识别唯一匹配关系，重建源语义和输入事实，验证目标配置和活跃集；有界虚拟机仅在容量租赁下执行接受的中间表示，并在其注册后置条件通过后才发布分阶段输出。  

现有层次结构留下具体的系统缺口。技能压缩可保留过程契约或衡量控制义务在压缩后是否存续，但通常不会为模型选择的程序分配物理活跃集效应[28,14]。成本感知规划器使用配置文件以偏好更廉价的工具[30]，但配置文件不会构建保持关系的有界程序。计划门控或cgroup可拒绝或停止不安全进程[33,34]，但无法恢复预期结果。反之，用数据库或流式算子替代pandas并不因使用更少内存而正确：过滤、输出键、归约语义和边界情况仍需匹配声明的任务[2,22,16]。技能本质上是异构的：短API包装器、表分析过程和科学文件工作流无需共享相同的资源瓶颈。我们针对的重要类别是：技能声明资源敏感的访问义务、生成的计划暴露可恢复的声明式计算、存在有界实现，且声明结果允许注册后置条件。CSV聚合、序列归约、科学元数据、分块数组、工作簿流式处理和风险排序审计日志选择实例化了该类别的不同成员。在这些成员中，可复用单元是受检关系 \(r=\langle S_r, I_r, L_r, A_r, G_r\rangle\)。其中 \(S_r\) 识别源计算，\(I_r\) 检查不可变输入事实，\(L_r\) 构造规范有界中间表示，\(A_r\) 推导其区域，\(G_r\) 在发布前验证结果。技能路由建立任务和工具上下文，随后独立检查器在调度前重建并验证具体关系实例。因此，新的计算通过实现这五个特定关系义务来扩展SkillEffect，同时复用通用调度信任边界。  

本文探讨以下问题：智能体运行时能否在调度前将超预算的模型生成工具计划转换为受检有界实现，而不改变声明的任务结果？评估具有两个互补角色。算子特征描述衡量六类工具族的物理机会：具体访问选择可在不改变声明答案的情况下改变活跃集。SkillEffect实验随后在六个插件中实例化一种关系契约，并练习完整的提案-检查-执行边界，从独立重建到有界虚拟机执行、容量租赁和分阶段发布。扩展研究使用XLSX衡量引导成本，并用Top-kk选择测试同一契约下新的有界状态模式。贡献包括：  
- • 对六个工具族具体智能体系统故障模式的物理特征描述：立即和有界访问路径可在产生不同活跃集和硬限制完成结果时保持相同声明结果，包括正确但立即执行时失败的模型生成计划；  
- • 围绕通用五义务关系契约构建的提案-检查-执行信任边界，其中语义和资源算术与关系特定，而绑定、唯一选择、准入、有界执行、租赁和发布是共享的；  
- • 对六种有界执行模式下六个插件的评估，包括（i）保留XLSX引导以衡量现有模式的扩展成本，以及（ii）Top-kk选择以在不改变通用核心的情况下测试质上新的保留状态模式。  

图1实例化了为路由技能生成的具体Polars程序的提案-检查-执行边界；第3节在注册表中泛化了相同的关系接口。  

## 2 系统模型与保证  
### 2.1 资源与准入模型  
SkillEffect为内存隔离工具服务实现受保护优化边界。接受的调度携带任务保持实现和容量承诺。当原始计划或受审计降级方案均无法建立这些条件时，控制在工具分配前返回，以便调度器选择其他工具、预算或执行站点。所选技能描述预期工具过程及其资源需求。在调度时，SkillEffect将提交的程序与其注册表中受审计的关系进行匹配。匹配关系将识别的源计算和不可变输入事实绑定到有界目标、内存限制和发布检查。LLM及其GPU内存位于此工具阶段容量域之外。令 \(p\) 为已生成但未提交的工具程序，\(x\) 为其不可变输入，\(\pi\) 为平台清单。我们将捕获计划的峰值物理内存建模为  
\[
W_e(x) = \begin{cases} 
n_e(x), & \text{立即} \\
\min\!\left(n_e(x), \ell_e\right), & \text{有界}
\end{cases} \tag{1}
\]  
\[
U_\pi(p,x) = F_\pi + M_\pi + \max_t \sum_{e \in \mathcal{A}_p(t)} \bigl[\alpha_{\pi,e} W_e(x) + R_e(x)\bigr].
\]  
其中 \(\mathcal{A}_p(t)\) 是在时间 \(t\) 同时活跃的效应集，\(n_e(x)\) 是效应 \(e\) 的输入大小状态，\(\ell_e\) 是其有界窗口。因此 \(W_e(x)\) 对立即效应保留完整状态，对有界效应最多保留 \(\ell_e\)。\(F_\pi\) 是固定运行时状态，\(M_\pi\) 是冻结平台预留，\(\alpha_{\pi,e}\) 将逻辑活跃状态映射到物理占用，\(R_e\) 覆盖暂存和输出状态。对 \(t\) 取最大值组合重叠效应，同时允许顺序阶段复用容量。算子特征描述从校准的全新cgroup信封实例化这些术语。在六个注册插件中，检查器直接推导可变区域和分阶段输出项，并从平台清单添加哈希绑定运行时和I/O预留。保证边界将源派生可变区域与解释器、分配器和内核状态的经验常数组合。  

#### 受检关系与规则选择  
令 \(\mathcal{R}\) 为六关系注册表，\(B\) 为工具阶段容量预算，\(G_r\) 为与关系 \(r\) 注册的在线后置条件，\(V_q\) 为评估中用于任务 \(q\) 的精确验证器。对于每个适用的 \(r \in \mathcal{R}\)，不受信任的构建器可提议包含有界配置和目标中间表示的受检记录 \(z_r\)。独立检查器通过重建完整的允许源抽象语法树、其源派生语义参数、不可变输入事实，以及规则的算术和方言义务来评估 \(C_r(z_r; p,x,\pi)\)。它还验证提议的有界窗口和分阶段输出容量，并为该配置重建规范目标中间表示和活跃集约束。此闭合源到目标关系建立源到目标可接受性；\(G_r\) 检查在线结果，而 \(V_q\) 在评估中评分精确任务结果。在线后置条件是注册关系的一部分。规则选择和语义参数从提交的源和输入重构；窗口和分阶段输出容量保持为受检提议参数。均不依赖评估预言机的预期值。定义接受集  
\[
\mathcal{C}_{B,\pi}(p,x) = \left\{ (r, z_r) \ \middle| \ \begin{array}{l} r \in \mathcal{R},\ C_r(z_r; p,x,\pi) = \mathrm{pass}, \\ z_r.U \leq B \end{array} \right\}. \tag{2}
\]  
注册表实现  
\[
(r^\star, z^\star) = \begin{cases} 
c, & \mathcal{C}_{B,\pi}(p,x) = \{c\}, \\
\bot, & \text{其他}.
\end{cases} \tag{3}
\]  
选择成功时，\(z^\star.T\) 是提供给虚拟机的有界中间表示。零接受规则导致弃权，而多接受规则导致歧义拒绝。认证器既不接收任务也不接收族标签。算子特征描述前端有单独的识别身份案例和有序类型或受保护降级；它提供广度证据，而非方程2和3的独立受检关系。  

#### 准入策略  
在硬限制下，准入和弃权具有不对称后果。调度未论证的计划可能终止工具执行并丢弃轨迹，而弃权发生在有界虚拟机执行或发布之前，并将控制返回给调用者。未知效应和歧义规则匹配在容量消耗前返回控制。准入证明当前注册表和限制下的可行性，而弃权保留替代工具、预算或执行站点的可用性。  

#### 容量与发布  
对于准入请求 \(i\)，令 \(r_i\) 和 \(z_i^\star\) 为其选择的关系和记录，\(y_i\) 为其分阶段结果，\(U_i = z_i^\star.U\) 为其受检峰值。令 \(H\) 为配置的cgroup `memory.max`，\(P_i\) 为独占请求cgroup的测量峰值，\(A_t\) 为发布时 \(t\) 的活跃租赁。令 \(\mathbf{E}_{\mathrm{limit},i}\) 为适用cgroup的`max/oom/oom_kill/oom_group_kill`事件向量，\(\sigma_i\) 为其观测到的交换字节（对于请求的独占cgroup或公共共享cgroup）。记 \(\mathsf{publish}_i\) 为 \(y_i\) 变为外部可见的事件。在获取租赁前，运行时要求 \(U_i \leq H \leq B\)。  
\[
U_i \leq H \leq B. \tag{4}
\]  
SQLite账本仅在`reserved`、`running`和`verified`状态字节总和不超过 \(B\) 时原子准入租赁。在共享容量实验中，账本容量和cgroup限制配置为相同值 \(B=H\)。输出发布满足 \(\mathsf{publish}_i \Longrightarrow G_{r_i}(y_i) = \mathrm{pass}\)。