CAREER: Enabling Trustworthy Complex Learning-enabled Autonomy

Machine learning (ML) is projected to be essential in future autonomy development. However, ML components such as deep neural networks (DNNs) may react unexpectedly to even tiny input variations. Recent incidents in ML-powered systems, such as Tesla and Uber autonomous vehicles, raise an urgent need for techniques and tools to formally verify the safety and robustness of DNNs before utilizing them in safety-critical applications.

The state-of-the-art research, focusing on the safety, robustness, and fairness of deep neural networks and neural network control systems, is powerful and promising for some parts of ML-powered autonomy development. However, enabling trustworthy, complex, learning-enabled autonomy is still challenging due to the need for verification technologies for system-level reactive behaviors involving complex interactions between multiple components.

This project's novelty is in creating new formal method foundations in modeling, specification, verification, and toolchains to address this grand challenge research problem beyond the state-of-the-art. The project's impact is the substantial enhancements of safety, reliability, and explainability of various learning-enabled unmanned systems. Additionally, the project will strengthen the research and study in autonomy-focused topics in Nebraska by recruiting undergraduate research assistants and integrating research findings into ML and autonomy verification courses.

It will also increase the interest and engagement of K-12 group students in STEM majors, science literacy, and broadening participation in computing by participating in outreach events such as the Girl Inc program and The Nebraska College Preparatory Academy Summer Camp. The project team will also collaborate with the University of Nebraska-Lincoln Osher Lifelong Learning Institute to give lectures and discussions for adults on how autonomy concepts and technologies may impact their lives.

This project involves two foundational research thrusts, modeling and specification and quantitative verification, along with software and trustworthy autonomy testbed development and rigorous evaluation. The project's expected research outcomes include 1) a new generic graph-based modeling approach for complex, learning-enabled autonomy (CLeA) in which CLeA's components and their interaction are represented using nodes and edges, respectively, 2) a new set-based algebra, built upon the concepts of probilistic star (or shortly ProbStar, a new variant of the well-known star set) and containing a collection of mathematical propositions and important operators such as parallel composition, decomposition, Minkowski sum, etc., that allow users to discover and keep track of the dependency between multiple reachable sets produced by different components in a CLeA and compose/decompose precise inputs for these components in the analysis, 3) a new set-based specification language to specify CLeA's temporal behaviors based on the concepts of ProbStar set representations, 4) a suite of algebra-based depth first search (DFS) reachability algorithms to construct the reachable set traces of all components in CLeA over multiple steps. and 5) a suite of scalable quantitative verification algorithms to quantify the satisfaction of CLeA's temporal properties under uncertainties.

Results from proposed research thrusts will be integrated into StarV, a new quantitative verification tool, to enhance its verification capacity for various applications. Indoor and outdoor learning-based autonomous driving testbeds using the F1Tenth platform and Robify robot will be developed to evaluate the proposed verification framework. CARLA simulator, SCENIC, and hardware-in-the-loop (HIL) simulation will also be used to assess the proposed research in various project phases.

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.