CAREER: NeuralSAT: A Constraint-Solving Framework for Verifying Deep Neural Networks

职业：NeuralSAT：用于验证深度神经网络的约束求解框架

• 批准号: 2238133
• 负责人: ThanhVu Nguyen
• 金额: $ 51.05万
• 依托单位: George Mason University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-07-01 至 2028-06-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2238133&HistoricalAwards=false
• 关键词: CAREER; NeuralSAT; Constraint; Solving; Framework

Deep Neural Networks (DNNs) have emerged as an effective approach to tackling real-world problems. However, just like traditional software, DNNs can have "bugs" and be attacked. This naturally raises the question of how DNNs should be tested, validated, and ultimately verified to meet the requirements of relevant robustness and safety standards. To address this question, researchers have developed powerful formal methods and tools to verify DNNs. However, despite many recent advances, existing approaches and tools still have challenges in achieving good precision and scalability. Moreover, they could produce unsound results and do not apply to DNNs such as Graph Neural Networks (GNNs). This project aims to address these challenges. The project's novelties are the integration of learning and abstraction ability in modern constraint solvers for accurate and scalable DNN verification, stress-testing DNN verifiers and certifying their results, and tackling GNNs through the lenses of other DNN approaches. The project's impacts are the development of new theories, advanced methods, and practical tools to ensure the accuracy and quality of DNN systems.The project has four technical research components. The first component develops NeuralSAT, a constraint-solver for DNNs that combines the conflict-driven clause learning ability of modern SAT solving and abstraction-based theory solver in SMT solving. The second component makes NeuralSAT more precise and efficient at scale by developing non-convex abstractions and leveraging heuristics and optimizations in modern SAT solvers. The third component uses clause learning and metamorphic testing to help developers find bugs in their DNN verifiers during production and certify their results during deployment. The fourth component explores GNNs, a powerful model in deep learning but with few existing formal techniques and tools by reducing GNN to Feed-forward Neural Network (FNN), which allows for the applications of FNN analyzers to GNNs. The project will benefit society by improving the reliability of systems embedding DNNs. The research contributes to ML by developing effective techniques to verify DNNs, allowing AI/ML researchers and users to improve their DNNs and deploy them with confidence. The research is supporting graduate and undergraduate student researchers and outreach activities for K-12 students in Prince William county of Northern Virginia.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可能会有“bug”并受到攻击。这自然会提出一个问题，即DNN应该如何进行测试、验证和最终验证，以满足相关鲁棒性和安全标准的要求。为了解决这个问题，研究人员开发了强大的正式方法和工具来验证DNN。 然而，尽管最近取得了许多进展，但现有的方法和工具在实现良好的精度和可扩展性方面仍然存在挑战。此外，它们可能会产生不合理的结果，并且不适用于DNN，如图神经网络（GNN）。该项目旨在应对这些挑战。该项目的创新之处在于将学习和抽象能力集成到现代约束求解器中，以实现准确和可扩展的DNN验证，对DNN验证器进行压力测试并验证其结果，并通过其他DNN方法的镜头来处理GNN。该项目的影响是开发新的理论，先进的方法和实用的工具，以确保DNN系统的准确性和质量。该项目有四个技术研究部分。第一个组件开发NeuralSAT，DNN的约束求解器，它结合了现代SAT求解的冲突驱动子句学习能力和SMT求解中基于抽象的理论求解器。 第二个组件通过开发非凸抽象和利用现代SAT求解器中的算法和优化，使NeuralSAT在规模上更加精确和高效。第三个组件使用子句学习和变形测试来帮助开发人员在生产过程中发现DNN验证器中的错误，并在部署过程中验证其结果。 第四部分探索了GNN，这是一种强大的深度学习模型，但通过将GNN简化为前馈神经网络（FNN），现有的正式技术和工具很少，这允许将FNN分析器应用于GNN。该项目将通过提高嵌入DNN的系统的可靠性来造福社会。 该研究通过开发有效的技术来验证DNN，从而为ML做出贡献，使AI/ML研究人员和用户能够改进他们的DNN并放心地部署它们。这项研究是支持研究生和本科生的研究人员和推广活动的K-12学生在威廉王子县的北方Virginia.This奖项反映了NSF的法定使命，并已被认为是值得通过评估使用基金会的智力价值和更广泛的影响审查标准的支持。