新智元報(bào)道

來(lái)源：ACM

編輯：Priscilla 好困

【新智元導(dǎo)讀】近日，ACM公布了2020年博士論文獎(jiǎng)得主，清華90后女學(xué)霸、UIUC博士、MIT助理教授范楚楚榮獲該獎(jiǎng)。

近日，ACM公布了2020年博士論文獎(jiǎng)，清華90后女學(xué)霸范楚楚憑借著題為「安全自主性的形式方法：數(shù)據(jù)驅(qū)動(dòng)的驗(yàn)證、綜合和應(yīng)用」的論文榮獲該獎(jiǎng)。

「ACM博士論文獎(jiǎng)」每年由ACM（美國(guó)計(jì)算機(jī)協(xié)會(huì)）頒發(fā)，用來(lái)表彰計(jì)算機(jī)科學(xué)和計(jì)算機(jī)工程領(lǐng)域最佳博士論文的作者，同時(shí)獲獎(jiǎng)?wù)邔⒌玫?/span>2萬(wàn)美元的獎(jiǎng)金。

ACM表示，范楚楚的論文在嵌入式和網(wǎng)絡(luò)物理系統(tǒng)的驗(yàn)證有著極為重要的貢獻(xiàn)，論文提出的驗(yàn)證技術(shù)已經(jīng)可以適用于工業(yè)規(guī)模的系統(tǒng)。

論文推進(jìn)了敏感性分析（sensitivity analysis）和符號(hào)化可達(dá)性（symbolic reachability）的理論，并開(kāi)發(fā)了相關(guān)的驗(yàn)證算法和軟件工具（DryVR，Realsyn）。

同時(shí)，論文還為不完整模型（incomplete models）的「黑盒子」系統(tǒng)開(kāi)發(fā)了第一個(gè)驗(yàn)證算法，該算法結(jié)合了概率近似正確（probably approximately correct, PAC）學(xué)習(xí)與模擬關(guān)系（simulation relations）和不動(dòng)點(diǎn)分析（fixed point analyses）。

其中，DryVR已被應(yīng)用于包括高級(jí)駕駛輔助系統(tǒng)、基于神經(jīng)網(wǎng)絡(luò)的控制器、分布式機(jī)器人和醫(yī)療設(shè)備等幾十個(gè)系統(tǒng)之中。而Realsyn則要優(yōu)于現(xiàn)有其他方法。

90后學(xué)霸

ACM博士論文獎(jiǎng)得主范楚楚

本次杰出博士論文獎(jiǎng)獲得者范楚楚是一名90后學(xué)霸，清華大學(xué)自動(dòng)化系本科2013屆畢業(yè)生。

之后到美國(guó)伊利諾伊大學(xué)香檳分校（UIUC），成為電氣與計(jì)算機(jī)工程系的六年碩博連讀研究生。

2020年秋季加入麻省理工學(xué)院航天航空工程系擔(dān)任助理教授，所在團(tuán)隊(duì)使用嚴(yán)格的數(shù)學(xué)方法，包括形式化方法、機(jī)器學(xué)習(xí)和控制理論，以設(shè)計(jì)、分析和驗(yàn)證安全自主系統(tǒng)。

從高中開(kāi)始，范楚楚學(xué)霸身份就已經(jīng)「暴露無(wú)遺」，曾參加全國(guó)物理競(jìng)賽和數(shù)學(xué)競(jìng)賽并獲獎(jiǎng)。

而在清華求學(xué)期間，也曾獲三星獎(jiǎng)學(xué)金、清華大學(xué)優(yōu)良畢業(yè)生稱號(hào)、全國(guó)電子設(shè)計(jì)競(jìng)賽三等獎(jiǎng)、清華大學(xué)挑戰(zhàn)杯等榮譽(yù)。

在UIUC攻讀博士學(xué)位時(shí)，師從電氣和計(jì)算機(jī)工程系教授Sayan Mitra，主要研究安全自主技術(shù)（如自動(dòng)駕駛汽車(chē)、航天器和無(wú)人機(jī)）、控制理論、機(jī)器學(xué)習(xí)、機(jī)器人技術(shù)等。

讀博期間更是發(fā)表了近20篇期刊論文和會(huì)議論文。

而本次獲獎(jiǎng)?wù)撐闹刑岬降尿?yàn)證算法和軟件工具C2E2、DryVR、Realsyn也是由范楚楚開(kāi)發(fā)的。

范楚楚的學(xué)術(shù)成果喜人，也因此獲得了UIUC的博士生眾多獎(jiǎng)項(xiàng)，2018年還獲得了國(guó)家頒發(fā)給優(yōu)秀自費(fèi)留學(xué)生的獎(jiǎng)學(xué)金。

結(jié)合范楚楚一直以來(lái)的學(xué)術(shù)背景與學(xué)術(shù)成果，這次能夠獲得UIUC 2020年度最佳博士論文獎(jiǎng)也是意料之內(nèi)。

榮譽(yù)獎(jiǎng)得主

ACM除了公布2020年度杰出博士論文獎(jiǎng)得主外，還公布了博士論文榮譽(yù)獎(jiǎng)，獲獎(jiǎng)?wù)叻謩e是Henry Corrigan-Gibbs和Ralf Jung，兩人均可獲得1萬(wàn)美元的獎(jiǎng)金。

ACM博士論文榮譽(yù)獎(jiǎng)得主：Henry Corrigan-Gibbs

Henry Corrigan-Gibbs是計(jì)算機(jī)科學(xué)和人工智能實(shí)驗(yàn)室的成員，也是MIT電氣工程和計(jì)算機(jī)科學(xué)系的助理教授，獲得斯坦福大學(xué)計(jì)算機(jī)科學(xué)博士學(xué)位。

研究重點(diǎn)是計(jì)算機(jī)安全、密碼學(xué)和計(jì)算機(jī)系統(tǒng)。

獲獎(jiǎng)?wù)撐念}為：通過(guò)拆分信任以保護(hù)隱私（Protecting Privacy by Splitting Trust）。

論文鏈接：https://people.csail.mit.edu/henrycg/files/academic/papers/dissertation.pdf

作者研究了如何在不了解用戶的任何其他信息的情況下穩(wěn)健地計(jì)算有關(guān)用戶群的匯總統(tǒng)計(jì)數(shù)據(jù)。

該論文開(kāi)發(fā)了一種新的概率可檢查證明系統(tǒng)，該系統(tǒng)允許每個(gè)瀏覽器發(fā)送一個(gè)簡(jiǎn)短的零知識(shí)證明，證明其對(duì)聚合統(tǒng)計(jì)數(shù)據(jù)的加密貢獻(xiàn)格式正確。同時(shí)還具有極快的證明速度。

ACM博士論文榮譽(yù)獎(jiǎng)得主：Ralf Jung

Jung是馬克思·普朗克軟件系統(tǒng)研究所的博士后研究員，也是MIT并行和分布式操作系統(tǒng)組的研究員，獲得薩爾大學(xué)計(jì)算機(jī)科學(xué)專業(yè)的學(xué)、碩、博學(xué)位。

研究領(lǐng)域包括編程語(yǔ)言、驗(yàn)證、語(yǔ)義和類型系統(tǒng)。

獲獎(jiǎng)?wù)撐念}為：理解和發(fā)展Rust編程語(yǔ)言（Understanding and Evolving the Rust Programming Language）。

論文鏈接：https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf

作者通過(guò)為Rust開(kāi)發(fā)直接解釋安全和不安全代碼之間相互作用的語(yǔ)義基礎(chǔ)，解決了缺少對(duì)Rust安全聲明是否真正成立的嚴(yán)格調(diào)查的問(wèn)題，為Rust的一個(gè)重要子集提供了安全性證明。

此外，論文還提供了一個(gè)平臺(tái)，即使存在不安全的代碼，也能用于正式驗(yàn)證基于類型的優(yōu)化。

獲獎(jiǎng)?wù)撐?br>

這篇論文是范楚楚2019年在完成伊利諾伊大學(xué)香檳分校電氣和計(jì)算機(jī)工程專業(yè)博士學(xué)位時(shí)提交的論文。

論文鏈接：https://www.ideals.illinois.edu/bitstream/handle/2142/106202/FAN-DISSERTATION-2019.pdf

在現(xiàn)實(shí)世界中，自主系統(tǒng)的典型模型的驗(yàn)證和合成在理論上是不可知的，由于其高維度、非線性、非確定性和混合性，近似的解決方案也十分具有挑戰(zhàn)性。

為了應(yīng)對(duì)這些挑戰(zhàn)，論文提出了：

通過(guò)非線性混合系統(tǒng)的可達(dá)性分析進(jìn)行數(shù)據(jù)驅(qū)動(dòng)的算法驗(yàn)證；
干擾下的高維線性系統(tǒng)的控制器合成。

在理論方面，論文提出的技術(shù)具有穩(wěn)定性、精確性和相對(duì)完整性的保證。

在實(shí)驗(yàn)方面，論文提出的技術(shù)可以成功地應(yīng)用于一系列具有挑戰(zhàn)性的問(wèn)題，包括首次驗(yàn)證的發(fā)動(dòng)機(jī)控制模型、衛(wèi)星控制系統(tǒng)、自動(dòng)駕駛和基于高級(jí)輔助駕駛系統(tǒng)（ADAS）的操作。

論文貢獻(xiàn)

1. 通過(guò)對(duì)非線性混合系統(tǒng)和非線性過(guò)渡系統(tǒng)的可達(dá)性分析，開(kāi)發(fā)了一種數(shù)據(jù)驅(qū)動(dòng)的安全驗(yàn)證算法，從而推進(jìn)了網(wǎng)絡(luò)物理系統(tǒng)（cyber-physical systems, CPS）的驗(yàn)證。

數(shù)據(jù)驅(qū)動(dòng)算法在非線性系統(tǒng)的數(shù)據(jù)使用方面可以實(shí)現(xiàn)局部最優(yōu)，并且成倍地減少了非線性過(guò)渡系統(tǒng)所需搜索的次數(shù)。從而能夠驗(yàn)證難以解決的大型模型。

2. 提出了第一個(gè)用于驗(yàn)證現(xiàn)實(shí)世界中沒(méi)有精確數(shù)學(xué)模型的網(wǎng)絡(luò)物理系統(tǒng)框架。其關(guān)鍵是將這些系統(tǒng)視為帶有「黑盒」模擬器的「白盒」自動(dòng)機(jī)。。

因此，驗(yàn)證方法可以將自動(dòng)機(jī)上的最壞情況的推理與黑盒上的概率推理結(jié)合起來(lái)。

3. 提出了一種極大地提高有干擾的大型線性系統(tǒng)的控制合成效率的算法。該算法通過(guò)無(wú)需量化的線性計(jì)算簡(jiǎn)化合成問(wèn)題，并利用SMT求解器，實(shí)現(xiàn)了可擴(kuò)展性。

此外，作者還開(kāi)發(fā)了相關(guān)的軟件工具：C2E2（混合系統(tǒng)的驗(yàn)證）、DryVR（黑盒組件的系統(tǒng)驗(yàn)證）和RealSyn（用于整體）。

其中，C2E2是第一個(gè)成功驗(yàn)證豐田動(dòng)力總成控制系統(tǒng)和航天器會(huì)合問(wèn)題的工具；也是目前唯一能夠處理混合信號(hào)電路等高度非線性模型的工具。

參考資料：

https://awards.acm.org/about/2020-doctoral-dissertation

-往期精彩-

90后清華女校友范楚楚獲ACM 2020唯一博士論文獎(jiǎng)！出任MIT助理教授后再摘桂冠