经认证的机制性编辑：技能移除与保留的行为保证

机制性编辑（消融、权重编辑、激活引导）是从神经网络中遗忘有害能力、同时保留有用能力的标准工具。当前方法仅通过测试来验证其效果，而测试永远无法覆盖整个连续输入区域。可解释性与验证交叉领域的既有工作，会对模型的描述进行认证：例如某个电路计算什么，或该描述是否忠实地解释了整个模型。相比之下，我们认证的是编辑的行为效果：对于区域内的每个输入，禁用某个电路都会移除一项技能，并可证明地保留另一项技能；这是一种信息流安全意义上的特征无干扰保证。我们展示了从玩具 ReLU 网络到标准 softmax + LayerNorm transformer 的此类经认证编辑，在连续嵌入空间区域上证明技能的移除与保留；通过改用可靠的界传播方法，所处理的输入扰动维度约达到精确求解器能力的 9 倍。此外，我们证明不存在任何有限的确定性黑盒测试能够认证技能移除，并构造出一种编辑：它通过了穷举测试，却在一个可任意缩小的残留区域上被证明会失败。这些保证适用于规模较小的标准架构网络；同时，与任何移除声明一样，它们预设目标技能具有可判定的规范，而现实世界的危害可能并不具备这一性质。