CAREER: Provable Patching of Deep Neural Networks

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

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.