Formal Verification of Local Robustness of a Classification Algorithm for a Spatial Use Case

TL;DR

The paper tackles the reliability of an on-board hybrid AI system for satellite RWA anomaly detection by formalizing local robustness of the neural classifiers used for anomalies C and D. It combines a physics-informed data-processing pipeline with small neural networks and demonstrates high classification performance, while developing a envelope-based verification workflow using Marabou to certify local robustness under time-series perturbations. The key contributions include a practical methodology to bound the data-processing outputs and verify neural components, empirical robustness profiling across perturbations, and initial steps toward global robustness constraints to define safe operating regions. This work advances trust and verifiability of AI-enabled fault-detection in space, offering a path toward end-to-end robustness assurances within complex, proprietary pipelines.

Abstract

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.

Figures (15)

• Figure 1: Time series of a RWA spin rate and friction torque
• Figure 2: Histograms used to classify anomalies C and D
• Figure 3: Data processing pipeline.
• Figure 4: Classification algorithm overview.
• Figure 5: Example of time series and effect of some perturbations