🤖 machine learning

Formal Mechanistic Interpretability: Automated Circuit Discovery with Provable Guarantees

本文提出了一套利用神经网络验证技术实现自动化电路发现的算法，能够为生成的电路在输入域鲁棒性、鲁棒修补及最小性方面提供可证明的理论保证，并通过实验验证了其相较于传统方法具有显著更强的鲁棒性。

原作者： Itamar Hadad, Guy Katz, Shahaf Bassan

发布于 2026-02-20

📖 1 分钟阅读☕ 轻松阅读

原作者： Itamar Hadad, Guy Katz, Shahaf Bassan

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

这篇论文提出了一种给神经网络“做手术”的新方法，旨在找出神经网络中真正负责做出决策的“核心电路”，并且保证这个发现是绝对可靠、无懈可击的。

为了让你轻松理解，我们可以把神经网络想象成一个巨大的、复杂的交响乐团。

1. 核心问题：乐团里谁在真正演奏？

当这个乐团（神经网络）演奏出一首美妙的曲子（比如识别出一只猫）时，我们想知道：

到底是哪几位乐手（神经元）在真正起作用？
哪些乐手只是在那儿“打酱油”（无关紧要的组件）？

以前的方法（启发式方法）就像是：

指挥家随机叫停几个乐手，看看曲子是不是还听得过去。如果停掉某个乐手，曲子没变，那就觉得这个乐手不重要。

缺点：这就像是在“碰运气”。也许你停掉的乐手刚好在休息，或者你只试了今天天气好的时候。如果换个天气（稍微改变一下输入），或者换个时间，那个乐手可能突然变得至关重要。以前的方法没有保证，一旦环境微调，找到的“核心乐手”可能就不准了。

2. 这篇论文的突破：给乐团做“数学体检”

作者们引入了一套带有“数学保证”的自动化算法。他们不再靠猜，而是用一种叫**“神经网络验证”**的数学工具（就像给乐团做全方位的体检），确保找到的“核心电路”在任何情况下都管用。

他们提出了三种**“铁证如山”的保证**：

A. 输入鲁棒性（Input Robustness）：无论观众怎么变脸，乐手都得稳

比喻：假设观众（输入数据）稍微变个脸（比如猫的照片稍微有点模糊，或者光线暗一点）。以前的方法可能发现：“哦，这个乐手在清晰照片下有用，在模糊照片下没用。”
新方法的保证：我们找到的乐手，无论观众怎么微调（在连续范围内），都能完美演奏。就像找到的核心乐手，不管台下观众是笑是哭，他都能精准地拉出那个音符。

B. 补丁鲁棒性（Patching Robustness）：无论替补怎么换，主力都得稳

比喻：为了测试谁是主力，我们通常会把非主力的乐手“静音”（Patch，即补丁）。以前的方法通常是把静音的乐手换成“零声音”或者“平均声音”。
新方法的保证：我们不仅测试静音，还测试所有可能的替补声音。只要核心乐手在任何可能的替补方案下都能把曲子拉对，那他就是真的核心。这就像说：“不管替补席上坐的是谁，只要核心乐手在，演出就不会崩。”

C. 最小性（Minimality）：只要最精简的“梦之队”

比喻：以前找到的“核心乐手”可能有一堆人，其中几个其实是多余的。
新方法的保证：我们不仅找出了核心，还保证没有一个人是多余的。如果你再踢掉任何一个，演出就会失败。这就是“最小化”——找到那个最精简、最不可或缺的乐手组合。

3. 他们是怎么做到的？（神奇的“双胞胎”技巧）

为了证明这些保证，作者发明了一种叫**“双生子编码”（Siamese Encoding）**的巧妙方法。

比喻：想象你有一对双胞胎。
- 哥哥（完整模型）：演奏整首交响乐。
- 弟弟（候选电路）：只演奏你怀疑是核心的那部分，其他部分被“静音”或“替换”。
验证过程：让这对双胞胎同时上台，面对所有可能的观众（连续输入）和所有可能的替补（连续补丁）。
数学证明：如果弟弟（电路）在任何情况下都能和哥哥（完整模型）唱得一模一样（误差在允许范围内），那么弟弟就是绝对可靠的核心电路。

4. 实验结果：慢一点，但稳得多

代价：这种“数学体检”比以前的“碰运气”要慢（因为要计算所有可能性）。
回报：以前的方法找到的电路，稍微有点干扰就失效了（鲁棒性只有 20%-50%）。而新方法找到的电路，100% 鲁棒！哪怕输入数据有一丁点变化，或者替补方案稍微不同，电路依然完美工作。

总结

这篇论文就像是为神经网络的“黑盒”打开了一扇带锁的安全门。

以前：我们像盲人摸象，摸到哪儿算哪儿，找到的“电路”可能只是暂时的巧合。
现在：我们有了数学上的“验明正身”。我们不仅能找出神经网络里真正干活的那一小部分，还能发誓：这部分在任何合理的干扰下，都能完美工作，而且没有一个是多余的。

这对于AI 安全至关重要。如果你要开一辆自动驾驶汽车，你希望系统里的“刹车电路”是那种“碰运气”找到的，还是这种经过数学证明、在任何路况下都绝对可靠的电路？这篇论文就是为后者铺平了道路。

这是一篇发表于 ICLR 2026 的会议论文，题为《形式化机械可解释性：具有可证明保证的自动化电路发现》（Formal Mechanistic Interpretability: Automated Circuit Discovery with Provable Guarantees）。

该论文针对机械可解释性（Mechanistic Interpretability, MI）中“电路发现”（Circuit Discovery）任务存在的核心缺陷——即现有方法多依赖启发式或近似算法，缺乏在连续输入域上的严格可证明保证——提出了一套基于神经网络验证（Neural Network Verification）技术的自动化算法框架。

以下是该论文的详细技术总结：

1. 问题背景与挑战

核心问题：机械可解释性旨在将神经网络逆向工程为人类可理解的组件（即“电路”）。然而，现有的电路发现方法（如基于采样的消融实验）通常只能保证在离散样本点上电路与模型行为一致。
现有局限：
- 缺乏鲁棒性：微小的输入扰动或补丁（patching）操作的变化可能导致电路的“忠实性”（faithfulness）失效。
- 启发式依赖：大多数算法依赖启发式搜索，无法保证发现的是最小或最简电路。
- 无理论保证：缺乏在连续输入域和补丁域上的形式化证明。
目标：开发一种能够生成具有可证明保证（Provable Guarantees）的电路的自动化框架，确保电路在连续扰动下依然忠实于原模型，并满足最小性要求。

2. 方法论 (Methodology)

论文提出了一套结合神经网络验证与电路发现的新框架，核心包含以下三个技术支柱：

2.1 三种可证明保证类型

作者形式化了三种关键的保证类型，均严格定义在连续域上：

**输入域鲁棒性 **(Input Domain Robustness)：确保电路在连续输入区域（如 $\ell_p$ 球）内，其输出与完整模型输出的差异始终小于阈值 $\delta$ 。
**补丁域鲁棒性 **(Patching Domain Robustness)：解决传统补丁方法（如零值补丁、均值补丁）的任意性问题。要求电路在连续补丁域（即非电路组件的激活值在连续范围内变化）内保持忠实。
**最小性保证 **(Minimality)：形式化了多种“最小”概念，从弱到强包括：
- 准最小 (Quasi-minimal)
- 局部最小 (Locally-minimal)
- 子集最小 (Subset-minimal)
- 基数最小 (Cardinally-minimal，即全局最优)

2.2 核心技术：双生子编码 (Siamese Encoding)

为了利用现有的神经网络验证器（如 $\alpha,\beta$ -CROWN）来验证电路属性，作者提出了双生子网络编码技术：

输入域验证：将完整模型 $G$ 和候选电路 $C$ 堆叠，共享输入层。非电路组件的激活被固定为常数。验证器检查在输入扰动范围内， $G$ 和 $C$ 的输出差异是否始终满足约束。
补丁域验证：构建一个双输入网络。一个分支处理输入 $x$ 以获取完整模型的激活；另一个分支处理输入 $z$ （用于生成补丁值）。电路分支接收 $x$ 但将其非电路组件的激活替换为 $z$ 产生的激活。验证器检查在所有可能的 $z$ 下，电路输出是否忠实。
同时验证：通过扩展编码（Triple Siamese），可同时验证输入和补丁的鲁棒性。

2.3 算法与理论连接

单调性 (Monotonicity)：论文发现了一个关键理论性质——电路单调性。如果忠实性谓词 $\Phi$ 是单调的（即添加组件不会破坏忠实性），那么简单的贪心算法（Algorithm 1）就能收敛到子集最小电路。
理论突破：证明了在特定的输入域和补丁域设置下（满足 $Z \subseteq Z'$ 且激活空间闭合），上述保证是单调的，从而为算法收敛提供了理论依据。
最小电路近似：针对更强的“基数最小”问题，作者利用了电路阻塞集（Circuit Blocking Sets）的对偶性。通过寻找阻塞集的最小击中集（Minimum Hitting Set, MHS），可以高效地近似或精确找到全局最小电路。

3. 主要贡献 (Key Contributions)

形式化定义：首次为电路发现定义了严格在连续域上成立的输入鲁棒性、补丁鲁棒性和多种最小性保证。
理论连接：揭示了输入/补丁鲁棒性与最小性保证之间的深刻理论联系（特别是通过单调性性质），并证明了阻塞集与电路之间的对偶关系。
算法框架：提出了一套自动化算法（基于贪心搜索、二分搜索和 MHS 对偶），能够生成满足上述保证的电路。
实证验证：利用最先进的验证器 $\alpha,\beta$ -CROWN，在多个视觉基准（MNIST, CIFAR-10, GTSRB, TaxiNet）上进行了实验。

4. 实验结果 (Results)

实验在标准视觉模型（如 ResNet, CNN）上进行，对比了采样基线（Sampling-based）与可证明方法（Provable）：

鲁棒性提升：
- 输入鲁棒性：采样方法在连续扰动下的鲁棒性极低（例如 CIFAR-10 上仅约 46.5%，MNIST 上约 19.2%），而可证明方法达到了 100% 的鲁棒性。
- 补丁鲁棒性：传统的零值或均值补丁方法在连续补丁域下鲁棒性同样较低（约 30%-60%），而可证明方法同样达到 100%。
- 代价：可证明方法由于涉及验证查询，计算时间显著增加（从秒级增加到分钟级），但电路大小（Size）与采样方法相当甚至更优。
最小性分析：
- 实验展示了不同算法（贪心、二分、MHS）在电路大小和收敛时间上的权衡。
- MHS 方法虽然计算最慢，但能提供最接近全局最优（基数最小）的电路，且其计算出的下界能有效评估其他算法的优劣。
定性分析：通过 Grad-CAM 可视化发现，可证明鲁棒的电路在对抗扰动下能保持与完整模型一致的注意力分布，而采样电路的注意力会发生偏移。

5. 意义与影响 (Significance)

安全性基石：该工作为机械可解释性奠定了形式化基础。在安全关键领域（如自动驾驶、医疗），仅靠启发式发现的电路是不可靠的，因为微小的扰动可能导致模型行为不可预测。可证明保证消除了这种不确定性。
理论突破：将神经网络验证领域的前沿技术引入机械可解释性，解决了长期存在的“忠实性”定义模糊和缺乏连续域保证的问题。
未来方向：随着神经网络验证技术的扩展（处理更大模型），该方法有望应用于更复杂的模型（如 Transformer），推动可解释性从“定性观察”向“定量保证”转变。

总结：这篇论文通过引入形式化验证技术，成功解决了电路发现中缺乏严格保证的痛点，提出了一套能够生成在连续扰动下依然忠实且最小化的电路的算法，为构建更安全、更可靠的 AI 系统提供了重要的理论工具和实证支持。