Practical Formal Verification of Industrial Neural Networks in Aerospace
ABSTRACT Recent advances in artificial intelligence (AI) and machine learning (ML) have sparked growing interest in deploying these technologies within aerospace systems. However, airborne systems incorporating AI/ML components must comply with stringent certification requirements. The novelty of ML technologies poses significant challenges, as existing certification standards are often insufficient or inapplicable. In response, certification authorities have released guidance addressing the qualification, assurance, and certification of ML-enabled systems, with formal methods, particularly formal verification, emerging as a promising means of compliance. In this talk, we examine the application of formal verification to neural network models in the aerospace domain, highlighting key challenges and proposing practical solutions. A central challenge lies in accurately characterizing the operational design domain (ODD), as counterexamples generated outside the ODD are not meaningful for certification. Common practice approximates the ODD as the Cartesian product of input value ranges observed in training data, implicitly assuming input independence. However, aerospace inputs, such as sensor measurements of physical environments, often exhibit strong correlations, making this approximation overly conservative. To address this issue, we propose a convex hull–based approximation of the ODD, which can be natively supported by state-of-the-art neural network verification tools. We demonstrate the effectiveness of this approach through case studies involving industrial-scale aerospace neural networks. Finally, we discuss formal properties of interest in aerospace applications and provide an assessment of the strengths, limitations, and performance of current formal verification tools when applied to real-world models. |
BIO Dr. Cong Liu serves as a Principal Engineer within the Applied Research and Technology organization at Collins Aerospace. Dr. Liu is a PI for the DARPA Assured Neuro Symbolic Learning and Reasoning (ANSR) program, where he leads the Collins-UT Austin team investigating a neuro-symbolic approach to LLM fine-tuning. He is also a Co-Investigator for the NASA ULI TRANSCEND project: Trustworthy Resilient Autonomous Agents for Safe City Transportation in the Evolving New Decade. Dr. Liu’s primary area of expertise lies in the design automation of cyber-physical systems, particularly through the application of formal methods. Dr. Liu has made significant contributions to several high-profile programs, including the DARPA Cyber Assured Systems Engineering (CASE) program and the DARPA Architecture and Analysis for High-Assurance Autonomy (AAHAA) program. Dr. Liu earned his Ph.D. in Electrical Engineering and Computer Sciences from the University of California, Berkeley. |