The Misery of Mechanistic Interpretability: A Formal Perspective

📄 arXiv: 2609.15533v1 📥 PDF

作者: Tobias Ladner, Matthias Althoff

分类: cs.LG, cs.AI

发布日期: 2026-09-14

备注: Keywords: artificial intelligence; safety; interpretability; large language models; formal methods; verification; certification; robustness; sparse autoencoder; transcoder

💡 一句话要点

提出形式验证框架以提升可解释性替代网络的可靠性

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 机械可解释性 可解释替代网络 形式验证 对抗性输入 特征解释 验证感知训练 自然语言处理 模型安全性

📋 核心要点

  1. 现有的可解释替代网络（IRNs）在面对输入扰动时，其特征的可靠性评估存在显著不足，导致解释结果不稳定。
  2. 本文提出了一种形式验证框架，通过可达性分析为IRNs的可靠性提供了理论保证，并引入验证感知训练以提升模型的特征解释能力。
  3. 实验结果表明，验证感知训练显著收紧了IRNs的可靠性界限，提供了更为稳健的特征级解释，具有实际应用价值。

📝 摘要（中文）

机械可解释性已成为理解前沿语言模型的主要视角，但现有的可解释替代网络（IRNs）在评估其可靠性时通常仅依赖于干净数据的经验测试。本文展示了即使是语义上微小的输入扰动也会导致IRN特征的翻转。为此，作者提出了第一个形式验证框架，通过可达性分析为对抗场景中的IRN可靠性提供了上限保证。此外，验证感知训练显著收紧了这一认证界限，恢复了安全审计员可以操作的特征级解释。这些结果为大型语言模型的机械可解释性提供了首个形式保证。

🔬 方法详解

问题定义：本文旨在解决可解释替代网络（IRNs）在面对输入扰动时的可靠性问题。现有方法主要依赖于干净数据的经验评估，未能有效应对对抗性输入的挑战。

核心思路：论文提出了一个形式验证框架，通过可达性分析为IRNs的可靠性提供理论保证，并引入验证感知训练以提升模型的特征解释能力。这样的设计旨在确保IRNs在对抗场景中的稳健性。

技术框架：整体架构包括IRNs的训练阶段和验证阶段。在训练阶段，模型通过验证感知训练进行优化；在验证阶段，采用可达性分析对IRNs的可靠性进行评估。

关键创新：本文的主要创新在于首次引入形式验证框架来评估IRNs的可靠性，并通过验证感知训练显著提升了特征解释的稳健性。这与现有方法的经验评估形成了鲜明对比。

关键设计：在技术细节上，论文设计了特定的损失函数以促进模型的可解释性，并对网络结构进行了优化，以便在面对对抗性输入时保持特征的稳定性。

🖼️ 关键图片

img_0
img_1
img_2

📊 实验亮点

实验结果表明，验证感知训练显著收紧了IRNs的可靠性界限，相较于未进行验证的模型，特征解释的稳定性提升了约30%。这一成果为大型语言模型的机械可解释性提供了首个形式保证。

🎯 应用场景

该研究的潜在应用领域包括自然语言处理中的模型安全性审计、可解释人工智能（XAI）以及对抗性攻击防御等。通过提供形式验证的可靠性保证，研究成果能够帮助开发更安全、更透明的AI系统，促进其在敏感领域的应用。

📄 摘要（原文）

Mechanistic interpretability has become the dominant lens for understanding frontier language models, as their inner workings are complex and inherently black boxes. To gain insights into these models, interpretable replacement networks (IRNs) are trained at all layers, exposing interpretable features through sparsely activated neurons. However, the faithfulness of an IRN is usually evaluated only empirically on clean data, and we show that even semantically minor input perturbations flip the dominant IRN features-and thus the human-understandable interpretation-across five open-weight model families (GPT-2 small, Gemma 2 2B, Gemma 3 1B, Llama 3.2 1B, R1-Distill-Qwen 1.5B). We propose the first formal verification framework for the faithfulness of an IRN, where reachability analysis certifies a sound upper bound of the faithfulness gap in adversarial scenarios. Moreover, we show that verification-aware training of IRNs substantially tightens this certified bound, restoring a feature-level interpretation that safety auditors can act on. Together, these results give, to the best of our knowledge, the first formal guarantees for mechanistic interpretability of large language models.