Assured Autonomy (2018 - 2022)

Introduction

Intelligent autonomous systems are being increasingly applied to various domains and industries, due to advances in modelling, sensing, algorithm design and other technologies. However, formal safety assurances for these systems has not kept pace with these advances: this is because autonomous systems rely heavily on machine learning technologies, which lack the necessary mathematical framework to provide guarantees on correctness. Without assurances, trust in the safety and operation of any learning-enabled cyber-physical system (LE-CPS) will be limited, hampering their broad deployment.

This project aims to address this challenge by developing new mathematical approaches and tools for the verification of data-driven ML algorithms in these systems to enhance their autonomy and assure they are achieving an acceptable level of safety.

Motivation

Cyber-Physical Systems (CPSs) with learning components are increasingly being deployed in safety-critical applications. However formal verification methodologies only offer limited support for the safety analysis of such systems. The project aims to fill this gap by developing new algorithms and software toolkits for the verification of learning-enabled CPSs (LE-CPSs).

Objectives and current results

To enable the development of verification methods, the project aims at defining semantic models and formal specification languages for LE-CPSs. Our efforts are focussed on two main objectives:

• the analysis of neural networks in isolation and
• the analysis of interactions between several learning-enabled components and the environment.

Our group contributed several techniques to verify neural networks via, e.g., Mixed-integer Linear Programming or Symbolic Interval Propagation. Our approaches present state-of-the-art solutions for the verification of both feed-forward and recurrent neural networks.

We extended the techniques above to account for LE-CPSs operating in an environment. The resulting models are amenable to formal verification and we proposed several techniques to verify them against specifications expressed in rich logics such as LTL, CTL or ATL.

More details on our current research can be found in the Software and Publications sections below.

Software

The following tools have been developed within the project:

• VENUS (VErification of NeUral Systems), a state-of-the-art sound and complete verification toolkit for ReLU-based feed-forward neural networks. It can be used to check reachability and local adversarial robustness properties. VENUS implements a MILP-based verification method and leverages dependency relations between the ReLU nodes to prune the search tree that needs to be considered during branch-and-bound. It additionally implements methods based on symbolic interval propagation and input domain splitting. [paper] [download]

Publications

Team members

Principal investigator

• Prof. Alessio Lomuscio

Research associates

• Dr. Elena Botoeva
• Dr. Panagiotis Kouvaros
• Dr. Francesco Leofante
• Dr. Jianglin Lan

Collaborators

• Mr Patrick Henriksen
• Ms Yi-Ling Liu
• Dr. Yang Zheng

Previous collaborators

• Dr. Michael Akintunde
• Dr. Edoardo Pirovano

  Funding

This research is funded by DARPA under the Assured Autonomy program.