Verification of Anomaly Detectors

异常检测器的验证

• 批准号: 498974831
• 负责人: Professor Dr. Daniel Neider
• 金额: --
• 依托单位: Professur für Verifikation und formale Garantien des maschinellen Lernens
• 依托单位国家: 德国
• 项目类别: Research Units
• 资助国家: 德国
• 项目状态: 未结题
• 来源: https://gepris.dfg.de/gepris/projekt/498974831?language=en
• 关键词: Verification; Anomaly; Detectors

Anomaly detectors have to work safely and reliably when deployed in safety-critical applications, such as chemical plants. Failure to report anomalies may result in imminent hazards to the environment and human life. False alarms during regular operation may result in unnecessary downtime of plants and, thus, substantial financial or scientific costs. Therefore, this project's overall goal is to develop efficient methods to verify (i.e., to prove formally) the safety and reliability of artificial neural networks used in anomaly detection (Project A1) and data generation (Project A4).While the general topic of verifying artificial neural networks has recently started to receive increasing attention, there is a lack of methods for the types of neural networks that will arise in this research unit: neural networks on multi-modal sequential data that are trained in unsupervised learning settings. With this project, we will contribute to closing this gap, thereby substantially advancing the state of the art in neural network verification.First, we will elicit correctness properties that neural networks need to satisfy to operate safely and reliably - both in the context of this research unit and beyond. To this end, we will closely collaborate with Projects A1 and A4 as well as with Projects B1 and B2.Second, we will formalize the elicited correctness properties. This task will entail developing a novel temporal logic, provisionally entitled Neural Temporal Logic (NTL), that we will specifically tailor to neural networks over multi-modal sequential data. With this new logic, it will also become possible - for the first time - to express (and verify) "fuzzy" properties such as "an alarm has to be triggered when the gas in a given pipe starts to condensate".Third, we will develop efficient algorithms to verify neural networks against correctness properties expressed in NTL. We will consider both qualitative verification methods (proving or disproving that a network satisfies a property) and quantitative verification methods (computing the probability of a network satisfying a property). For both settings, we will develop two orthogonal types of verification algorithms: one operating on the actual neural network and one computing property-preserving abstractions. Since one can, in general, not hope that every neural network will immediately satisfy all correctness properties, we intend to also develop techniques that use counterexamples (obtained from failed verification attempts) to "repair" neural networks so that they fulfill the correctness properties. We will evaluate our algorithms empirically on the neural networks produced in Projects A1 and A4.

当部署在安全关键应用（如化工厂）时，异常检测器必须安全可靠地工作。不及时报告异常可能会对环境和人类生命造成迫在眉睫的危害。正常运行中的误报可能导致工厂不必要的停机，从而造成大量的财务或科学成本。因此，该项目的总体目标是开发有效的方法来验证（即正式证明）用于异常检测（项目A1）和数据生成（项目A4）的人工神经网络的安全性和可靠性。虽然验证人工神经网络的一般主题最近开始受到越来越多的关注，但缺乏针对该研究单元将出现的神经网络类型的方法：在无监督学习设置中训练的多模态序列数据的神经网络。通过这个项目，我们将有助于缩小这一差距，从而大大推进神经网络验证的最新技术。首先，我们将引出神经网络需要满足的正确性属性，以安全可靠地运行——无论是在本研究单位的背景下还是在其他地方。为此，我们将与A1和A4项目，以及B1和B2项目紧密合作。其次，我们将形式化推导出的正确性属性。这项任务将需要开发一种新的时间逻辑，暂时称为神经时间逻辑（NTL），我们将专门针对多模态序列数据的神经网络进行定制。有了这种新的逻辑，它也将成为可能——这是第一次——表达（并验证）“模糊”属性，比如“当给定管道中的气体开始冷凝时，必须触发警报”。第三，我们将开发有效的算法来验证神经网络是否符合NTL中表达的正确性。我们将考虑定性验证方法（证明或否定网络满足某一属性）和定量验证方法（计算网络满足某一属性的概率）。对于这两种设置，我们将开发两种正交类型的验证算法：一种操作在实际的神经网络上，另一种计算保持属性的抽象。因为一般来说，我们不能指望每个神经网络都能立即满足所有的正确性属性，所以我们还打算开发一些技术，使用反例（从失败的验证尝试中获得）来“修复”神经网络，使其满足正确性属性。我们将在项目A1和A4中产生的神经网络上对我们的算法进行经验评估。