研究者提出可认证机制编辑:在连续输入区域上证明技能移除与保留
研究者提出可认证机制编辑,用形式化方法证明一次编辑能在指定连续输入区域移除目标技能并保留另一技能。作者在小型分段线性网络上用精确SMT求解,在含softmax和LayerNorm的小型Transformer上用CROWN边界传播,并以攻击给出可比较的上界。论文构造出通过密集测试却仍在极小区域保留技能的编辑,说明有限确定性黑盒测试不能提供这种区域保证。结论是概念验证,依赖技能具有可判定的形式化规格;尚未证明能直接移除大型模型中复杂的现实危害。
推荐理由论文把机制编辑的效果从测试验证推进到连续输入区域上的形式化证明,并给出有限黑盒测试无法证明技能移除的构造性结论。