清华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 岁科学家的科研之路,也才刚刚开始,未来可期。

原文连结六度声明DMCA 政策

相关新闻

大家都在看

留言区

留言如有不雅或攻击性文字、重复灌水、广告、外站连结等内容,本网站将保有删除留言之权利