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