Configuring Safe Spiking Neural Controllers for Cyber-Physical Systems through Formal Verification

TL;DR

This paper presents a method to tune spiking neural network controllers for cyber-physical systems to ensure safety and accuracy using formal verification and MILP, reducing computational costs with data-driven techniques.

Contribution

It introduces a hyperparameter tuning approach for SNN controllers that guarantees safety compliance through formal verification, combining MILP modeling and data-driven optimization.

Findings

Successfully verified safety of SNN controllers on benchmarks.

Reduced verification calls via data-driven techniques.

Enhanced confidence in deploying energy-efficient SNNs in CPSs.

Abstract

Spiking Neural Networks (SNNs) are a subclass of neuromorphic models that have great potential to be used as controllers in Cyber-Physical Systems (CPSs) due to their energy efficiency. They can benefit from the prevalent approach of first training an Artificial Neural Network (ANN) and then translating to an SNN with subsequent hyperparameter tuning. The tuning is required to ensure that the resulting SNN is accurate with respect to the ANN in terms of metrics like Mean Squared Error (MSE). However, SNN controllers for safety-critical CPSs must also satisfy safety specifications, which are not guaranteed by the conversion approach. In this paper, we propose a solution which tunes the $temporal$ $window$ hyperparameter of the translated SNN to ensure both accuracy and compliance with the safe range specification that requires the SNN outputs to remain within a safe range. The core verification problem is modelled using mixed-integer linear programming (MILP) and is solved with Gurobi. When the controller fails to meet the range specification, we compute tight bounds on the SNN outputs as feedback for the CPS developer. To mitigate the high computational cost of verification, we integrate data-driven steps to minimize verification calls. Our approach provides designers with the confidence to safely integrate energy-efficient SNN controllers into modern CPSs. We demonstrate our approach with experimental results on five different benchmark neural controllers.