CAREER: Proof Sharing and Transfer for Boosting Neural Network Verification

职业：促进神经网络验证的证明共享和转移

• 批准号: 2238079
• 负责人: Gagandeep Singh
• 金额: $ 50万
• 依托单位: University of Illinois at Urbana-Champaign
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-02-01 至 2028-01-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2238079&HistoricalAwards=false
• 关键词: CAREER; Proof; Sharing; Transfer; Boosting

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.

尽管在各种具有挑战性的现实世界任务中表现出色，但仍然对最先进的深神经网络（DNNS）的可信赖性仍然存在。适用于现实世界部署的DNN的开发需要正式证明它们满足了大量值得信赖的规格（例如，鲁棒性，安全性，公平性）。如果他们没有，那么DNN将进行迭代修复或重新训练，直到正式证明是值得信赖的。总体而言，值得信赖的DNN开发要求将DNN验证者用于不同的规格和DNN。每次呼吁DNN验证者的计算要求都在计算上要求，尽管在提高最新验证器的精确和可扩展性方面，近年来验证单个DNN和规格的精确性和可伸缩性，但现有的验证符基本上是不可接受的，并且是无法可持续的，并且是可信赖的DNNS的可信赖发展。这是因为每对新的规格和DNN都需要从头开始运行昂贵的验证者。该项目的新颖性是通过设计新概念，理论，算法和表示的设计来克服这一障碍，以实现DNNS的增量验证。该项目的影响使DNN验证更加可扩展，可持续和访问。这允许可信赖的DNN的可扩展发展，从而确保该技术实现了它在改变社会和经济方面的真正潜力。 该项目介绍了证明共享和证明转移的新概念，以实现增量DNN验证。通过计算多个规格的共同证明，证明共享可以使对同一DNN上的多个规格进行验证。通过将一个网络上生成的证明用于多个类似网络，证明传输可以提高多个网络的验证。通过设计用于DNN培训和维修的新机制，可以进一步提高精度，速度和记忆收益。该项目设计的递增DNN验证的框架和工具与DNN培训，维修和验证的各种方法兼容。该奖项反映了NSF的法定任务，并被认为是通过基金会的知识分子优点和更广泛影响的审查标准来通过评估来获得支持的。