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

机制可解释性读到的往往是IRN，而IRN在对抗输入上是否仍忠实于模型，缺少可证明的保证。

• 场景：作者称前沿语言模型内部是黑盒，dense计算产生多义神经元（polysemantic neurons）。通行做法是在各层训练可解释替换网络（interpretable replacement network, IRN），用稀疏激活特征代替原计算，再由自动化解释给特征贴可读标签。安全审计若按这些标签做拒绝或放行，解释就只和这个替身一样可信。
• 现有不足：作者称IRN通常只在干净数据上用重构损失评估；单点修补（patch）会偏离“复现真实机制”的目标。对抗样本已知存在约十年，语言上的语义保持扰动也已知，但“解释能否在对抗输入下存活”几乎未被测试或验证。电路追踪若做在替换后的模型上，IRN的忠实性就更关键；直接在原模型上追踪电路，作者称尚不能扩展到前沿模型（Gao et al., 2025b）。
• 核心观察：Fig. 1用Gemma 2 2B、Gemma Scope SAE第16层的例子说明，干净句上主导特征读成病原体培养，轻微同义替换后主导特征改读成职场文化，模型本身未改，变的是IRN暴露的解释。附录A给出该例的特征表（top-8 Jaccard为0.23）。作者同时强调：底层模型在对抗输入上也可以改变行为，只有稳健模型才被期望保持主导特征。
• 提出的方法：作者提出用可达性分析给IRN的忠实差距（faithfulness gap）做可靠上界，并称这是据其所知对大语言模型机制可解释性的形式化保证框架；再用verification-aware训练收紧该认证界，使特征级解释更可供安全审计使用。贡献分为三步：跨模型族展示敏感性（Sec. 3）、建立验证框架（Sec. 4）、用训练收紧差距（Sec. 5），并在Sec. 6给出整模型的组合验证设想。

作者在引言与Sec. 7把相关工作分成电路、稀疏替换网络、忠实性批评和形式化解释四支，并称此前IRN只做经验评估、没有对抗设定下的最坏情况保证。

电路级可解释性

• Olah et al. (2020)、Wang et al. (2023)：从视觉电路发现延伸到语言模型，把对某任务活跃的一部分注意力头组成电路，例如间接宾语识别；Feucht et al. (2026)报告Llama中的十进制加法电路，Geiger et al. (2025)讨论对同一任务共同激活的神经元簇与因果抽象。
• Conmy et al. (2023)：目标是自动发现这些电路。作者指出，被找出的单元仍然多义，因而难以解释（Elhage et al., 2022）。
• 直接在原模型上的电路追踪：作者在引言中称Somvanshi et al. (2026)一类方法尚不能扩展到前沿模型（Gao et al., 2025b），因此实践中常先换成IRN再追踪（Ameisen et al., 2025）。

稀疏可解释替换网络

• SAE：Huben et al. (2024)用稀疏自编码器把残差流拆成稀疏特征并重构残差流；单层宽隐层被当作通用逼近器（Hornik et al., 1989）。变体包括gated SAE（Rajamanoharan et al., 2024a）、专用激活（Gao et al., 2025a），以及面向功能重要性而非重构的端到端字典学习（Braun et al., 2024）。
• Transcoder：Dunefsky et al. (2024)用transcoder重构MLP输出；Ameisen et al. (2025)将其扩到跨层计算块。MLP被当作自然替换对象，因为Geva et al. (2021)、Meng et al. (2022)称每个MLP模块在残差流上做特定概念更新，但计算不透明；注意力则通常可直接读出token关系（Vaswani et al., 2017）。
• 稀疏特征上的电路：Marks et al. (2025)在SAE上、Ameisen et al. (2025)在TC上发现并编辑可解释因果图。作者称这些工作的IRN都只做经验评估。

特征标注与忠实性批评

• 自动解释：Bills et al. (2023)、Paulo et al. (2025)用另一个LLM为特征生成并打分自然语言描述；Lin (2023)的Neuronpedia公开这类标注。Gurnee et al. (2023)用带标签特征在原模型中定位计算。
• 对忠实性的批评：Heap et al. (2026)称随机初始化模型上训练的SAE，自动解释分数与训练好的模型相近；Paulo & Belrose (2026)称同一模型、同一数据上学到的特征并不相同。Li et al. (2026)用对抗攻击展示IRN脆弱，本文Sec. 3称是在此基础上增加模型族与IRN类型。Kumar et al. (2024)讨论针对对抗提示的认证防御，作者称其扩展性差。

可解释性中的形式保证

• 事后解释器：LIME（Ribeiro et al., 2016）、SHAP（Lundberg & Lee, 2017）假设输入邻域内近似线性；Anchors（Ribeiro et al., 2018）等基于采样的解释缺少可证明保证（Wu et al., 2023; Bassan & Katz, 2023; La Malfa et al., 2021）。作者把Sec. 3的前提连接到这条关于常规网络解释稳健性的文献。
• 形式验证：Kaulen et al. (2025)总结神经网络验证进展；Bassan et al. (2025)、Marques-Silva & Ignatiev (2022)在多种威胁模型下做带保证的解释。Hadad et al. (2026)在视觉模型上做可证明的电路发现。作者称本文把这条线带到大语言模型。

基线与数据：实验基线是公开的标准训练IRN，记为STD；对比训练为PGD对抗增广（Madry et al., 2018）、可达集损失SET（Koller et al., 2025）以及LoRA（Hu et al., 2022）。改写用WordNet（Miller, 1995）；MAJOR改写用Gemma 2 2B-it。句子来自WikiText-2测试集（Merity et al., 2017），附录C.1写明取200句、目标token为句中一个实词。激活函数按模型族取ReLU（GPT-2）、JumpReLU（Gemma Scope）、TopK（Llama Scope）。

整体思路是：先用同义改写观察活跃特征集有多不稳定，再把“IRN是否在对抗邻域内复现原计算”写成可验证的δ-等价，最后用对可达集的惩罚来训练更易认证的IRN。作者把该框架称为对IRN忠实性的形式验证，工具是CORA的zonotope可达性分析。

问题设定与δ-等价

• IRN两种形式：SAE在层k重构残差流Hk（式2）；TC从注意力后的Hk′重构MLPk的输出（式3）。激活φ按家族为ReLU、JumpReLU或TopK。解释读自φ(·)(i)>0的特征下标，训练时的稀疏惩罚使dIRN≫dmodel时只有少数特征点燃；标签由激活该特征的输入自动摘要（Paulo et al., 2025）。
• 对抗集合：对一句输入构造X⊂Rdmodel×τ。逐token在嵌入空间对全部同义词取凸包，再做笛卡尔积，以避免枚举组合爆炸。传播到层k的集合记为Hk。正文实验里，因验证器还不能扩展到整模型，Hk是在该层对对抗激活取凸包，而不是把X一路传播过来。
• 忠实性定义：Def. 1称，若对所有H̃k∈Hk，残差与SAE之差或MLP与TC之差的ℓ∞范数≤δ，则该层IRN与模型δ-等价；δ足够小则称忠实。Fig. 3把差值网络画成两条并行路径：认证的差集落在小盒[−δ,δ]dmodel内即通过。SAE把MLP换成恒等映射。
• 界的方向：真值δ∗通常算不出，用攻击最大化差值得到下界δ，用验证得到上界δ̄，满足δ≤δ∗≤δ̄。Jaccard相反：攻击给出上界J̄（只能证明重叠可以降到这么低），需要验证的是不可翻转特征对应的下界J。图中用测试集上δ与δ̄的中位数之间的填充箱表示差距，须使中位δ∗落在箱内，晶须为两者的25%与75%分位。

验证器与结构优化

• 验证问题：附录B.1的Def. 2是：对网络Φ、连续输入集X和不安全集S，证明所有x̃∈X都有Φ(x̃)∉S。该问题NP-hard（Katz et al., 2017），所用验证器给出可靠但不完备的结果。CORA用zonotope（Girard, 2005）表示集合，仿射层直接映射，非线性层用线性近似加区间误差（式6，Singh et al., 2018; Koller et al., 2026），再检查输出集与S不相交。
• 不必显式构造宽隐层：附录B.2只认证差值集的ℓ∞界。TC分支只有一层高维非线性，夹在线性映射之间；当Hk是轴对齐盒时，预激活区间可用一步区间算术得到围包参数，再把Wkdec diag(mk) Wkenc收成单个矩阵Mk,TC（式10），从而不显式构造dIRN维zonotope。MLP因多层不能同样折叠，仍由集合验证器给Mk,MLP与Ik,MLP，最后差值围包为式(12)。SAE用恒等替换MLP。
• Jaccard作为副产品：附录B.3在同一围包上读预激活区间。若某特征的区间整个高于阈值则认证为激活，整个低于则认证为关闭；跨在阈值上的记为未知。只对认证激活的特征计算与干净输入top-20的Jaccard，得到J≤J∗。搜索最小可验证δ̄用对验证查询的二分（附录C.1，Alg. 2）。
• Fig. 8的几何：作者用二维切片示意，不忠实时MLP与TC的输出曲面分开甚至相交，只能认证大δ；曲面对齐后小δ即可。

训练以收紧忠实差距

• 四种设定：STD为给定的标准训练IRN。PGD用PGD找到的H̃k做增广（Madry et al., 2018）。SET用可达集损失（Koller et al., 2025），直接惩罚Fig. 3c里偏大的误差集，使IRN流形与模型流形对齐。LoRA是低秩更新（Hu et al., 2022），可与PGD或SET组合。正文微调的是OpenAI的GPT-2 SAE。
• 训练细节（附录C.1）：AdamW，学习率1×10−4，权重衰减1×10−3，批量8，每层5个epoch；PGD步数10，步长取扰动半径的1/4。SET的可达集损失权重λ=0.1，干净重构为L1，总损失为重构加λ倍集合损失。LoRA秩r=8，只更新IRN，缩放α/r=2。GPT-2的扰动半径ε=0.1，按各模型残差流激活的量级选取；更大模型用更大ε，附录写明以保持相对扰动幅度。TopK的K在前向中固定，验证时用附录C.2.5的围包。
• 作者给出的理由：标准训练只兼顾干净数据上的重构与稀疏，不处理对抗输入，因而会拉低上一节的验证结果。LoRA即使验证器要求全空间稳健，作者仍报告能改进忠实性，并认为该现象可能迁到非NLP模型，论文未报告跨领域实验。

整模型的组合验证（设想）

• 为何不能端到端：Def. 1需要Hk包住传播后的全部对抗输入。注意力（Bonaert et al., 2021）和MLP都可以围包，但作者称围包往往过保守，模型也可能大到无法一次查询验完。因此Sec. 6逐块验证：每块给出输入–输出集合关系，相邻块中前者输出集含于后者的轴对齐输入盒，且每块IRN的δ足够小，则整模型通过。首块输入初始化为X，其后各块用传播样本的凸包初始化。
• 含入失败时的四种处理：加计算时间以收紧输出集；放大下一块的输入集（可能影响下游）；开发者重训某些块以获得更紧的输出界；上游收紧后下游也可跟着收紧。作者称每一点都需要更细的算法，留作未来工作。当前Hk仍偏小，例如GPT-2 SAE第6层约小5倍（Tab. 5），组合验证尚未做成。

实验设置

• 模型与IRN：GPT-2（SAE与TC，ReLU）、Gemma 2 2B（SAE与TC，JumpReLU，Gemma Scope）、Gemma 3 1B（SAE与TC）、Llama 3.2 1B（SAE与TC，TopK，Llama Scope）、R1-Distill-Qwen 1.5B（正文Table 1写作Qwen 1.5B，仅SAE，EleutherAI TopK）。附录C.2.5写Llama 3.2 1B的dmodel=2048、dIRN=131072、K=32；C.2.7写Qwen为dmodel=1536、κ=28层、dIRN=65536、K=32。GPT-2的dmodel=768。Table 1没有Qwen的TC行。
• 数据与扰动：WikiText-2测试集200句，目标token为句中一个实词（附录C.1）。MINOR：目标前换一个实词为WordNet同义词。MEDIUM：目标前全部实词换同义词。MAJOR：Gemma 2 2B-it在保留目标的前提下改写全句。Fig. 1/附录A的定向攻击另用PGD 300步、8次随机重启，压低四个生物相关特征的预激活。
• 指标：top-20 Jaccard，J=|A∩B|/|A∪B|。Table 1的J min、J mean是攻击导出的上界J̄，按层取最小或平均；作者写MINOR下最差层重叠相对下降约73%，MAJOR下约95%，这两个百分数是作者对Table 1的概括，不是表内原列。忠实差距为ℓ∞意义下的δ，报告攻击下界与验证上界。另报平均活跃特征数，以及MINOR改写导致下一token预测翻转的比例。
• 验证与训练设置：CORA，二分搜索最小可验证δ̄。图中箱为中位δ到中位δ̄，晶须为q25与q75。训练超参见第3问；Fig. 13各层使用同一套超参。硬件、软件版本写在附录C.1，正文未逐项列出数值。论文未报告与人工标注的一致性。
• 评审方式：特征标签来自Neuronpedia自动解释（附录A的表为gemmascope-res-16k）。主指标是集合重叠与ℓ∞界，不用LLM给攻击是否成功打分。

主结果

Table 1给出全层top-20 Jaccard的攻击上界。J min越低，说明存在一层在该改写级别下主导特征重叠更小。

表格较宽，可左右滑动

模型	IRN	MINOR J min / mean	MEDIUM J min / mean	MAJOR J min / mean
GPT-2	SAE	0.27 / 0.37	0.06 / 0.18	0.05 / 0.13
GPT-2	TC	0.70 / 0.79	0.45 / 0.62	0.38 / 0.54
Gemma 2 2B	SAE	0.62 / 0.78	0.35 / 0.59	0.33 / 0.54
Gemma 2 2B	TC	0.46 / 0.57	0.20 / 0.33	0.20 / 0.31
Gemma 3 1B	SAE	0.55 / 0.69	0.30 / 0.49	0.30 / 0.44
Gemma 3 1B	TC	0.47 / 0.67	0.18 / 0.42	0.20 / 0.38
Llama 3.2 1B	SAE	0.54 / 0.66	0.26 / 0.45	0.33 / 0.42
Llama 3.2 1B	TC	0.56 / 0.64	0.25 / 0.40	0.21 / 0.35
Qwen 1.5B	SAE	0.37 / 0.49	0.18 / 0.29	0.12 / 0.20

• 作者称两种IRN都出现下降，且Table 1的数字只是上界：攻击只见证一个坏输入，不能排除重叠更低的输入；稳健且忠实的IRN需要高的下界J。
• 作者同时写明，底层模型在对抗输入上也可以改变行为，因此不能把特征翻转都算成IRN失真。不忠实的极端例子是IRN靠大偏置永远点亮同一组“安全”特征，此时J恒为1，却不能反映模型是否安全，所以J单独不够用。
• 同表中GPT-2的TC在三级扰动上的J min都高于其SAE（0.70对0.27、0.45对0.06、0.38对0.05）；Gemma 2 2B则是SAE的J min高于TC。作者没有把“SAE一律更稳”写成结论。

逐层忠实差距

• 测了什么：Fig. 4在GPT-2全部层上同时画SAE与TC的δ下界和上界。附录Fig. 9、Fig. 11、Fig. 12对其余家族做同样的MINOR级逐层图，样本同为200句。纵轴是faithfulness gap δ，箱的含义与Sec. 4一致。
• 结果：作者称各层都验证到可观差距。举例：GPT-2第1层SAE对某个δ<1已δ-等价，即对抗输入下重构残差的ℓ∞差平均小于1；作者称在底层模型自身的残差流上也观察到过这种量级的差。后层上界和下界一起上升。作者称TC的差距通常大于SAE，因为TC要复现MLP，SAE只需重构输入。Fig. 12上，作者称R1-Distill-Qwen 1.5B的SAE比Llama 3.2 1B的SAE（Fig. 9）低一个数量级的忠实程度，且非逐元TopK的差距远高于GPT-2。图中逐层精确读数在转写文本里没有逐点列出，除第1层“δ<1”外不转写。
• 作者的解读：后层更不忠实，作者认为可能是因为模型在后层建立更复杂的联系，而现有IRN没有准确复现这些计算；并强调上升不是不完备验证器的假象，因为攻击找到的下界也在上升。

验证感知训练

• 测了什么：Fig. 5比较GPT-2第6层SAE在STD、PGD、PGD+LoRA、SET、SET+LoRA下的忠实差距，设置与Sec. 4相同。Fig. 6画同一层、同一批设定的top-20 Jaccard，箱从认证下界J到攻击上界J̄。Fig. 13把同一训练比较扩到GPT-2 SAE的第3、5、6、8、10、12层，纵轴以10^4为单位。
• 结果：作者称SET相对STD的认证上界约−90%。差集在dmodel=768中，作者称SET相对STD的相对误差体积约10−779。SET平均活跃特征13.9个，比STD少81%。LoRA在验证器要求全空间稳健时仍能改进忠实性。Fig. 6上，作者称干净输入的top-20里只有2–3个对对抗输入可证保留，但J在全部测试过的训练设定上都有改进。Fig. 13上，作者称只有集合式的verification-aware训练能把差距维持在小的水平，其他对抗训练做不到；文本没有给出各层的精确δ。
• 作者的解读：重训后的IRN更接近模型（Fig. 5），因此这时的Jaccard比基线IRN更有意义；作者认为特征仍保不住，应归因于底层模型本身不稳健。依据是：MINOR改写已经使GPT-2的下一token预测在21%的样本上翻转。

其他消融与分析

• 附录A、Table 2：Gemma 2 2B第16层SAE，定向PGD后top-8 Jaccard J=0.23；干净端8个特征里4个为生物学读法，攻击端该簇消失，3个通用特征保留。标签是Neuronpedia自动解释，不是人工复核。
• Tab. 5：作者称GPT-2 SAE第6层当前使用的Hk比组合验证所需大约小5倍，因而还不能逐块拼成整模型证明。
• Fig. 13：各层共用Sec. 5的训练超参；作者称后层差距变大这一趋势在其他模型族的Fig. 9、11、12中同样出现。
• 负面结果：重训没有带来“可观的”特征保持（作者原话为preservation is still not substantial）；忠实IRN仍可以特征过窄，从而永远看不到某个可能不安全的特征（Sec. 8）。Qwen在Table 1中没有TC结果。
• 附录C.2写明其余模型族的验证沿用各自激活的围包（JumpReLU、TopK），并称即便高维的Llama 3.2 1B IRN也可以验证。转写文本未给出这些图的逐层端点数字，故不写入表内。

作者指出的局限与后续方向

• 仍是近似：Sec. 8称，尽管重训后的IRN arguably更忠实，它们仍是近似；作者把本文看成通向形式化验证IRN的推动，而不是最终答案。
• 忠实不等于完备：同一节称，即使IRN忠实，特征集合过窄时也可能永远不表示某个（可能不安全的）特征，从而观察不到它。作者认为，训练后差集仍然大，本身可以当作“特征太少”的信号，并指向有通用逼近保证的动态特征扩展（Hornik et al., 1989）。
• 正文验证集中在GPT-2：Sec. 8称主体主要覆盖GPT-2的验证结果；其他IRN的验证被作者看作工程任务，并称Llama 3.2 1B的高维IRN以及其余模型族已在附录C.2.5等处验证。作者认为，设计语言模型及其IRN时就把验证考虑进去，会是有价值的方向。
• 组合验证尚未可行：Sec. 6称，尽管Fig. 5上误差集的界有改进，所用Hk仍然偏小（例如GPT-2 SAE第6层小约5倍，Tab. 5），还不能组合验证整个LLM的忠实性。作者相信结合加时、放大输入集、重训模型块、上游收紧带动下游这四条可以再缩小缝隙，但每条都需要更细的算法，留作未来工作。
• 后续技术方向：Sec. 8与结论展望称，逐层保证为全模型验证（Sec. 6）和跨层transcoder等扩展打基础。未决方向包括各组件的自动对齐，以及在不牺牲模型能力的前提下把差集收得足够紧。
• 披露与复现：伦理声明称，把IRN的脆弱性写明原则上可能帮助想误导解释的对手，但作者认为披露有益，因为同一认识让实践者能认证何时可以信任一个解释。复现声明称代码与Lean形式化随补充材料发布；这是作者对材料状态的陈述，不是已在正文中给出的实验结果。

实验覆盖范围

• 被测模型：Sec. 3与Table 1覆盖GPT-2、Gemma 2 2B、Gemma 3 1B、Llama 3.2 1B、R1-Distill-Qwen 1.5B（表中写作Qwen 1.5B）；前四者含SAE与TC，Qwen行只有SAE。逐层δ图：GPT-2为Fig. 4，其余在附录Fig. 9、11、12，均为200句、MINOR级。
• 训练实验的模型与层：Sec. 5的STD/PGD/SET/LoRA比较做在OpenAI的GPT-2 SAE上，主图为第6层（Fig. 5、Fig. 6）；Fig. 13扩展到第3、5、6、8、10、12层，各层超参相同。论文未报告在Gemma、Llama或Qwen上重复这组训练。
• 扰动与攻击：三级自然语言改写为MINOR、MEDIUM、MAJOR；MAJOR的改写模型是Gemma 2 2B-it。定向解释攻击的细节在附录A：PGD 300步、8次随机重启，对象是Gemma 2 2B第16层SAE的四个生物特征。验证用的是每层局部凸包Hk，不是从嵌入把X经全部注意力与MLP传播到该层。
• 规模与激活：附录C.1写明WikiText-2测试集200句。GPT-2使用ReLU、ε=0.1、dmodel=768；Llama 3.2 1B为TopK、K=32、dIRN=131072、dmodel=2048；R1-Distill-Qwen 1.5B为TopK、K=32、dIRN=65536、28层、dmodel=1536。论文未报告每个条件的随机重复次数。
• 验证器范围：认证的是单层差值网络的ℓ∞界以及由此读出的特征激活区间（附录B.2–B.3）。Sec. 6的逐块含入检查被写成设想；Tab. 5用于说明第6层Hk约小5倍。注意力围包引用Bonaert et al. (2021)，作者称现有围包往往过保守，因而没有报告整模型的端到端认证通过率。

这篇工作把“IRN是否在对抗邻域里复现模型计算”从干净集上的重构损失，改写成可认证的ℓ∞忠实差距，并在五个开源模型族上同时报告攻击上界和验证上界。

• 问题：安全审计常读SAE或transcoder的稀疏特征。这些特征只在替身忠实时才代表模型。Fig. 1显示，同义改写可以让Gemma 2 2B第16层SAE的主导读法从病原体培养变成职场文化，模型权重不变。附录A中该定向攻击的top-8 Jaccard为0.23。
• 方法：同义词嵌入的凸包构成局部集合Hk。Def. 1要求IRN与恒等映射（SAE）或MLP（TC）的差在ℓ∞下不超过δ。CORA用zonotope围包差值网络，并以轴对齐盒上的区间算术避免显式构造dIRN维隐层；二分搜索最小可验证上界，攻击提供下界。预激活区间同时给出不可翻转特征的Jaccard下界。训练侧用可达集损失SET，可与秩8的LoRA结合，对照为STD和PGD。
• 改写实验：WikiText-2上200句、top-20特征。Table 1中GPT-2 SAE的J min从MINOR的0.27降到MAJOR的0.05；Qwen 1.5B SAE从0.37降到0.12。GPT-2的TC明显更高（MAJOR的J min为0.38），Gemma 2 2B则是SAE高于TC。作者把这些数当作攻击上界，并写MINOR、MAJOR相对最差层重叠约−73%与−95%。
• 验证与训练：Fig. 4上GPT-2各层差距都在，第1层SAE可认证到某个δ<1，后层上下界一起变大，TC通常大于SAE。Fig. 5上，SET相对STD把第6层SAE的认证上界约缩小90%，平均活跃特征13.9个（−81%）。Fig. 6上可证保留的top-20特征仍约2–3个。作者将其联系到GPT-2自身：MINOR改写使下一token在21%的样本上翻转。
• 结论与边界：作者称这提供了IRN忠实差距的形式化界，并认为验证感知训练使两个流形对齐。同时写明：重训IRN仍是近似；忠实也不保证特征完备；正文验证主要在GPT-2；第6层Hk约小5倍（Tab. 5），整模型组合验证、跨层TC，以及不牺牲能力的差集收紧，都还是后续工作。