用形式化验证提升卫星故障检测模型的抗干扰能力
Formal Verification of Local Robustness of a Classification Algorithm for a Spatial Use Case
- 用Marabou工具验证神经网络在局部输入扰动下的稳定性
- 量化输入可容忍的最大扰动范围以评估模型可靠性
- 适合关注航天级AI系统可信性验证的研究者
卫星部件故障代价高昂且难以处理，常需大量人力物力。在卫星上嵌入基于混合AI的故障检测系统可提前发现问题，显著减轻负担。但此类系统必须具备极高的可靠性。为确保这种可靠性，我们采用形式化验证工具Marabou，验证用于AI算法的神经网络模型的局部鲁棒性。该工具可量化模型输入在多大程度上被扰动时输出行为仍保持稳定，从而增强对模型在不确定性下的性能信任度。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。