又一位清華校友獲得ACM 博士論文獎

[[411517]]

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

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

2020 年 ACM 最佳博士論文獎

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

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

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

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

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

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

個人主頁：http://chuchu.mit.edu/

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

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

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

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

2020 ACM 博士論文榮譽提名獎

2020 年 ACM 博士論文獎的榮譽提名授予了 Henry Corrigan-Gibbs 和 Ralf Jung。

Corrigan-Gibbs 獲得提名的博士論文為《Protecting Privacy by Splitting Trust》，這項研究借助理論與實踐相結(jié)合的技術(shù)改善了互聯(lián)網(wǎng)用戶隱私問題。他提出了一種新型的概率可驗證明 (PCP)系統(tǒng)，然后應(yīng)用這種技術(shù)開發(fā)了可擴展、滿足實際行業(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)用戶的任何其他信息的情況下，有效計算有關(guān)用戶群的聚合統(tǒng)計數(shù)據(jù)。例如，該論文介紹了一種工具，使 Mozilla 能夠測量有多少火狐用戶遇到了某種網(wǎng)絡(luò)跟蹤器，而無需了解是哪些用戶遇到了該跟蹤器或遇到的原因。這項研究開發(fā)了一種新的概率可驗證明系統(tǒng)，該系統(tǒng)允許每個瀏覽器發(fā)送一個簡短的零知識證明，證明其對聚合統(tǒng)計數(shù)據(jù)的加密貢獻(xiàn)格式正確。論文的關(guān)鍵創(chuàng)新是驗證證明的速度非常快。

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

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

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

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

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

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

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

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

機器之心先前也報道過 2018 年、2019 年的博士論文獎。

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

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