Deep Learning Meets Formal Methods: A Certified Neural Network Synthesis Approach for Airborne Collision Avoidance

Deep neural networks (DNNs) are being deployed in countless real-world applications, including safety-critical domains such as autonomous vehicles and collision avoidance systems in unmanned aircraft. Due to the unpredictability of the network in edge cases, the use of formal verification techniques has become a necessity to certify safety specifications. However, when the network is not certified for a certain property, it is also essential to have a method for adjusting its behavior. Hence, we focus on the synthesis of certified DNNs, that is, how to automatically build a neural network that is guaranteed to satisfy the required properties. We use a \textit{Counter-Example Guided Inductive Synthesis} (CEGIS) loop, alternating phases of training, formal verification, and training data generation from counterexamples, to synthesize certified networks without impacting their classification accuracy. Finally, we evaluate this approach on a DNN-based collision avoidance system, ACAS Xu, demonstrating the feasibility of this synthesis method in practical applications.