CAREER: Verified AI in Cyber-Physical Systems through Input Quantization

用神经网络和其他机器学习技术实现的人工智能(AI)的进步已经改变了计算机可以完成的任务。尽管有潜力，但人工智能对网络物理系统(CP)的影响相对较小。许多CP与安全非常重要的物理世界进行交互，因此对于CP来说，99.9%的时间内具有卓越性能的解决方案可能仍然是不可接受的。不幸的是，人工智能系统很难被证明是正确的-很难相信系统总是会做它们设计要做的事情。本研究的目的是推进形式化方法的基础，使基于人工智能的CPS形式化验证实用化。如果成功，这项工作将使人们对人工智能系统产生合理的信任，并允许人工智能应用于与物理世界交互的安全关键流程中。该项目研究了用性能相似且更容易验证的近似来取代人工智能组件的近似方法。研究中探索的主要方法通过首先执行输入量化来近似神经网络或其他机器学习组件。输入量化将连续值的输入舍入为一组有限的离散值，从而允许在输入数量较少时进行穷举。调整量化程度允许在近似值的接近程度(性能)和验证的简易性之间进行权衡。此外，可以使用AI组件的黑盒执行来构建这样的近似，以便所开发的技术可以用于神经网络之外的机器学习组件以及尚未发现的设计。该项目成熟了使用输入量化来证明CP的系统级特性的技术，包括新的核心数据结构和不同的量化和修复方法，以实现对具有AI组件的CP的可扩展闭环验证。这项研究的各个方面将被整合到研究生和本科课程中，以及针对计算机科学中传统上代表性较低的群体的K-12学生的外展努力的一部分。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Advances in artificial intelligence (AI) implemented with neural networks and other machine learning techniques have transformed what computers can accomplish. Despite their potential, AI has had comparatively less impact on cyber-physical systems (CPS). Many CPS interact with the physical world where safety is important, so a solution with superior performance 99.9% of the time may still be unacceptable for a CPS. Unfortunately, AI systems are hard to prove correct — it is difficult to trust the systems will always do what they are designed to do. The goal of this research is to advance the foundations of formal methods in order to make formal verification of AI-based CPS practical. If successful, the work will enable a justified trust in AI systems and allow AI to be applied within safety-critical processes that interact with the physical world. The project investigates approximation approaches where an AI component is replaced by an approximation with similar performance that is easier to verify.The main approach explored in the research approximates a neural network or other machine learning component by first performing input quantization. Input quantization rounds the continuous-valued inputs to a finite set of discrete values, allowing for exhaustive enumeration when the number of inputs is low. Adjusting the degree of quantization allows for a trade off between the closeness of the approximation (the performance) and the ease of verification. Further, such an approximation can be constructed using black-box executions of the AI component, so that the developed techniques can be used on machine learning components beyond neural networks as well as with yet-to-be-discovered designs. This project matures techniques for the use of input quantization to prove system-level properties of CPS, including new core data structures and different quantization and repair approaches to enable scalable closed-loop verification for CPS with AI components. Aspects of the research will be integrated in graduate and undergraduate courses, as well as part of outreach efforts with K-12 students targeting traditionally underrepresented groups in computer science.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.