研究者提出「认证式机制编辑」，用可靠界传播在连续嵌入区域上证明技能移除与保留，并证明有限黑盒测试无法认证移除
相关研究与后续进展
核心概要
该工作把机制编辑（消融、权重编辑、激活引导）的效果从「测试验证」提升为「行为认证」：对连续嵌入空间区域内的每一个输入，证明禁用某电路可移除一项技能并保留另一项技能，在从玩具 ReLU 网络到标准 softmax + LayerNorm transformer 上给出移除与保留的证明，并借助可靠界传播把可处理的输入扰动维度提升到精确求解器约 9 倍；同时证明不存在任何有限确定性黑盒测试能认证移除，并构造出一个能通过穷举测试却在可任意缩小的「幸存者口袋」上必然失败的编辑。
Fig. 1. An edit that every test approves and the solver refutes. (a) Skill A’s removal region for a constructed two-input model after an ablation edit. A 15 × 15 grid (shown), a 201 × 201 grid of 40,401 points and 300 random inputs all report the skill removed while the solver nonetheless returns a surviving input (star). (b) The edited skill-A output along x0 through the survivor: a tent of three ReLUs rises above zero in a band 0.0006 wide, between neighboring grid points 0.002 apart (Proposition 3). (c) An automated search over trained models, 80 per input dimension, finds no illusion with two or three inputs and three with four or five; their survivor regions lie below 1.5 × 10−6 of the domain (95% Clopper–Pearson bound).
arXiv · 第 3 页深度剖析
提出对编辑的行为效果进行认证，而非仅认证模型描述：证明禁用某电路后，在连续嵌入空间区域内对每个输入都移除一项技能并保留另一项技能，即信息流安全意义上的特征非干扰保证。 此前位于可解释性与验证交界处的工作认证的是「模型描述」——电路计算了什么、或是否忠实解释整个模型；该工作改为认证「编辑的行为效果」，把保证对象从描述转向编辑本身。 在从玩具 ReLU 网络到标准 softmax + LayerNorm transformer 的网络上给出移除与保留的证明，覆盖连续嵌入空间区域。
通过改用可靠界传播（sound bound propagation），在保持证明可靠性的同时，把可处理的输入扰动维度提升到精确求解器约 9 倍。 相对精确求解器，可扩展性显著提高，使认证能覆盖更高维的输入扰动区域。 文中报告约 9 倍于精确求解器可处理输入扰动维度的结果。
证明不存在任何有限确定性黑盒测试能够认证移除，并给出一个通过穷举测试却可证明在「幸存者口袋」上失败的编辑，该口袋可被做得任意小。 把「测试无法覆盖整个连续输入区域」这一直觉上升为不可能性结论，说明仅靠测试验证移除在原理上不可行。 以构造性反例加证明的形式给出：一个通过穷举测试的编辑，在可任意缩小的幸存者口袋上必然失败。
启示与展望
该结果面向需要在连续输入区域上获得移除与保留保证的场景，适用于消融、权重编辑、激活引导等机制编辑工具的使用者，尤其是关心「禁用某电路是否真的移除一项技能、同时不破坏另一项技能」的研究者与工程实践者。保证在小型、标准架构网络上成立，从玩具 ReLU 网络一直到标准 softmax + LayerNorm transformer；可靠界传播的引入使可处理的输入扰动维度约为精确求解器的 9 倍，从而把认证扩展到更高维的连续嵌入空间区域。
保证成立的前提是目标技能具有可判定规格，而文中指出真实世界的危害未必具备这一性质，因此认证能覆盖的移除目标范围仍待明确。保证目前限于小型、标准架构网络，向更大或非标准架构的推广仍是开放问题。此外，移除不可被有限确定性黑盒测试认证的结论针对的是确定性黑盒测试这一设定，其他验证范式下的情形值得进一步观察。