CAREER: Provable Patching of Deep Neural Networks

职业：可证明的深度神经网络修补

• 批准号: 2048123
• 负责人: Aditya Thakur
• 金额: $ 50万
• 依托单位: University of California-Davis
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2021
• 资助国家: 美国
• 起止时间: 2021-07-01 至 2026-12-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2048123&HistoricalAwards=false
• 关键词: CAREER; Provable; Patching; Deep; Neural

Deep neural networks (DNNs) have been successfully applied to a wide variety of problems, including image recognition, natural-language processing, medical diagnosis, and self-driving cars. As the accuracy of DNNs has increased so has their complexity and size. Moreover, DNNs are far from infallible, and mistakes made by DNNs have led to loss of life, motivating research on verification and testing to find mistakes in DNNs. In contrast, the central goal of this research is to develop techniques and tools for repairing a trained DNN once a mistake has been discovered. Provable Patching of DNNs computes a minimal change (patch) to the parameters of a trained DNN to correct its behavior according to a given specification. The project is interdisciplinary, combining the areas of Formal Methods and Machine Learning. The project develops theoretical foundations, designs efficient algorithms, and evaluates practical applications of Provable Patching of DNNs. The intellectual merits are (i) ensuring that the patching techniques are provably effective, generalizing, local, and efficient, and (ii) supporting different classes of safety and fairness specifications. The broader impacts of the project include (i) developing new undergraduate and graduate courses related to program correctness and formal methods, and (ii) broadening the participation of Computer Science undergraduate students by developing education and research activities targeting community college and transfer students.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.

深度神经网络（DNN）已成功应用于各种问题，包括图像识别、自然语言处理、医疗诊断和自动驾驶汽车。随着DNN的准确性增加，其复杂性和大小也增加了。此外，DNN远非万无一失，DNN所犯的错误导致了生命的损失，激发了对验证和测试的研究，以发现DNN中的错误。相比之下，这项研究的中心目标是开发技术和工具，以便在发现错误后修复经过训练的DNN。DNN的可证明修补计算训练DNN的参数的最小变化（补丁），以根据给定的规范纠正其行为。该项目是跨学科的，结合了形式方法和机器学习领域。该项目开发了理论基础，设计了有效的算法，并评估了DNN的可证明修补的实际应用。智能优点是（i）确保修补技术是可证明有效的，通用的，本地的，和高效的，（ii）支持不同类别的安全性和公平性规范。该项目更广泛的影响包括：（i）开发与程序正确性和形式方法相关的新的本科生和研究生课程，以及（ii）通过发展针对社区学院和转学生的教育和研究活动，扩大计算机科学本科生的参与。该奖项反映了NSF的法定使命，并通过使用基金会的智力价值进行评估，被认为值得支持和更广泛的影响审查标准。

项目成果

SyReNN: A Tool for Analyzing Deep Neural Networks

• DOI: 10.1007/s10009-023-00695-1
• 发表时间: 2021-01
• 期刊: Tools and Algorithms for the Construction and Analysis of Systems
• 作者: Matthew Sotoudeh;Zhen-Zhong Tao;Aditya V. Thakur

Provable repair of deep neural networks

• DOI: 10.1145/3453483.3454064
• 发表时间: 2021-04
• 期刊: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
• 作者: Matthew Sotoudeh;Aditya V. Thakur

Architecture-Preserving Provable Repair of Deep Neural Networks

• DOI: 10.1145/3591238
• 发表时间: 2023-04
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Zhe Tao;Stephanie Nawas;Jacqueline Mitchell;Aditya V. Thakur