时间：2024年1月12日 上午10：00-11：00

地点：北二区大会议室

主讲人：宋富 中科院软件所研究员

主持人：王瑞 首都师范大学信息工程学院教授

主讲人简介：宋富，现任中国科学院软件研究所研究员。长期从事形式化验证理论、技术、工具与应用研究，在程序设计语言（POPL、OOPSLA）、形式化验证（CAV、FM、TACAS）、软件工程（ICSE、ESEC/FSE、ASE、ISSTA、ACM TOSEM、IEEE TSE）、网络空间安全（S&P、USENIX Security、NDSS、IEEE TDSC）等领域国际顶级/著名会议/期刊发表高质量论文80余篇（CCF-A/中科院一区论文40余篇），参与撰写CCF中国计算机科学技术发展报告3份、Springer 书1章。曾入选上海市浦江人才计划、上海市晨光学者。

主讲内容简介：神经网络量化技术将模型的浮点数权重转化到固定少量位数的表示，有效减少神经网络模型内存开销且提升运行效率，因为量化神经网络广泛应用于资源受限设备。在安全攸关领域，量化神经网络的鲁棒性需要进行形式验证，但是之前针对实数或浮点数的神经网络的形式验证技术不适用于量化神经网络，急需针对量化神经网络的鲁棒性形式验证技术方法。本报告将介绍我们在量化神经网络的鲁棒性形式验证的研究进展，包括基于二元决策图（BDD）的二值量化神经网络定量形式验证和整数线性规划的多值量化神经网络定性形式验证。