Supporting Formal Methods for Machine Learning Verification in Urban Air Mobility

The development of Urban Air Mobility (UAM) infrastructure has garnered significant attention in recent years. Specifically, researchers have explored using Machine Learning (ML) technology to improve the efficiency and scalability of the UAM ecosystem. However, incorporating ML into safety-critical applications requires increased Verification and Validation (V&V) efforts to ensure safety to human life, an endeavor that is heavily scrutinized but not yet solved in current research. This paper proposes utilizing formal methods to verify ML systems integrated within UAM as a mitigation to safety concerns. We present brief surveys on ML trends within UAM and formal methods trends within UAM. We then combine these disciplines to argue for the usage of formal methods for ML verification in UAM while discussing modern trends within formal verification of ML systems. By utilizing formal methods alongside traditional verification techniques to verify ML systems, the safety and reliability of UAM can be increased. Therefore, this paper calls for further research into formal verification of ML within UAM.