类型化仿射决策结构的威力：一项案例研究

TADS（类型化仿射决策结构）是一种新颖、简洁的神经网络白盒表示。在本文中，我们将 TADS 应用于神经网络验证问题，利用它们为期望的神经网络性质生成证明或简洁的错误刻画。在一个案例研究中，我们考虑神经网络对对抗攻击的鲁棒性，即输入上的微小改变会剧烈改变神经网络的感知，并展示 TADS 可用于对鲁棒性错误如何以及在哪里发生提供精确诊断。我们通过引入前置条件投影（Precondition Projection）这一技术实现这些结果，该技术产生一个在给定输入空间子集上精确描述网络行为的 TADS，并将其与 PCA（一种传统的、被广泛理解的降维技术）结合。我们展示了 PCA 易于与 TADS 兼容。所有分析均可利用 TADS 丰富的代数性质以直接的方式实现，证明了 TADS 框架在神经网络可解释性与验证中的效用。尽管 TADS 尚未像最先进的神经网络验证器那样高效扩展，我们展示了通过使用基于 PCA 的简化，它们仍可以扩展到中等规模问题，并为潜在错误生成可用于其他目的（如调试网络或生成新训练样本）的简洁解释。