论文标题
CheckInn：Imandra（扩展）中的广泛范围神经网络验证
CheckINN: Wide Range Neural Network Verification in Imandra (Extended)
论文作者
论文摘要
神经网络越来越依赖为复杂安全系统（例如自动驾驶汽车）的组成部分。对在更大的验证周期中嵌入神经网络验证的工具和方法的需求很高。但是，由于感兴趣的广泛验证属性，很难进行神经网络验证，每个验证范围通常仅适用于专用求解器中的验证。在本文中，我们展示了最初设计用于验证，验证和仿真金融基础架构的iMandra，以及一种定理供体，可以为神经网络验证提供整体基础架构。我们开发了一个新颖的图书馆Checkinn，该图书馆在Imandra的神经网络中形式化，并涵盖了神经网络验证的不同重要方面。
Neural networks are increasingly relied upon as components of complex safety-critical systems such as autonomous vehicles. There is high demand for tools and methods that embed neural network verification in a larger verification cycle. However, neural network verification is difficult due to a wide range of verification properties of interest, each typically only amenable to verification in specialised solvers. In this paper, we show how Imandra, a functional programming language and a theorem prover originally designed for verification, validation and simulation of financial infrastructure can offer a holistic infrastructure for neural network verification. We develop a novel library CheckINN that formalises neural networks in Imandra, and covers different important facets of neural network verification.
