论文指可解释替换网络忠实性易被微小扰动翻转，提出形式化验证框架

论文指出，机制可解释性中可解释替换网络（IRN）的忠实性通常只在干净数据上做经验评估，而语义上极小的输入扰动就会翻转主导 IRN 特征，从而改变人类可理解的解释，这一现象在 GPT-2 small、Gemma 2 2B、Gemma 3 1B、Llama 3.2 1B、R1-Distill-Qwen 1.5B 五个开放权重模型族上均出现。作者提出首个针对 IRN 忠实性的形式化验证框架，用可达性分析在对抗场景下给出忠实性差距的可靠上界。作者还表明，验证感知训练能显著收紧该认证上界，恢复安全审计人员可据以行动的特征级解释。论文关键词包括形式化方法、验证、认证、鲁棒性、稀疏自编码器与 transcoder。