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

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

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.