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