图片来源：视觉中国

近日，ACM公布了2020年博士论文奖得主，清华90后女学霸、UIUC博士、MIT助理教授范楚楚荣获该奖。

近日，ACM公布了2020年博士论文奖，清华90后女学霸范楚楚凭借着题为「安全自主性的形式方法：数据驱动的验证、综合和应用」的论文荣获该奖。

「ACM博士论文奖」每年由ACM（美国计算机协会）颁发，用来表彰计算机科学和计算机工程领域最佳博士论文的作者，同时获奖者将得到2万美元的奖金。

ACM表示，范楚楚的论文在嵌入式和网络物理系统的验证有着极为重要的贡献，论文提出的验证技术已经可以适用于工业规模的系统。

论文推进了敏感性分析（sensitivity analysis）和符号化可达性（symbolic reachability）的理论，并开发了相关的验证算法和软件工具（DryVR，Realsyn）。

同时，论文还为不完整模型（incomplete models）的「黑盒子」系统开发了第一个验证算法，该算法结合了概率近似正确（probably approximately correct, PAC）学习与模拟关系（simulation relations）和不动点分析（fixed point analyses）。

其中，DryVR已被应用于包括高级驾驶辅助系统、基于神经网络的控制器、分布式机器人和医疗设备等几十个系统之中。而Realsyn则要优于现有其他方法。

90后学霸

ACM博士论文奖得主范楚楚

本次杰出博士论文奖获得者范楚楚是一名90后学霸，清华大学自动化系本科2013届毕业生。

之后到美国伊利诺伊大学香槟分校（UIUC），成为电气与计算机工程系的六年硕博连读研究生。

2020年秋季加入麻省理工学院航天航空工程系担任助理教授，所在团队使用严格的数学方法，包括形式化方法、机器学习和控制理论，以设计、分析和验证安全自主系统。

从高中开始，范楚楚学霸身份就已经「暴露无遗」，曾参加全国物理竞赛和数学竞赛并获奖。

而在清华求学期间，也曾获三星奖学金、清华大学优良毕业生称号、全国电子设计竞赛三等奖、清华大学挑战杯等荣誉。

在UIUC攻读博士学位时，师从电气和计算机工程系教授Sayan Mitra，主要研究安全自主技术（如自动驾驶汽车、航天器和无人机）、控制理论、机器学习、机器人技术等。

读博期间更是发表了近20篇期刊论文和会议论文。

而本次获奖论文中提到的验证算法和软件工具C2E2、DryVR、Realsyn也是由范楚楚开发的。

范楚楚的学术成果喜人，也因此获得了UIUC的博士生众多奖项，2018年还获得了国家颁发给优秀自费留学生的奖学金。

结合范楚楚一直以来的学术背景与学术成果，这次能够获得UIUC 2020年度最佳博士论文奖也是意料之内。

荣誉奖得主

ACM除了公布2020年度杰出博士论文奖得主外，还公布了博士论文荣誉奖，获奖者分别是Henry Corrigan-Gibbs和Ralf Jung，两人均可获得1万美元的奖金。

ACM博士论文荣誉奖得主：Henry Corrigan-Gibbs

Henry Corrigan-Gibbs是计算机科学和人工智能实验室的成员，也是MIT电气工程和计算机科学系的助理教授，获得斯坦福大学计算机科学博士学位。

研究重点是计算机安全、密码学和计算机系统。

获奖论文题为：通过拆分信任以保护隐私（Protecting Privacy by Splitting Trust）。

论文链接：https://people.csail.mit.edu/henrycg/files/academic/papers/dissertation.pdf

作者研究了如何在不了解用户的任何其他信息的情况下稳健地计算有关用户群的汇总统计数据。

该论文开发了一种新的概率可检查证明系统，该系统允许每个浏览器发送一个简短的零知识证明，证明其对聚合统计数据的加密贡献格式正确。同时还具有极快的证明速度。

ACM博士论文荣誉奖得主：Ralf Jung

Jung是马克思·普朗克软件系统研究所的博士后研究员，也是MIT并行和分布式操作系统组的研究员，获得萨尔大学计算机科学专业的学、硕、博学位。

研究领域包括编程语言、验证、语义和类型系统。

获奖论文题为：理解和发展Rust编程语言（Understanding and Evolving the Rust Programming Language）。

论文链接：https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf

作者通过为Rust开发直接解释安全和不安全代码之间相互作用的语义基础，解决了缺少对Rust安全声明是否真正成立的严格调查的问题，为Rust的一个重要子集提供了安全性证明。

此外，论文还提供了一个平台，即使存在不安全的代码，也能用于正式验证基于类型的优化。

获奖论文

这篇论文是范楚楚2019年在完成伊利诺伊大学香槟分校电气和计算机工程专业博士学位时提交的论文。

论文链接：https://www.ideals.illinois.edu/bitstream/handle/2142/106202/FAN-DISSERTATION-2019.pdf

在现实世界中，自主系统的典型模型的验证和合成在理论上是不可知的，由于其高维度、非线性、非确定性和混合性，近似的解决方案也十分具有挑战性。

为了应对这些挑战，论文提出了：

• 通过非线性混合系统的可达性分析进行数据驱动的算法验证；

• 干扰下的高维线性系统的控制器合成。

在理论方面，论文提出的技术具有稳定性、精确性和相对完整性的保证。

在实验方面，论文提出的技术可以成功地应用于一系列具有挑战性的问题，包括首次验证的发动机控制模型、卫星控制系统、自动驾驶和基于高级辅助驾驶系统（ADAS）的操作。

论文贡献

1. 通过对非线性混合系统和非线性过渡系统的可达性分析，开发了一种数据驱动的安全验证算法，从而推进了网络物理系统（cyber-physical systems, CPS）的验证。

数据驱动算法在非线性系统的数据使用方面可以实现局部最优，并且成倍地减少了非线性过渡系统所需搜索的次数。从而能够验证难以解决的大型模型。

2. 提出了第一个用于验证现实世界中没有精确数学模型的网络物理系统框架。其关键是将这些系统视为带有「黑盒」模拟器的「白盒」自动机。。

因此，验证方法可以将自动机上的最坏情况的推理与黑盒上的概率推理结合起来。

3. 提出了一种极大地提高有干扰的大型线性系统的控制合成效率的算法。该算法通过无需量化的线性计算简化合成问题，并利用SMT求解器，实现了可扩展性。

此外，作者还开发了相关的软件工具：C2E2（混合系统的验证）、DryVR（黑盒组件的系统验证）和RealSyn（用于整体）。

其中，C2E2是第一个成功验证丰田动力总成控制系统和航天器会合问题的工具；也是目前唯一能够处理混合信号电路等高度非线性模型的工具。

参考资料：

https://awards.acm.org/about/2020-doctoral-dissertation

本文转载自微信公众号“新智元“（ID：AI_era），来源：ACM，编辑：Priscilla、好困。文章原标题：《90后清华女校友范楚楚获ACM 2020唯一博士论文奖！出任MIT助理教授后再摘桂冠》。文章为作者独立观点，不代表芥末堆立场，转载请联系原作者。