考虑一个 ReAct 风格的智能体，配有一个每轮容量为 $16{,}384$ 位的未登录草稿板（scratchpad）。输出轨迹上的回归测试显示无行为变化，然而在受控重放下禁用草稿板后的同一条轨迹，揭示了规划任务上工具令牌概率分布中 $0.0163$ 位的偏移。这一差异不是探针伪影。它是审计的一个结构特征：记录轨迹未能区分两个性质上不同的系统——一个其隐藏容量在测试分布上处于休眠状态，另一个其隐藏容量处于活跃状态。识别哪一个成立，正是审计的任务。
这是两个不同的量：多少内部状态逃逸了轨迹，以及其中多少驱动了下一步行动。仅依赖输出的黑盒审计视图会将它们合并为一个既不可计算也不具诊断性的单一「隐藏性」判断。一个拥有大日志缺口但无行为性隐藏驱动的系统，与一个拥有小缺口但强驱动的系统是无法区分的，尽管二者的审计含义截然不同。
本文提出一个双重证书协议，分别回答每个问题。静态证书 $\varepsilon_{\text{state}}^{\text{UB}}$ 仅依据部署拓扑，通过未追踪信道上的割集界对残差熵 $H(S_t \mid \tilde T_t)$ 给出上界。动态证书 $\delta_{\text{act}}^{\text{LB}}$ 通过三种探针类别之一（重放、干预或代理，取决于审计者的访问权限）对残差决策相关性 $I(S_t; A_t \mid \tilde T_t)$ 给出下界。这两个证书是独立的轴：一个 $\varepsilon_{\text{state}}^{\text{UB}}$ 大而 $\delta_{\text{act}}^{\text{LB}}$ 小的系统具有不可恢复但处于休眠状态的状态；两个都大的系统则具有不可恢复且活跃的状态。两者都是可审计的。两者都不是单个标量所能揭示的。
动态轴亦可被索引化。审计者不仅可追问残差状态是否重要，还可追问它在何处重要：哪个模块、哪个去噪步骤或哪个通信边承载了决策相关性。这将证书从标量诊断转化为部署隐藏状态几何上的激活剖面。
以 $\tilde T_t$ 为条件本身就是保护措施的一部分，而非干扰项。如果一个模型将隐写或压缩式推理写入记录轨迹，则该信息位于 $\tilde T_t$ 中，并被 $I(S_t; A_t \mid \tilde T_t)$ 条件化移除。动态证书衡量的是超越已记录轨迹的残差决策相关性；它不计数已经对审计记录可见的隐藏性。
贡献。 本文为智能体审计定义了一个双重证书框架 $(\varepsilon_{\text{state}}^{\text{UB}}, \delta_{\text{act}}^{\text{LB}})$。命题~\ref{prop:static-ub} 通过未追踪信道上的最小割给出了残差隐状态熵的拓扑上界。命题~\ref{prop:dynamic-lb} 并非一个新的信息论不等式；它是一个审计归约，将条件 DPI 转化为残差决策相关性的三个可容许下界探针——重放、干预和代理。
我们在三种残差状态几何上评估该协议：一个 ReAct 草稿板模块、一条扩散语言模型去噪轨迹，以及一条多智能体私人报告边。同一计算公式在不同设置中被复用，但索引从模块变为时间步再变为通信边。附录中的校准覆盖了只读代理估计和一个人工合成真实场景，其中静态边界与真实隐藏状态熵相匹配。一个 Lean 4 工件从 Mathlib 第一原理对推论~\ref{cor:auto-exact} 进行了机械化验证，并从有限离散定义证明了迹缺口链式法则和条件 DPI，仅割集容量上界保留为命题~\ref{prop:static-ub} 的外生结构前提（精确边界见 §\ref{sec:external-axioms}）。
Comments