清华90后 MIT助理教授范楚楚获ACM最佳博士论文奖

如果说哺乳期带娃面试斩获 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
岁科学家的科研之路,也才刚刚开始,未来可期。

天钧 | 今日时事新闻:清华90后 MIT助理教授范楚楚获ACM最佳博士论文奖

相关推荐: 毕业季的女博士们:工作难找、陷入内卷、被离婚…

历史学博士Amber在海边放松心情,她在6月接到了丈夫的离婚电话。 讲述人:Cindy,北大文科学士,牛津考古博士。 “我们的社会是不是产出太多没用的文科博士了?” 2014年7月,我从北京大学毕业,前往英国读研,专业是我一直心念念的考古学——虽然在本科选修过…