Verification of Anomaly Detectors

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

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.