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

利用神经网络和其他机器学习技术实现的人工智能（AI）的进步已经改变了计算机可以完成的任务。尽管人工智能具有潜力，但它对网络物理系统（CPS）的影响相对较小。许多CPS与物理世界进行交互，其中安全性非常重要，因此在99.9%的时间内具有上级性能的解决方案可能仍然无法接受CPS。不幸的是，人工智能系统很难证明是正确的-很难相信系统会一直做它们被设计做的事情。本研究的目标是推进形式化方法的基础，以使基于AI的CPS的形式化验证实用。如果成功，这项工作将使人们对人工智能系统产生合理的信任，并允许人工智能应用于与物理世界交互的安全关键流程。该项目研究了近似方法，其中人工智能组件被替换为具有类似性能的近似，更容易验证。研究中探索的主要方法通过首先执行输入量化来近似神经网络或其他机器学习组件。输入量化将连续值输入舍入为离散值的有限集合，从而允许在输入数量较低时进行穷举枚举。调整量化的程度允许在近似的接近度（性能）和验证的容易性之间进行权衡。此外，这种近似可以使用AI组件的黑盒执行来构建，因此所开发的技术可以用于神经网络之外的机器学习组件以及尚未发现的设计。该项目成熟了使用输入量化来证明CPS的系统级属性的技术，包括新的核心数据结构和不同的量化和修复方法，以实现具有AI组件的CPS的可扩展闭环验证。该研究的各个方面将被整合到研究生和本科生课程中，以及针对传统上代表性不足的计算机科学群体的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.