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

arXiv: https://arxiv.org/abs/2509.03948 · HTML: https://mlsanity.com/paper/2509.03948/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 3 of its 13 references that are in the map.
- First posted on arXiv 4 Sep 2025.

## Builds on (most cited first, 3 of 3)

- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Neural Network Verification with Branch-and-Bound for General Nonlinearities](https://mlsanity.com/paper/2405.21063/) (2024)
- [Neural Network Verification with PyRAT](https://mlsanity.com/paper/2410.23903/) (2024)

## Abstract (arXiv)

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.