尊龙凯时

时间：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）的二值量化神經網絡定量形式驗證和整數線性規劃的多值量化神經網絡定性形式驗證
。