通过形式化方法实现可验证的、针对性的解释

深度神经网络在自主驾驶和医疗诊断等安全关键领域得到部署，利益相关者需要可解释且具有形式保证的解释。现有XAI方法不足：启发式归因方法（如LIME、积分梯度）指示影响特征但未对决策边界提供数学保证；而形式方法验证鲁棒性却是无针对性的，分析最近的边界而不关心其是否代表关键风险。在安全关键系统中，所有误分类并不等价；将“停止”标志误认“60公里/小时”标志远比将其误认“禁止超车”标志更危险。我们引入ViTaX（Verified and Targeted Explanations），一种形式化XAI框架，生成具有数学保证的针对性准解释。对于给定输入（类别y）和用户指定的关键备选类别（类别t），ViTaX：（1）识别对y→t转换最敏感的最小特征子集，（2）应用形式可达性分析，保证对这些特征施加epsilon扰动无法将分类翻转为t。我们通过面向特定目标类的epsilon鲁棒性进行形式化，认证特征子集在扰动针对特定目标类别时是否保持鲁棒性。ViTaX是首个为模型对用户识别的备选方案提供形式保证解释的方法。在MNIST、GTSRB、EMNIST和TaxiNet上的评估显示，解释保真度提高超过30%，且解释基数最小。