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