Safe Control Systems with Neural Networks

We address the fundamental question of how to trust a neural network that controls a dynamical system. Since neural networks are large black boxes, we need both automatic methods to analyze such systems and human-interpretable certificates of the analysis results. We devise automatic and sound methods to respectively certify correctness and incorrectness of neural-network controllers.

Control systems are everywhere. For example, flood gates control the water level in rivers all over the country to ensure that we have a regular supply of water throughout the year, independent of weather and demand, while avoiding flooding. Much of this is controlled automatically by control software, traditionally designed by engineers with mathematical rigor and practical experience.

Artificial intelligence has made tremendous progress in data-driven approaches with so-called artificial neural networks. Machines are superior at predicting the water level from the vast amount of data that we have. However, neural networks are large black boxes that cannot be reasoned about like traditional software. It is thus unclear how we can trust this new generation of systems when employed in critical applications like water management.

In this project, we lay the grounds for reasoning about neural-network control systems. First, we need to certify that these systems work correctly. Second, if the system is not correct, we need to detect errors so we can fix them. Crucially, these procedures have to be automatic because it is not possible for humans to understand those black-box systems. Thus we aim to bridge the gap to traditional software where certification is the standard way to trust a system.