研究者提出可认证机制编辑：在连续输入区域上证明技能移除与保留

现有机理编辑（如消融、权重编辑、激活引导）仅依赖测试集验证有害能力的消除与有用能力的保留，无法覆盖连续输入空间，且无法在理论上保证移除的彻底性。

• 测试验证的局限性：作者指出，测试集只能回答已测试输入上的表现；越狱攻击往往发生在安全训练分布之外，通过基准测试的遗忘编辑容易被分布外输入逆转。
• 形式化可解释性研究的空白：作者认为，现有将形式化验证引入可解释性的工作主要验证模型的描述性属性（如电路忠实性、计算内容或稳定性），未证明编辑操作在连续输入区域上的实际行为效果。
• 黑盒测试的不可行性假设：作者假设任何有限的确定性黑盒测试（包括自适应查询）都无法排除模型中残留的微小存活区域（survivor pocket），普通训练即可产生通过全部测试的干预幻觉。
• 特征非干涉的安全保证：论文提出基于形式化证明的机理编辑认证框架，并从信息流安全视角将能力移除定义为特征非干涉，即编辑后组件的输出在整个连续区域内证明独立于被禁止的输入特征。
• 威胁模型：
  • 攻击者目标：寻找使被编辑模型重新触发被消除技能（即输出大于 0）或破坏保留技能的存活输入。
  • 攻击者知识与能力：具备有限次查询的确定性黑盒测试能力（允许自适应查询），或在连续嵌入球内通过投影梯度攻击实施对抗扰动。
  • 受害系统：经神经元消融、权重置零、激活引导或 SAE 特征钳位编辑的神经网络（涵盖分段线性 ReLU 模型至标准 Transformer）。

可解释性形式化验证（描述轴）

• 模型精度与电路属性验证：Gross et al.（2024）在小域上验证未编辑模型的准确率下界；Hadad et al.（2026）验证发现电路在激活补丁下的忠实性与最小性；Anani et al.（2026）验证电路在数据集重采样下的稳定性。作者指出这些工作验证的是固定模型的描述是否保真，不涉及编辑对任务行为的改变。
• 可验证 Transformer 解释：Somani（2026）使用 SMT 求解器验证电路解释的四个描述性属性（计算内容、逐输入边必要性、最终残差鲁棒性等）。作者指出该工作明确声明不保证编辑的行为效果，其对模型的修改仅是为了便于求解器验证而剥离组件。

模型编辑证书与统计保证

• 权重编辑输出偏差界：Andric（2025）为权重编辑提供证书，但约束的是有限提示词集上的输出偏差界。作者指出该界衡量的是输出改变了多少而非行为变成了什么，且有限提示词测试无法排除目标技能存活。
• 统计遗忘与因果保真度：Koloskova et al.（2025）提供训练数据层面的统计不可区分性保证；Asiaee（2026）提供自适应干预采样下的随时有效置信序列；Pandey & Kulkarni（2026）刻画数据分布间的移除-保留前沿。作者指出这些工作属于平均情况或过程保证，不保证单模型在连续区域内的最坏情况行为。

黑盒不可行性与安全非干涉

• 黑盒探测局限：Bakman et al.（2026）证明静态黑盒探测无法区分模型是否隐藏对抗行为；Yang & Yeung（2026）给出无 oracle 遗忘认证的经验有限查询不可行性。本文的 Proposition 3 则针对确定性自适应黑盒测试给出了严格不可能定理。
• 几何信息流控制：Storek et al.（2026）在智能体中验证不受信输入到敏感动作的零信息流。作者称本文首次将非干涉性质用于验证机理编辑的行为效果。

对比基线与基准设置

• 基线与对比方法：论文在自建的合成规则、模加法及引用上下文中评测，对比了密集网格测试（15×15 与 201×201 网格）、随机采样测试（300 至 1,000 点），以及消融（ablation）、权重编辑（weight edit）、靶向抑制（targeted steering）、均值差引导（diff-of-means steering）和稀疏自编码器特征钳位（SAE clamp）。

作者定位

• 作者称现有形式化解释工作聚焦于“该解释是否保真”，而本文回答“对电路采取干预后会发生什么”，首次在连续输入区域上对机理编辑提供最坏情况下的技能移除与保留形式化保证。

论文提出机理编辑形式化认证框架（Certified Mechanistic Edits），将网络权重与输入区域转换为逻辑约束，结合 SMT 精确求解与边界传播，数学证明编辑在整个连续输入区域内使目标技能消失且保留技能不被破坏。

问题形式化与断言定义

• 模型与断言形式化：考虑分段线性网络，所有权重为有理数。断言表示为三元组 (h, R, ▷)，其成立条件为： \forall x \in R : g_h(x) \triangleright 0 该公式表示在闭箱区域 R 内的所有输入，模型输出头 h 均严格大于或小于等于 0。
• 技能移除与保留：设待移除技能为 A、保留技能为 B。移除证明即证明断言 (A, R_A, ≤) 成立；保留证明即证明 B 在其指定区域上保持原有符号方向。
• 认证半径与区域扩张：为衡量编辑对扰动的鲁棒性，将区域 R 沿各维度向外扩张 ε 得到 R_ε。认证半径定义为： \varepsilon^* = \sup\{\varepsilon \in [0, \varepsilon_{\max}] : (h, R_\varepsilon, \triangleright) \text{ 对 } g \text{ 成立}\} 该公式定义了使断言在扩张区域 R_ε 上持续成立的最大扩张半径上限。

SMT 精确求解与凸包松弛

• 精确有理数编码：将网络权重转化为精确分数，ReLU 转化为条件分支式。通过向 Z3 求解器断言否定命题进行求解；若返回 unsat 则证明断言在全域成立，若返回 sat 则输出具体的违例反例。
• 标记序列的凸包松弛：离散 token 序列的布尔编码会导致求解器分支爆炸；论文采用凸包松弛（hull relaxation），用嵌入单纯形上的连续混合权重替代离散选择，由于松弛区域是离散输入的超集，unsat 结果可直接保证离散序列下的断言成立。
• 浮点误差松弛处理：求解器基于精确有理数，而实际执行基于 float64。论文证明两者前向误差界约为 10^-13，因此在验证时引入松弛裕度（玩具模型取 γ = 10^-9，门控 Transformer 取 10^-6），确保证明结论向浮点执行程序迁移。

边界传播扩展与攻击夹逼

• 非线性组件的声音松弛：Softmax 与 LayerNorm 包含指数与除法，超出线性算术范畴。论文引入 CROWN 边界传播工具计算输出上下界；该方法具有健全性（soundness），即绝不认证错误断言，但可能因松弛不完备而漏报。
• 投影梯度攻击夹逼：在超出精确求解能力的边界之外，采用基于投影梯度的对抗攻击（projected-gradient attack）从上方寻找反例半径，形成双向夹逼区间，用两者间隙量化证明器的松弛程度。

特征非干涉认证

• 双副本孪生编码：为证明编辑后的输出在机制上完全独立于被禁特征，构建包含两份网络副本的孪生结构（siamese encoding），输入 x 与 y 仅在被禁坐标上允许自由变动。
• 影响度二分求解：求解器判断是否存在输入对满足输出差绝对值大于 κ。通过对 κ 二分搜索求解最小上界；当证明 κ = 0 成立时，即严格认证了特征非干涉。

实验设置

• 被测模型：共 6 个模型，涵盖两输入单隐藏层 ReLU 玩具模型（Toy MLP separated 与 entangled，隐藏层宽 16）、3-12-8-2 深度 MLP、8 宽 2 头 6 层门控 Transformer（Gate transformer）、p=5 且 8 宽 2 头的模加 Transformer（Adder transformer），以及 64 宽 4 头 2 层的标准 Softmax + LayerNorm Transformer。
• 测试任务与区域：玩具模型采用 [0, 1]^2 连续域上的规则分类任务（x0 > 0.5 为技能 A，x1 > 0.5 为技能 B）；门控 Transformer 采用包含连续嵌入噪声的多序列任务（48 维扰动）；模加 Transformer 评测 625 个干净序列的独立位置模 5 加法（40 维扰动）；Softmax + LN Transformer 评测包含引用标记上下文的任务（448 维扰动）。
• 编辑方法变体：包括隐藏神经元消融（ablation）、头与神经元权重置零（weight edit）、靶向常数抑制（targeted steering）、基于均值差的激活引导（diff-of-means steering）以及稀疏自编码器特征钳位（SAE feature clamp）。
• 评测指标：技能移除认证半径与保留认证半径（ε*）、攻击破坏半径（attack radius）、双副本特征非干涉认证影响度（κ）。
• 判定与证明方式：采用 Z3 SMT 求解器进行无量词线性实数算术求解（判定 unsat / sat）；对非线性 Transformer 采用 CROWN 边界传播求解下界，并辅以投影梯度攻击给出上界；辅以网格搜索及随机投点对比。
• 样本量与重复规模：干预幻觉实验覆盖 160 个训练模型（输入维度 2 至 5 维各 80 个模型合并），采用 40,401 点网格、1,000 个随机输入及 2×10^6 次均匀随机投点进行统计检验。

主结果

表格较宽，可左右滑动

（据 Table II。Toy MLP、Deep MLP 与 Adder transformer 移除半径在搜索上限处饱和；Softmax + LN transf. 移除半径与保留半径均受攻击半径夹逼，攻击破坏半径分别为 0.03、0.05 与 0.1；Adder transformer 同时在全部 625 个干净序列上证明了精确正确性。）

• 全输入区域行为保证成立：作者称，无论是在双输入网络还是标准非线性 Transformer 上，编辑后的技能移除与保留均能在连续输入区域内获得数学证明，打破了有限测试集覆盖不全的局限。
• 精确求解器能同时处理全序列与连续球：作者称，结合凸包松弛与 SMT 编码，精确求解器可在单次查询中一次性覆盖离散 token 序列组合与连续嵌入扰动空间。
• 认证边缘紧贴模型真实判定边界：作者称，在玩具模型上，认证区域在扩张后直接终止于模型自身的决策边界处，残余微小间隙来自模型本身的判定裕度，而非证明工具的松弛。

黑盒测试不可行性与干预幻觉

• 测了什么：评估有限测试集能否可靠验证技能移除，检验是否存在通过测试但实际保留技能的干预幻觉模型（Figure 1）。
• 实验结果：人工构造的编辑模型通过了 40,401 个点的密集网格测试和 300 个随机点测试，且技能 B 的保留完全得证，但求解器检测到宽度仅 0.0006 的存活带（Figure 1a, 1b）；在对 160 个自然训练模型的自动化测试中，输入维度为 4 和 5 的模型中共出现 3 个幻觉模型（2 维为 0/49，3 维为 0/100，4 维为 2/92，5 维为 1/106，Figure 1c），它们通过了密集网格与 1,000 个随机点测试，但在 2×10^6 次均匀随机测试中无一命中，Clopper-Pearson 95% 置信上限表明其存活区域体积小于全域的 1.5×10^-6。
• 作者解读：作者称该结果证实了 Proposition 3，说明干预幻觉是普遍存在的现象而无需对抗构造，有限确定性黑盒测试在原理上无法认证技能移除。

手术式编辑与激活引导的附带损害对比

• 测了什么：对比神经元消融、权重编辑等手术式编辑与基于均值差的激活引导在移除技能 A 时对保留技能 B 的附带损伤（Figure 6）。
• 实验结果：在分离和纠缠玩具模型上，消融、权重编辑和靶向抑制使技能 B 的认证半径完全保持不变（分别为 0.0996 和 0.0961）；而均值差引导随着剂量增加，技能 B 的认证半径呈严格线性下降（分离模型上剂量 4 时降至 0.0908，剂量 16 时降至 0.0656，拟合优度 R^2 ≥ 0.999），直至保留断言被彻底推翻（Figure 6a, 6b）。在 Softmax Transformer 上，不存在任何既能移除技能 A 又能保留技能 B 的引导剂量。
• 作者解读：作者称该结果证实了 Proposition 4，证明手术式编辑能实现零附带损伤，而数据驱动的引导向量必然按剂量线性侵蚀保留技能裕度，无法彻底调和移除与保留的冲突。

特征非干涉认证实验

• 测了什么：通过双副本架构评估编辑后模型输出是否在机制上完全独立于被禁输入特征（Figure 4）。
• 实验结果：在 Softmax + LN Transformer 上，编辑后的认证影响度严格达到 0，说明读出输出完全忽略了被禁用的引用内容，且该非干涉成立半径超过了单纯的移除半径；在玩具模型上，手术式编辑将影响度从 22 压缩至 0.001 以下；在故意构造的纠缠模型上，编辑虽然认证了移除，但影响度仅从 63 降到 10；对于幻觉模型，求解器反驳了非干涉并测得与帽形高度一致的 0.60 影响度上限。
• 作者解读：作者称输出低于阈值不等于内部对特征脱敏，特征非干涉证明提供了比单纯数值截断更强的安全性判定。

其他消融与分析

• 求解器前沿与规模伸缩（Table III）：门控 Transformer 在 8 宽 1 头 6 层（48 变量）下 ε=0.005 用时 230 秒，但在 12 宽或 16 宽（72 与 96 变量）下 ε=0.005 均超过 300 秒超时。
• 复合分布式电路消融（Figure 3）：在门控 Transformer 上，仅关闭注意力头或仅关闭 3 个 MLP 神经元均会导致技能 A 持续触发，必须联合消融方能认证移除。
• 边界传播声音性验证 M0（Section IV-B）：在双输入 ReLU 玩具模型上，CROWN 计算出的移除半径（0.5）与两项保留半径（0.0996）与 SMT 精确求解器完全一致。
• 稀疏自编码器特征钳位（App. D）：在技能 A 分布于 3 个特征的模型中，SAE 钳位取得 ≥0.5 的移除半径和 0.064 的保留半径（消融保留半径为 0.100）。
• 离散与连续扰动尺度对比（Section V-F）：单个 token 替换在嵌入空间的最小位移为 2.94，约为连续认证球半径的 324 倍。
• 浮点执行间隙分析（App. B）：在零裕度边界构造断言中，SMT 证明在实数域成立，但在 float64 下约四分之一区域产生约 10^-16 的浮点违例。

负面结果与例外

• 引导在 Transformer 上的调和失败：在 Softmax + LayerNorm Transformer 上，作者报告均值差引导在任何测试剂量下都无法同时满足移除技能 A 和保留技能 B。
• 精确求解器的扩展超时：在门控 Transformer 达到 8 层（64 变量）时，凸包松弛失效（too loose）；达到 16 宽 2 头 8 层（128 变量）时，即使放宽至 30 分钟也全部超时（Table III）。
• 组件不可分性：在从头训练的标准 Softmax Transformer 中，贪婪搜索未能找到可分离的头/MLP 电路，因此只能退而求其次采用位置作用域的注意力敲除。

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

• 模型规模较小与求解器扩展瓶颈（Section VI Scale）：当前保证仅在小型、标准架构网络上获得证明；精确前沿受内部条件分支的指数级组合限制，边界传播虽声音但不完备，与攻击半径之间的较宽间隙反映了证明器的松弛。
• 边界传播在零半径退化（Section VI Scale）：CROWN 松弛在 ε = 0 处退化，因此二分搜索仅能探测并报告半径 ≥ 10^-4 的球。
• 未能在标准架构中定位离散组件电路（Section VI Scale）：在从头训练的标准 Softmax Transformer 中，贪婪搜索未能发现可分离的头/MLP 电路，迫使编辑采用位置作用域注意力路径敲除而非组件级电路编辑。
• 连续嵌入噪声不等于离散提示词鲁棒性（Section VI Input region instead of arbitrary prompt）：认证保证定义在标记序列 × 连续嵌入球上，单 token 替换位移是认证球的约 324 倍，不能外推为前沿大模型上的离散提示词鲁棒性。
• 依赖可判定 Ground Truth 规格的假设（Section VI The decidable-oracle assumption）：被测技能均具备明确可计算的规则函数，而前沿模型的真实危害行为缺乏此类判定标准，输出是否表现出危害通常存在争议且一般不可判定，该假设无法直接迁移到真实场景。
• 预训练小语言模型与真实技能验证（Section VII Conclusion and Future Work）：作者计划下一步在具备真实安全能力的预训练小语言模型上评测边界传播，并引入离散编辑距离证书以补充连续证书。

实验覆盖范围

• 被测网络架构共 6 种：实验覆盖 2 种双输入单层 ReLU 玩具模型、1 种深度 MLP、1 种门控 Transformer、1 种模加 Transformer 和 1 种 2 层 Softmax+LN Transformer，全部为小规模网络。
• 测试任务均为人工构造的可计算规则：包括二维平面阈值切分规则、模 5 算术运算以及合成的引用标记上下文任务，未测试真实自然语言有害数据集。
• 最大扰动维度为 448 维：连续扰动范围限制在输入域的闭箱扩张或嵌入空间中的 L_∞ 连续噪声球，未测试更大规模嵌入维度。
• 编辑技术涵盖五种变体：包括神经元消融、权重置零、靶向抑制、均值差引导以及 SAE 特征钳位。
• 未报告真实前沿模型及大参数量架构：论文未在任何前沿开源或闭源大模型上运行形式化验证，也未报告真实越狱或非对齐风险下的防御实验。

• 论文定位：论文提出了机理编辑的行为级形式化认证框架，在连续输入区域上证明了模型编辑对目标技能的消除和对有用技能的保留。
• 要解决的问题：现有机理编辑依赖测试集进行经验评估，不仅无法覆盖连续输入空间，而且无法防御分布外越狱；论文证明了有限黑盒测试在理论上无法保证技能完全移除。
• 核心方法设计：基于有理数对分段线性模型进行 SMT（Z3）精确编码，通过凸包松弛处理全 token 序列搜索；针对 Softmax 和 LayerNorm 等非线性操作引入 CROWN 边界传播计算声音下界，辅以投影梯度攻击双向夹逼，并利用孪生架构认证特征非干涉。
• 关键实验结果：
  1. 在 Softmax + LayerNorm Transformer 上，边界传播证明位置作用域编辑消除了技能 A 并保留技能 B，在 448 维嵌入扰动下移除认证半径达到 0.0091，保留半径达到 0.0079 与 0.0098（Figure 2）。
  2. 理论证明有限确定性黑盒测试无法认证移除（Proposition 3），在 160 个自然训练模型中发现 3 个通过密集测试但在 SMT 下被反驳的幻觉模型，存活区域体积小于全域的 1.5×10^-6（Figure 1）。
  3. 理论与实验均证明手术式编辑能实现零附带损伤，而均值差引导会按剂量线性侵蚀保留技能裕度（拟合优度 R^2 ≥ 0.999），在 Transformer 上无法同时实现移除与保留（Figure 6）。
• 结论与安全启示：作者认为形式化证明可以替代经验测试集作为安全编辑生效的确凿依据，但要走出玩具与已知公式范畴，必须首先建立针对真实有害能力的确定性或概率性形式化判定规格。