NSF-BSF: SHF: Small: Certifiable Verification of Large Neural Networks

软件系统在现代生活的几乎每个领域都扮演着重要的角色。为了降低开发新软件的难度，人工智能（AI）领域的研究一直在推广一种新的编程模式：不是让人类工程师设计和编码算法，而是将一组训练样例与机器学习算法一起使用，以自动推断软件实现。在经典编程中，由于这些代码是由人类编写的，我们可以说服其他人它是正确的。然而，在机器学习系统中，程序相当于将输入转换为输出的高度复杂的数学公式。然而，关键的困难在于，目前还不可能对这种系统的正确性进行推理。该项目通过开发一种名为Reluplex的算法来解决这个问题，该算法能够证明深度神经网络（dnn）的属性，或者在属性不成立时提供反例。该项目有三个主要目标。首先，研究人员开发了算法技术，以大大减少需要通过验证工具探索的状态数量。其次，他们开发了一种生成可检查验证证明的策略。可检查的正确性证明使得不需要依赖验证工具的正确性；相反，人们只能依赖于一个小型可信的证明检查器的正确性。最后，研究人员在一个开源工具中实现了这种方法，并在现实世界的工业dnn上进行了评估。鉴于人工智能组件在安全关键系统（如自动驾驶汽车）中变得无处不在，这项研究将增加对这些系统的信任。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Software systems play important roles in almost every area of modern life. In order to reduce the difficulty of developing new software, research in the field of artificial intelligence (AI) has been promoting a new model of programming: instead of having a human engineer design and code algorithms, a set of training examples are used together with machine-learning algorithms to automatically extrapolate software implementations. In classical programing, because such code is written by humans, we can persuade others that it is correct. In machine-learned systems, however, the program amounts to a highly complex mathematical formula for transforming inputs into outputs. The key difficulty, however, is that it is not possible currently to reason about correctness in such systems.This project addresses this issue by developing an algorithm, called Reluplex, capable of proving properties of deep neural networks (DNNs) or providing counter-examples if the properties fail to hold. The project has three main objectives. First, the investigators develop algorithmic techniques to greatly reduce the number of states that need to be explored by a verification tool. Second, they develop a strategy for producing checkable verification proofs. Checkable correctness proofs make it unnecessary to rely on correctness of the verification tool; one can instead rely only on the correctness of a small trusted proof-checker. Finally, the investigators implement this approach in an open-source tool and evaluate it on real-world industrial DNNs. Given that AI components are becoming ubiquitous in safety-critical systems, such as autonomous vehicles, this research will increase trust in these systems.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.