564
0
0
2024-10-10 20:58:50
2025-06-04
時間：10月11日（周五） 16:30-17:30
地點：西海岸校區(qū)信息南樓A527會議室
報告摘要：深度學習系統(tǒng)已在諸多安全攸關領域中得到了廣泛應用，與傳統(tǒng)軟件系統(tǒng)不同，深度學習系統(tǒng)數(shù)據(jù)驅動的特點使得該類系統(tǒng)擁有與傳統(tǒng)系統(tǒng)完全不同的決策邏輯，并且深度學習系統(tǒng)的高維輸入、龐大參數(shù)規(guī)模和狀態(tài)空間使得其復雜程度遠遠超過傳統(tǒng)的軟件系統(tǒng)，從而使得目前應用于傳統(tǒng)軟件系統(tǒng)的形式化建模和驗證技術難以直接應用于大規(guī)模深度學習系統(tǒng)的可信性、魯棒性的保障之中。本次報告中將對相關問題以及我們近期關于深度神經網絡的語義魯棒性驗證和估計的部分工作結果進行介紹。我們給出了語義擾動和局部魯棒性的形式化定義，這一定義可以涵蓋當前人們關心的大部分語義擾動類型，在此基礎上，我們給出了一種基于統(tǒng)計的方法，用于驗證神經網絡對于一般語義擾動的局部魯棒性。在CIFAR-10和ImageNet上的實驗表明，與當前最先進的統(tǒng)計認證算法相比，我們的方法僅使用3.32%-6.55%的運行時間即可提供與之相同的理論保證。我們還從統(tǒng)計模型檢驗的角度給出了DNN局部魯棒性和全局魯棒性的估計算法，僅用少量圖片即可獲得與傳統(tǒng)方法使用大量圖片計算得到的全局魯棒性值強相關的結果，并對主流統(tǒng)計模型檢驗工具中使用的Okamoto bound估計方法進行了改進，利用Clopper-Pearson置信區(qū)間設計了新的統(tǒng)計模型檢驗算法，可以直接替代現(xiàn)有模型檢驗工具中的Okamoto bound，比現(xiàn)有模型檢驗算法節(jié)省40%-60%的時間。
報告人簡介：孫猛，北京大學數(shù)學科學學院信息與計算科學系副主任，教授，博士生導師， CCF形式化方法專委執(zhí)行委員，CCF區(qū)塊鏈專委執(zhí)行委員，CSIAM區(qū)塊鏈專委常務委員，CSIAM金融科技與算法專委常務委員，CAAI人工智能邏輯專委委員。主要研究領域包括程序理論、軟件形式化方法、信息物理系統(tǒng)、可信人工智能、區(qū)塊鏈與智能合約，主持及作為主要成員參與國家自然科學基金、重點研發(fā)計劃等國家及省部級項目十余項，在IEEE TSE、ICSE、FSE、NeuIPS、AAAI、FM等期刊及會議發(fā)表論文百余篇，獲TASE2015、SBMF2017等國際會議最佳論文獎，任FACS2009、TTSS2011、ICFEM2018、TASE2023、FACS2024、ICFEM2024等國際會議程序委員會主席，F(xiàn)M、TACAS、ICECCS等多個國際會議程序委員會委員。
