提出认证机制编辑以证明技能移除与保留

该论文提出一种机制编辑（mechanistic edits）的形式化验证方法，旨在为神经网络的能力移除提供行为保证，而非仅依赖无法覆盖连续输入区域的测试。作者证明了在特定嵌入空间区域内，禁用某个电路可确切移除目标技能并保留另一项技能，实现了信息流安全意义上的特征非干扰保证。 研究从简单的 ReLU 网络扩展到标准的 softmax + LayerNorm Transformer 架构，通过切换到声 bound 传播（sound bound propagation），将精确求解器能处理的输入扰动维度扩大了约 9 倍。同时，论文证明了不存在任何有限的确定性黑盒测试能够完全认证移除效果，并构造了一个反例：某次编辑通过了穷尽测试，但在一个任意小的幸存者口袋中仍会失败。 这些保证适用于小型标准架构网络，但前提是目标技能必须具备可判定规范，而现实世界的有害内容可能不具备此属性。事实部分包括实验规模、维度提升倍数及理论证明结论；推断部分在于该方法对现有对齐验证范式的挑战；猜测部分涉及该方法在复杂现实场景中的适用性边界。