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.