报告题目: 深度学习系统的可信性保障

时间：10月11日（周五） 16:30-17:30

地点：西海岸校区信息南楼A527会议室

报告摘要：深度学习系统已在诸多安全攸关领域中得到了广泛应用，与传统软件系统不同，深度学习系统数据驱动的特点使得该类系统拥有与传统系统完全不同的决策逻辑，并且深度学习系统的高维输入、庞大参数规模和状态空间使得其复杂程度远远超过传统的软件系统，从而使得目前应用于传统软件系统的形式化建模和验证技术难以直接应用于大规模深度学习系统的可信性、鲁棒性的保障之中。本次报告中将对相关问题以及我们近期关于深度神经网络的语义鲁棒性验证和估计的部分工作结果进行介绍。我们给出了语义扰动和局部鲁棒性的形式化定义，这一定义可以涵盖当前人们关心的大部分语义扰动类型，在此基础上，我们给出了一种基于统计的方法，用于验证神经网络对于一般语义扰动的局部鲁棒性。在CIFAR-10和ImageNet上的实验表明，与当前最先进的统计认证算法相比，我们的方法仅使用3.32%-6.55%的运行时间即可提供与之相同的理论保证。我们还从统计模型检验的角度给出了DNN局部鲁棒性和全局鲁棒性的估计算法，仅用少量图片即可获得与传统方法使用大量图片计算得到的全局鲁棒性值强相关的结果，并对主流统计模型检验工具中使用的Okamoto bound估计方法进行了改进，利用Clopper-Pearson置信区间设计了新的统计模型检验算法，可以直接替代现有模型检验工具中的Okamoto bound，比现有模型检验算法节省40%-60%的时间。

报告人简介：孙猛，北京大学数学科学学院信息与计算科学系副主任，教授，博士生导师， CCF形式化方法专委执行委员，CCF区块链专委执行委员，CSIAM区块链专委常务委员，CSIAM金融科技与算法专委常务委员，CAAI人工智能逻辑专委委员。主要研究领域包括程序理论、软件形式化方法、信息物理系统、可信人工智能、区块链与智能合约，主持及作为主要成员参与国家自然科学基金、重点研发计划等国家及省部级项目十余项，在IEEE TSE、ICSE、FSE、NeuIPS、AAAI、FM等期刊及会议发表论文百余篇，获TASE2015、SBMF2017等国际会议最佳论文奖，任FACS2009、TTSS2011、ICFEM2018、TASE2023、FACS2024、ICFEM2024等国际会议程序委员会主席，FM、TACAS、ICECCS等多个国际会议程序委员会委员。