CAREER: Proof Sharing and Transfer for Boosting Neural Network Verification

尽管它们在各种具有挑战性的现实任务中表现令人印象深刻，但人们仍然担心最先进的深度神经网络（DNN）的可信度。开发适合于现实世界部署的DNN需要正式证明它们满足大量值得信赖的规范（例如，鲁棒性、安全性、公平性）。如果它们没有，那么DNN会被反复修复或重新训练，直到它们被正式证明是值得信赖的。总的来说，可信的DNN开发需要针对不同的规范和DNN多次调用DNN验证器。对DNN验证器的每次调用都需要计算，虽然近年来在提高用于验证单个DNN和规范的最先进验证器的精度和可扩展性方面做了大量工作，但现有的验证器对于DNN的可靠开发来说仍然是不可扩展和不可持续的。这是因为对于每一对新的规范和DNN，都需要从头开始运行昂贵的验证器。该项目的创新之处在于通过设计新的概念、理论、算法和表示来克服这一障碍，以实现DNN的增量验证。该项目的影响使DNN验证更具可扩展性，可持续性和可访问性。这使得可信赖的DNN的可扩展开发成为可能，从而确保该技术实现其在改变社会和经济方面的真正潜力。 该项目引入了证据共享和证据传输的新概念，以实现增量DNN验证。证明共享通过计算多个规范的公共证明，使同一DNN上的多个规范的验证更具可扩展性和精确性。证明传输通过将在一个网络上生成的证明传输给多个类似的网络来增强跨多个网络的验证。通过设计DNN训练和修复的新机制，增量验证的精度、速度和内存增益得到了进一步提高。该项目中设计的增量DNN验证框架和工具是通用的，并与DNN培训，修复和验证的各种方法兼容。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.