說明：本文經授權轉載自 DeepTech 深科技。

如果說哺乳期帶娃面試斬獲 MIT 助理教授 offer，是 90 後科學家範楚楚踏入社會的第一個驚喜；那麼在工作一年後，得知自己的

博士畢業論文獲得 ACM（美國計算機協會，Association for Computing Machinery） 最佳博士論文獎，想必是的她的又一個人生驚喜。

圖 | 範楚楚（來源：受訪者）

本科畢業於清華、博士畢業於伊利諾伊大學，29 歲入職 MIT 擔任助理教授，這是陝西女孩範楚楚的學霸履歷。關於此次論文獲獎，她告訴 DeepTech，這篇論文是她的博士生導師提名的。

圖 | 範楚楚獲得 ACM 最佳論文獎（來源：ACM 官網）

ACM 獎項一般喜歡既有理論貢獻、又有實際應用案例、同時同行評價較高的論文。提名流程一般是先在校內提名，每所大學可提名 1-2 篇博士論文，因此僅學校內部的競爭就已非常激烈。所以每一篇被學校提名的論文就已經是非常優秀的了。

最終參與評選的各校集中提交論文，ACM 評審委員會會選出三份論文，並授予其中一篇最佳論文獎，兩篇榮譽獎。此次其論文入選理由是：這篇工作為嵌入式與資訊物理系統的驗證做出了奠基性貢獻，且展示了該技術應用於工業系統的可能性。

圖 | 範楚楚獲獎論文（來源：受訪者）

獲獎論文主要成果：靈敏性分析

範楚楚的研究方向是形式化方法，該領域在分支上還有很多經典方法，比如模型檢測和抽象解釋，這都是已被驗證的實用數學工具。其中，模型檢測還拿過 2007 年的圖靈獎。

她表示，在計算機科學和軟體工程領域，形式化方法要求所有東西都必須給出嚴謹證明。其主要指導思路是在設計系統時，不僅僅只是為了最佳化實際過程中的表現，而是要先理解使用者對於系統的需求是什麼，從而進行相關設計。在設計完之後，還要做驗證並給出嚴謹的證明，證明系統一定會滿足當初的設計要求。

圖 | 範楚楚在作報告（來源：受訪者）

此前，形式化方法的理論性工作更多集中在程式或電路設計上。近年來，無人車、四旋翼飛機等更多是使用網路實體系統。以嵌入式系統為例，計算機程式主要是控制一些物理實體，最簡單的例子就是無人駕駛汽車，即演算法最終要控制汽車。

因此，範楚楚更關注物理實體上的系統性質，

一些跟安全強相關的性質也都跟物理實體相關，比如說汽車必須遵守交通規則，也不能撞車或者撞人。

這些性質是在物理實體上，但又是被演算法控制的，所以演算法和物理實體是緊密連線的，那麼這時就不能單看某個部分，而這正是形式化方法領域近年來的熱門應用，讓它去結合控制論和機器學習一類的方法，並用在無人駕駛汽車等更復雜的系統上。

說到這裡，範楚楚講述了自己的實習經歷，在加入 MIT 工作之前，她曾在豐田汽車實習過，該公司為了讓汽車尾氣排放達到政府標準，專門設計了一個嵌入式系統去控制車輛的動力系統。

而她本次的獲獎論文，講的正是把一類形式化的方法，具體來說是靈敏度分析，用在嵌入式系統上、特別是非線性混合系統，比如無人車系統上。

人類生活環境中有很多不確定性，獲悉這種不確定性對系統的干擾過程，就叫做靈敏度分析。比如，一陣風吹過來，四旋翼飛機可能就沒法飛了，甚至會掉下來。在控制系統中，工程師肯定希望系統對大的外界干擾不太靈敏，這樣才意味著系統的魯棒性很強。這時就會涉及到低靈敏度，即把系統設計得更加安全魯棒。

在範楚楚讀博時，線性系統上的靈敏度分析已得到廣泛研究，但在非線性系統的靈敏度分析上還面臨著一些困難。因此，她讀博期間主要研究靈敏度分析如何用在非線性系統上，以及如何將程式和動態的物理實體混合在一起。

由於工業界的一些系統並沒有非常適合的模型，讓她去做靈敏度分析。為此，她使用機器學習演算法去學習靈敏度分析，然後用靈敏度分析的方法去檢查系統的安全性。當外界遇到干擾或不確定性，想知道系統有多靈敏，就可以先讓系統執行，然後在其周圍透過靈敏度分析去計算安全閾值。靈敏度分析的好處在於，在遇到外界干擾時，它能保證系統風險不會超過分析出來的安全閾值。以特定系統的表現為例，想象它周圍被一層安全氣泡包裹著，那麼即便有外界干擾，系統的真實表現也不會跑出氣泡的外邊，所以也就相應有了安全性的保證。

可用在無人汽車系統和飛機系統中

範楚楚說，

該論文成果的應用範圍非常廣泛，而做演算法的優勢正在於它不侷限於某一個具體應用。

無人車系統和飛機系統的安全性非常重要。很多時候無人車等自主系統的技術已經非常發達，但由於無法證明系統的安全性，因此無人車輛或四旋翼飛機就無法正式投入生產使用。

要證明安全性，就必須用形式化方法，使用模型分析和安全分析等方法，去證明系統的安全性。因此，她的方案在很多系統中都是不可或缺的環節。

以車輛上的特定演算法為例，它的自動剎車系統以及尾氣排放系統都要經過靈敏度分析。研究中，她還做過衛星對接系統，假如想把一個大型航天器發到太空，其中一個做法是把航天器分成很多小件，然後在太空中進行一一對接，對接時會有安全性的要求。而她的做法是透過給相關模型設計控制器，然後去驗證控制器的安全性。

基於獲獎論文的成果，此前範楚楚讀博時的導師已經成立位於 UIUC 的初創公司。在獲獎論文中，她開發的幾個軟體工具，也幫助該公司的工程師們去分析設計出來的系統以及演算法的靈敏度。

據她介紹，當時美國也有不少機構去贊助這家公司，因此這並不是一個單純盈利的公司，而是探索新成果如何在現實生活中得到應用，以及去發現業介面臨的相關問題，因此該公司的產品主要是安全分析工具以及檢測工具。

哺乳期帶娃面試，驚喜遠大於困難

2018 年末範楚楚開始給各個學校投簡歷，2019 年上半年開始參加各種面試、並於 2020 年秋季入職 MIT 航空航天系。她認為這跟當時找在北美找教職的市場非常好有關，同年還有另一位 UIUC 的女生也拿到了 MIT 的教職。

收到 MIT 入職 offer 之前，她一共面試了十幾家學校，由於小孩當時才四五個月，其中四場面試都是帶娃面試。開始她覺得作為哺乳期媽媽，去找工作會很困難，但是導師和朋友都勸她大膽去嘗試，最終她發現驚喜遠遠大於遇到的困難。

圖 | 範楚楚（來源：受訪者）

面試過程一般是 1-2 天，所應聘的學校一般會要求求職者，做一兩個演講來介紹自己的成果，剩下的時間主要是和不同老師進行一對一的面試。

當時小孩年紀太小，她不想長時間離開孩子，但當時要進行連續三個月的集中面試，一旦飛走面試基本就是三天，她也不想把孩子放家裡。於是有幾場面試，是先生和孩子陪著她面試的。

範楚楚的愛人是自己的在西北工業大學附屬中學讀高中時的同學，高中畢業後都考上了清華。到申請博士時，兩人關係已經比較穩定，於是同時申請到了伊利諾伊大學，後來在讀博期間結婚。兩人後來的研究領域都屬於計算機，但她先生更偏向機器學習和自然語言處理，而她自己則是研究安全性分析和形式化方法。

圖 | 左一、左二分別是範楚楚的先生和女兒（來源：受訪者）

她說自己先生是自然語音處理領域的非常讓人佩服的學者，為家庭做了很多犧牲。找工作時，他們同時收到了杜克大學的 offer，但是因為自己更想要 MIT 的工作機會，於是先生就放棄了杜克大學的 offer，選擇距離 MIT 比較近的亞馬遜公司上班。

範楚楚從小生活在陝西漢中市，父母都出身自農村，靠自己努力成為漢中當地高校的老師。中考時，範楚楚被省會西安的西工大附中錄取，父母為了陪她讀書來到西安，並重新入職到一間大專。但她的經歷並非一帆風順，高考參加過兩次，她表示後來在投遞論文和申請教職的過程中，也都曾被拒絕過。

但是回頭來看，這些挫折也磨鍊除了更強大的自己。今年是她入職 MIT 的第二年，這位 30 歲科學家的科研之路，也才剛剛開始，未來可期。

-End-

參考：

https：//awards。acm。org/about/2020-doctoral-dissertation

https：//chuchu。mit。edu/