一年一度的 ACM 博士論文獎今日發布，來自 MIT 的助理教授範楚楚因對嵌入式和網絡物理系統的驗證及其在工業規模自動化系統中的應用的貢獻而獲得了 ACM 的 2020 年博士論文獎。榮譽提名獎授予麻省理工學院的 Henry Corrigan-Gibbs 和馬克斯普朗克軟體系統研究所、麻省理工學院的 Ralf Jung。該獎項每年頒發一次，旨在獎勵計算機科學和工程領域最優秀的博士論文。今年的獲獎者將在 10 月 23 日於舊金山舉行的典禮上獲頒獎項。範楚楚榮獲 2020 年 ACM 最佳博士論文獎，她的獲獎論文為 2019 年從 UIUC 獲得博士學位的論文，論文題目《Formal Methods for Safe Autonomy: Data-Driven Verification, Synthesis, and Applications》。獲獎理由：為嵌入式與信息物理系統的驗證做出了奠基性貢獻，且展示了該技術應用於工業系統的可能性。
論文地址：https://www.ideals.illinois.edu/handle/2142/106202範楚楚的論文還推動了靈敏度分析和符號可達性理論的發展；開發了一系列驗證算法和軟體工具（DryVR, Realsyn）；展示了驗證技術在工業規模自動系統中的應用。本文提出的算法是第一個基於靈敏度分析的、可應用於非線性混合系統有界驗證的數據驅動算法。這一工作在工業規模問題上的開創性示範表明，驗證技術是可以規模化的。目前這項靈敏度分析已經獲得了專利，並開始進入商業化實踐。範楚楚還開發了第一個用不完整模型來驗證「黑盒子」系統的算法，該系統結合了概率近似正確（PAC）學習、模擬關係與定點分析。這項工作產生了一個工具 DryVR，已經應用於幾十種系統，包括先進的駕駛輔助系統、基於神經網絡的控制器、分布式機器人與醫療設備等。另外，範楚楚提出的算法在非線性車輛模型系統的合成控制器中具有廣泛的應用前景。本文提出的 RealSyn 方法優於其他算法，為自動駕駛汽車實時運動規划算法鋪平了道路。
個人主頁：http://chuchu.mit.edu/範楚楚現為 MIT 航空航天工程系的 Wilson 助理教授，也是可信賴自動化系統實驗室（Reliable Autonomous Systems Lab, REASL）的負責人。她的團隊致力於使用形式化方法、機器學習和控制理論等來設計、分析和驗證安全的自動化系統。2009 至 2013 年，她本科就讀於清華大學自動化系，並被選為優秀畢業生。本科畢業後前往伊利諾伊大學香檳分校（UIUC）攻讀博士學位，並於 2019 年順利拿到計算機工程博士學位。她的主要研究興趣在於安全自動化系統、信息物理系統、形式化方法、控制理論、機器學習、強化學習和機器人技術等。
博士期間，她不僅發表了多篇期刊和會議論文，還榮獲了 UIUC CSL 學生論文獎、UIUC Robert T. Chien 紀念獎等多個獎項。
博士畢業後，她被聘任為加州理工學院的博士後研究員，並於 2020 年 8 月正式入職 MIT，擔任航空航天工程系的助理教授。
2020 年 ACM 博士論文獎的榮譽提名授予了 Henry Corrigan-Gibbs 和 Ralf Jung。
Corrigan-Gibbs 獲得提名的博士論文為《Protecting Privacy by Splitting Trust》，這項研究藉助理論與實踐相結合的技術改善了網際網路用戶隱私問題。他提出了一種新型的概率可驗證明 (PCP)系統，然後應用這種技術開發了可擴展、滿足實際行業需求的 Prio 系統。Prio 已經部署在包括 Mozilla 在內的幾家大公司中，自 2019 年底以來，它一直在夜間版本的 火狐瀏覽器中發揮作用，這是有史以來最大的 PCP 部署。論文地址：https://people.csail.mit.edu/henrycg/files/academic/papers/dissertation.pdfCorrigan-Gibbs 的論文研究了如何在不了解有關用戶的任何其他信息的情況下，有效計算有關用戶群的聚合統計數據。例如，該論文介紹了一種工具，使 Mozilla 能夠測量有多少火狐用戶遇到了某種網絡跟蹤器，而無需了解是哪些用戶遇到了該跟蹤器或遇到的原因。這項研究開發了一種新的概率可驗證明系統，該系統允許每個瀏覽器發送一個簡短的零知識證明，證明其對聚合統計數據的加密貢獻格式正確。論文的關鍵創新是驗證證明的速度非常快。Corrigan-Gibbs 是 MIT 電氣工程和計算機科學系的助理教授，他也是計算機科學和人工智慧實驗室的成員。他的研究重點是計算機安全、密碼學和計算機系統。此前，Corrigan-Gibbs 在史丹福大學獲得計算機科學博士學位。Ralf Jung 的博士論文為《Understanding and Evolving the Rust Programming Language (https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf)》，該論文為 Rust 語言的安全系統編程奠定了第一個正式的基礎。
自從 2010 年 Mozilla 開發 Rust 以來，它在整個行業中越來越受歡迎。Rust 解決了語言設計中一個長期存在的問題：如何平衡安全性和控制。與 C++ 一樣，Rust 為程式設計師提供了對系統資源的低級控制。不同的是，Rust 採用了強大的 「基於所有權」 的系統來靜態確保安全，從而不會出現內存訪問錯誤、數據競爭等安全漏洞。然而，在 Jung 的論文之前，沒有嚴格調查表明 Rust 的安全聲明是否真的成立，並且由於 Rust 庫中廣泛使用「unsafe escape hatches」，這些聲明就很難評估。
https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf在他的博士論文中，Jung 通過為 Rust 開發直接解釋安全和不安全代碼之間相互作用的語義基礎，來解決這一挑戰。在這些基礎上，Jung 為 Rust 的一個重要子集提供了安全性證明。此外，該證明在自動證明助手 Coq 中被形式化，因此其正確性得到保證。此外，Jung 提供了一個平臺，即使存在不安全代碼的情況下也可用於正式驗證基於類型的優化。通過 Jung 的領導和對 Rust 不安全代碼指南工作組的積極參與，他的工作已經對 Rust 的設計產生了深遠的影響，並為其未來奠定了重要的基礎。Jung 是馬克斯普朗克軟體系統研究所的博士後研究員，也是 MIT 並行和分布式作業系統組的研究員。他的研究興趣包括程式語言、驗證、語義和類型系統。他在馬克斯普朗克軟體系統研究所進行了博士研究，並在薩爾大學獲得了計算機科學的博士、碩士和學士學位。機器之心先前也報導過 2018 年、2019 年的博士論文獎。2018 年，UC 伯克利博士生 Chelsea Finn 憑藉論文《Learning to Learn with Gradients》榮獲此獎。來自微軟的 Ryan Beckett、本科畢業於清華姚班的馬騰宇獲得榮譽提名。
2019 年，畢業於特拉維夫大學的 Dor Minzer 獲得該獎項，來自微軟的 Jakub Tarnawski 和出身清華姚班的吳佳俊獲得榮譽提名獎。
惠普工作站人工智慧合作夥伴招募
作為新基建重要領域，人工智慧（AI）正滲透到社會生活各個領域。在萬物互聯的時代大背景下，合作共贏是行業發展的新趨勢。惠普工作站現發起 #合作夥伴招募計劃 #，誠邀每個深耕人工智慧領域的企業合作，一起探索更多 AI 行業發展新機遇。作為惠普工作站合作夥伴，將有機會獲得惠普免費樣機測試支持；與惠普共同打造創新解決方案，聯合推廣、合作開拓商機，助力行業發展，實現共贏；還有機會與國內 / 國際人工智慧領域專家交流，獲得第一線行業資訊。
© THE END
轉載請聯繫本公眾號獲得授權
投稿或尋求報導：content@jiqizhixin.com