CAREER: Proof Sharing and Transfer for Boosting Neural Network Verification

Despite their impressive performance in a variety of challenging real-world tasks, concerns remain about the trustworthiness of state-of-the-art deep neural networks (DNNs). The development of DNNs suitable for real-world deployment requires formally proving that they satisfy a large number of trustworthy specifications (e.g., robustness, safety, fairness). If they do not, then the DNNs are iteratively repaired or re-trained until they are formally proven to be trustworthy. Overall, trustworthy DNN development requires calling a DNN verifier a large number of times for different specifications and DNNs. Each call to a DNN verifier is computationally demanding and while there has been plenty of work on improving the precision and scalability of state-of-the-art verifiers for verifying individual DNNs and specifications in recent years, the existing verifiers remain fundamentally non-scalable and unsustainable for trustworthy development of DNNs. This is because the expensive verifier needs to be run from scratch for every new pair of specifications and DNNs. The project novelties are in overcoming this barrier by the design of new concepts, theories, algorithms, and representations to enable incremental verification of DNNs. The project's impacts are making DNN verification more scalable, sustainable, and accessible. This allows scalable development of trustworthy DNNs thus ensuring that this technology realizes its true potential in transforming the society and economy. The project introduces the new concepts of proof sharing and proof transfer for enabling incremental DNN verification. Proof sharing makes the verification of multiple specifications on the same DNN more scalable and precise by computing a common proof for multiple specifications. Proof transfer boosts the verification across multiple networks by transferring the proofs generated on one network for multiple similar networks. Precision, speed, and memory gains from incremental verification are further improved by designing new mechanisms for DNN training and repair. The frameworks and tools for incremental DNN verification designed in this project are general, and compatible with diverse methods for DNN training, repair, and verification. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.