圖片來源：視覺中國

近日，ACM公布了2020年博士論文獎得主，清華90后女學霸、UIUC博士、MIT助理教授范楚楚榮獲該獎。

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

「ACM博士論文獎」每年由ACM（美國計算機協(xié)會）頒發(fā)，用來表彰計算機科學和計算機工程領(lǐng)域最佳博士論文的作者，同時獲獎者將得到2萬美元的獎金。

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

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

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

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

90后學霸

ACM博士論文獎得主范楚楚

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

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

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

從高中開始，范楚楚學霸身份就已經(jīng)「暴露無遺」，曾參加全國物理競賽和數(shù)學競賽并獲獎。

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

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

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

而本次獲獎論文中提到的驗證算法和軟件工具C2E2、DryVR、Realsyn也是由范楚楚開發(fā)的。

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

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

榮譽獎得主

ACM除了公布2020年度杰出博士論文獎得主外，還公布了博士論文榮譽獎，獲獎者分別是Henry Corrigan-Gibbs和Ralf Jung，兩人均可獲得1萬美元的獎金。

ACM博士論文榮譽獎得主：Henry Corrigan-Gibbs

Henry Corrigan-Gibbs是計算機科學和人工智能實驗室的成員，也是MIT電氣工程和計算機科學系的助理教授，獲得斯坦福大學計算機科學博士學位。

研究重點是計算機安全、密碼學和計算機系統(tǒng)。

獲獎論文題為：通過拆分信任以保護隱私（Protecting Privacy by Splitting Trust）。

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

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

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

ACM博士論文榮譽獎得主：Ralf Jung

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

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

獲獎論文題為：理解和發(fā)展Rust編程語言（Understanding and Evolving the Rust Programming Language）。

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

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

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

獲獎論文

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

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

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

為了應對這些挑戰(zhàn)，論文提出了：

• 通過非線性混合系統(tǒng)的可達性分析進行數(shù)據(jù)驅(qū)動的算法驗證；

• 干擾下的高維線性系統(tǒng)的控制器合成。

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

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

論文貢獻

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

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

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

因此，驗證方法可以將自動機上的最壞情況的推理與黑盒上的概率推理結(jié)合起來。

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

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

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

參考資料：

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

本文轉(zhuǎn)載自微信公眾號“新智元“（ID：AI_era），來源：ACM，編輯：Priscilla、好困。文章原標題：《90后清華女校友范楚楚獲ACM 2020唯一博士論文獎！出任MIT助理教授后再摘桂冠》。文章為作者獨立觀點，不代表芥末堆立場，轉(zhuǎn)載請聯(lián)系原作者。