论文标题
Imandra中的神经网络：矩阵表示作为验证选择
Neural Networks in Imandra: Matrix Representation as a Verification Choice
论文作者
论文摘要
随着神经网络已部署在越来越多的安全至关重要的应用中，对神经网络的正式验证工具的需求增加了。矩阵是形式化神经网络必不可少的数据结构。功能编程语言鼓励矩阵定义的各种方法。此功能已经在不同的应用程序中成功利用。我们问的问题是，这些想法是否以及如何应用于神经网络验证。功能编程语言Imandra结合了功能编程语言的语法和自动定理供体的力量。使用Imandra的这两个关键特征，我们探讨了不同的矩阵实现如何影响神经网络验证的自动化。
The demand for formal verification tools for neural networks has increased as neural networks have been deployed in a growing number of safety-critical applications. Matrices are a data structure essential to formalising neural networks. Functional programming languages encourage diverse approaches to matrix definitions. This feature has already been successfully exploited in different applications. The question we ask is whether, and how, these ideas can be applied in neural network verification. A functional programming language Imandra combines the syntax of a functional programming language and the power of an automated theorem prover. Using these two key features of Imandra, we explore how different implementations of matrices can influence automation of neural network verification.
