Certified Neural Networks: from Verification to Synthesis

Neural networks find applications in many safety-critical systems that raise concerns about their deployment: Are we sure they never advise doing anything catastrophic? Formal verification has been recently applied to prove whether an existing neural network is certified for some property; i.e., if it satisfies the property for all possible inputs or not. Formal verification can prove that a network satisfies a property but cannot fix the network in case it doesn’t. In this paper we focus on the automated synthesis of certified neural networks, that is, on how to automatically build a network that is guaranteed to respect some required properties expressed as logical constraints. We exploit a Counter Example Guided Inductive Synthesis (CEGIS) loop that alternates Deep Learning, Formal Verification, and a novel data generation technique that augments the training data to synthesize certified networks in a fully automated way. We identify a few conditions guaranteeing termination of the approach. We also investigate a soft constraint acceleration technique to reduce the number of CEGIS iterations and we test our approach to synthesize safety neural controllers for four case studies: a social robot application scenario, an expense prediction scenario, and two versions of the Airborne Collision Avoidance System X for unmanned aircraft benchmark (HCAS and ACASXu).