尊龙凯时

时间：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）的二值量化神经网络定量形式验证和整数线性妄想的多值量化神经网络定性形式验证。