又一位清華校友獲得ACM 博士論文獎(jiǎng)

[[411517]]

一年一度的 ACM 博士論文獎(jiǎng)今日發(fā)布，來自 MIT 的助理教授范楚楚因?qū)η度胧胶途W(wǎng)絡(luò)物理系統(tǒng)的驗(yàn)證及其在工業(yè)規(guī)模自動(dòng)化系統(tǒng)中的應(yīng)用的貢獻(xiàn)而獲得了 ACM 的 2020 年博士論文獎(jiǎng)。榮譽(yù)提名獎(jiǎng)授予麻省理工學(xué)院的 Henry Corrigan-Gibbs 和馬克斯普朗克軟件系統(tǒng)研究所、麻省理工學(xué)院的 Ralf Jung。

該獎(jiǎng)項(xiàng)每年頒發(fā)一次，旨在獎(jiǎng)勵(lì)計(jì)算機(jī)科學(xué)和工程領(lǐng)域最優(yōu)秀的博士論文。今年的獲獎(jiǎng)?wù)邔⒃?10 月 23 日于舊金山舉行的典禮上獲頒獎(jiǎng)項(xiàng)。

2020 年 ACM 最佳博士論文獎(jiǎng)

范楚楚榮獲 2020 年 ACM 最佳博士論文獎(jiǎng)，她的獲獎(jiǎng)?wù)撐臑?2019 年從 UIUC 獲得博士學(xué)位的論文，論文題目《Formal Methods for Safe Autonomy: Data-Driven Verification, Synthesis, and Applications》。獲獎(jiǎng)理由：為嵌入式與信息物理系統(tǒng)的驗(yàn)證做出了奠基性貢獻(xiàn)，且展示了該技術(shù)應(yīng)用于工業(yè)系統(tǒng)的可能性。

論文地址：https://www.ideals.illinois.edu/handle/2142/106202

范楚楚的論文還推動(dòng)了靈敏度分析和符號(hào)可達(dá)性理論的發(fā)展；開發(fā)了一系列驗(yàn)證算法和軟件工具（DryVR, Realsyn）；展示了驗(yàn)證技術(shù)在工業(yè)規(guī)模自動(dòng)系統(tǒng)中的應(yīng)用。

本文提出的算法是第一個(gè)基于靈敏度分析的、可應(yīng)用于非線性混合系統(tǒng)有界驗(yàn)證的數(shù)據(jù)驅(qū)動(dòng)算法。這一工作在工業(yè)規(guī)模問題上的開創(chuàng)性示范表明，驗(yàn)證技術(shù)是可以規(guī)模化的。目前這項(xiàng)靈敏度分析已經(jīng)獲得了專利，并開始進(jìn)入商業(yè)化實(shí)踐。

范楚楚還開發(fā)了第一個(gè)用不完整模型來驗(yàn)證「黑盒子」系統(tǒng)的算法，該系統(tǒng)結(jié)合了概率近似正確（PAC）學(xué)習(xí)、模擬關(guān)系與定點(diǎn)分析。這項(xiàng)工作產(chǎn)生了一個(gè)工具 DryVR，已經(jīng)應(yīng)用于幾十種系統(tǒng)，包括先進(jìn)的駕駛輔助系統(tǒng)、基于神經(jīng)網(wǎng)絡(luò)的控制器、分布式機(jī)器人與醫(yī)療設(shè)備等。

另外，范楚楚提出的算法在非線性車輛模型系統(tǒng)的合成控制器中具有廣泛的應(yīng)用前景。本文提出的 RealSyn 方法優(yōu)于其他算法，為自動(dòng)駕駛汽車實(shí)時(shí)運(yùn)動(dòng)規(guī)劃算法鋪平了道路。

個(gè)人主頁(yè)：http://chuchu.mit.edu/

范楚楚現(xiàn)為 MIT 航空航天工程系的 Wilson 助理教授，也是可信賴自動(dòng)化系統(tǒng)實(shí)驗(yàn)室（Reliable Autonomous Systems Lab, REASL）的負(fù)責(zé)人。她的團(tuán)隊(duì)致力于使用形式化方法、機(jī)器學(xué)習(xí)和控制理論等來設(shè)計(jì)、分析和驗(yàn)證安全的自動(dòng)化系統(tǒng)。

2009 至 2013 年，她本科就讀于清華大學(xué)自動(dòng)化系，并被選為優(yōu)秀畢業(yè)生。本科畢業(yè)后前往伊利諾伊大學(xué)香檳分校（UIUC）攻讀博士學(xué)位，并于 2019 年順利拿到計(jì)算機(jī)工程博士學(xué)位。她的主要研究興趣在于安全自動(dòng)化系統(tǒng)、信息物理系統(tǒng)、形式化方法、控制理論、機(jī)器學(xué)習(xí)、強(qiáng)化學(xué)習(xí)和機(jī)器人技術(shù)等。

博士期間，她不僅發(fā)表了多篇期刊和會(huì)議論文，還榮獲了 UIUC CSL 學(xué)生論文獎(jiǎng)、UIUC Robert T. Chien 紀(jì)念獎(jiǎng)等多個(gè)獎(jiǎng)項(xiàng)。

博士畢業(yè)后，她又考取了加州理工學(xué)院的博士后研究員，并于 2020 年 8 月正式入職 MIT，擔(dān)任航空航天工程系的助理教授。

2020 ACM 博士論文榮譽(yù)提名獎(jiǎng)

2020 年 ACM 博士論文獎(jiǎng)的榮譽(yù)提名授予了 Henry Corrigan-Gibbs 和 Ralf Jung。

Corrigan-Gibbs 獲得提名的博士論文為《Protecting Privacy by Splitting Trust》，這項(xiàng)研究借助理論與實(shí)踐相結(jié)合的技術(shù)改善了互聯(lián)網(wǎng)用戶隱私問題。他提出了一種新型的概率可驗(yàn)證明 (PCP)系統(tǒng)，然后應(yīng)用這種技術(shù)開發(fā)了可擴(kuò)展、滿足實(shí)際行業(yè)需求的 Prio 系統(tǒng)。Prio 已經(jīng)部署在包括 Mozilla 在內(nèi)的幾家大公司中，自 2019 年底以來，它一直在夜間版本的 火狐瀏覽器中發(fā)揮作用，這是有史以來最大的 PCP 部署。

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

Corrigan-Gibbs 的論文研究了如何在不了解有關(guān)用戶的任何其他信息的情況下，有效計(jì)算有關(guān)用戶群的聚合統(tǒng)計(jì)數(shù)據(jù)。例如，該論文介紹了一種工具，使 Mozilla 能夠測(cè)量有多少火狐用戶遇到了某種網(wǎng)絡(luò)跟蹤器，而無(wú)需了解是哪些用戶遇到了該跟蹤器或遇到的原因。這項(xiàng)研究開發(fā)了一種新的概率可驗(yàn)證明系統(tǒng)，該系統(tǒng)允許每個(gè)瀏覽器發(fā)送一個(gè)簡(jiǎn)短的零知識(shí)證明，證明其對(duì)聚合統(tǒng)計(jì)數(shù)據(jù)的加密貢獻(xiàn)格式正確。論文的關(guān)鍵創(chuàng)新是驗(yàn)證證明的速度非?？?。

Corrigan-Gibbs 是 MIT 電氣工程和計(jì)算機(jī)科學(xué)系的助理教授，他也是計(jì)算機(jī)科學(xué)和人工智能實(shí)驗(yàn)室的成員。他的研究重點(diǎn)是計(jì)算機(jī)安全、密碼學(xué)和計(jì)算機(jī)系統(tǒng)。此前，Corrigan-Gibbs 在斯坦福大學(xué)獲得計(jì)算機(jī)科學(xué)博士學(xué)位。

Ralf Jung 的博士論文為《Understanding and Evolving the Rust Programming Language (https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf)》，該論文為 Rust 語(yǔ)言的安全系統(tǒng)編程奠定了第一個(gè)正式的基礎(chǔ)。

自從 2010 年 Mozilla 開發(fā) Rust 以來，它在整個(gè)行業(yè)中越來越受歡迎。Rust 解決了語(yǔ)言設(shè)計(jì)中一個(gè)長(zhǎng)期存在的問題：如何平衡安全性和控制。與 C++ 一樣，Rust 為程序員提供了對(duì)系統(tǒng)資源的低級(jí)控制。不同的是，Rust 采用了強(qiáng)大的 “基于所有權(quán)” 的系統(tǒng)來靜態(tài)確保安全，從而不會(huì)出現(xiàn)內(nèi)存訪問錯(cuò)誤、數(shù)據(jù)競(jìng)爭(zhēng)等安全漏洞。

然而，在 Jung 的論文之前，沒有嚴(yán)格調(diào)查表明 Rust 的安全聲明是否真的成立，并且由于 Rust 庫(kù)中廣泛使用“unsafe escape hatches”，這些聲明就很難評(píng)估。

https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf

在他的博士論文中，Jung 通過為 Rust 開發(fā)直接解釋安全和不安全代碼之間相互作用的語(yǔ)義基礎(chǔ)，來解決這一挑戰(zhàn)。在這些基礎(chǔ)上，Jung 為 Rust 的一個(gè)重要子集提供了安全性證明。此外，該證明在自動(dòng)證明助手 Coq 中被形式化，因此其正確性得到保證。此外，Jung 提供了一個(gè)平臺(tái)，即使存在不安全代碼的情況下也可用于正式驗(yàn)證基于類型的優(yōu)化。

通過 Jung 的領(lǐng)導(dǎo)和對(duì) Rust 不安全代碼指南工作組的積極參與，他的工作已經(jīng)對(duì) Rust 的設(shè)計(jì)產(chǎn)生了深遠(yuǎn)的影響，并為其未來奠定了重要的基礎(chǔ)。

Jung 是馬克斯普朗克軟件系統(tǒng)研究所的博士后研究員，也是 MIT 并行和分布式操作系統(tǒng)組的研究員。他的研究興趣包括編程語(yǔ)言、驗(yàn)證、語(yǔ)義和類型系統(tǒng)。他在馬克斯普朗克軟件系統(tǒng)研究所進(jìn)行了博士研究，并在薩爾大學(xué)獲得了計(jì)算機(jī)科學(xué)的博士、碩士和學(xué)士學(xué)位。

機(jī)器之心先前也報(bào)道過 2018 年、2019 年的博士論文獎(jiǎng)。

2018 年，UC 伯克利博士生 Chelsea Finn 憑借論文《Learning to Learn with Gradients》榮獲此獎(jiǎng)。來自微軟的 Ryan Beckett、本科畢業(yè)于清華姚班的馬騰宇獲得榮譽(yù)提名。

2019 年，畢業(yè)于特拉維夫大學(xué)的 Dor Minzer 獲得該獎(jiǎng)項(xiàng)，來自微軟的 Jakub Tarnawski 和出身清華姚班的吳佳俊獲得榮譽(yù)提名獎(jiǎng)。