Applied Mathematics Seminar——基于抽象解释的神经网络验证

摘要:
随着神经网络在安全攸关场景中的应用越来越多，验证其安全性与鲁棒性变得日益重要。抽象解释是一种对用于形式描述复杂系统行为的数学结构进行抽象和近似并推导或验证其性质的理论。报告将介绍抽象解释在神经网络验证中的应用，并重点介绍一种基于迭代抽象分析的神经网络安全性和鲁棒性完备验证方法。其主要思想是，以一种按需的方式，将原验证问题分解成若干个子验证问题；整体框架采用迭代精化的方式开展验证，而具体每个子验证问题则采用基于抽象解释的分析来进行检验。

个人简介：
陈立前，国防科技大学计算机学院副教授，主要从事程序分析验证与修复、抽象解释相关研究。在ACM/IEEE Transactions、POPL、FSE、ASE等期刊会议上发表论文70余篇，曾获ACM SIGSOFT杰出论文奖，出版教材译著3部。研究成果获省部级科技进步一等奖1项、二等奖1项。部分成果已在航天、国防等领域重大工程中应用。