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

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.