Formal Verification of Local Robustness of a Classification Algorithm for a Spatial Use Case
This addresses the costly and resource-intensive issue of satellite component failures by enabling earlier and more dependable fault detection, though it is incremental as it applies an existing verification method to a specific domain.
The paper tackled the problem of ensuring high reliability for AI-based fault detection in satellites by using the formal verification tool Marabou to verify the local robustness of neural network models, quantifying input perturbations before output instability.
Failures in satellite components are costly and challenging to address, often requiring significant human and material resources. Embedding a hybrid AI-based system for fault detection directly in the satellite can greatly reduce this burden by allowing earlier detection. However, such systems must operate with extremely high reliability. To ensure this level of dependability, we employ the formal verification tool Marabou to verify the local robustness of the neural network models used in the AI-based algorithm. This tool allows us to quantify how much a model's input can be perturbed before its output behavior becomes unstable, thereby improving trustworthiness with respect to its performance under uncertainty.