科研导师：张昕，助理教授

研究方向：程序设计语言，软件工程，高可靠人工智能

个人主页：https://xinpl.github.io

程序推理技术指的是一系列用来保障软件质量、提高程序员生产效率的技术，包括程序分析、类型检查、各种形式化验证方法等。在几十年的发展中，它有着很多成功的用例：比如微软采用模型检查，消除了windows中大部分的蓝屏问题；又比如空中客车应用抽象解释成功验证了飞机控制器的正确性。正当研究人员为这一系列成果欢欣鼓舞，认为程序推理的各种技术正从学术界走向工业界、从成功个例走向广泛应用时，软件产业界却正经历着一场向“软件2.0”的转变。

什么是“软件2.0”？这一转变对程序推理技术又意味着什么？“软件2.0”指的是基于机器学习的软件。在过去（“软件1.0”时代），机器学习技术经常被用来发掘数据中的知识，为各种算法提供启发（heuristics），而在“软件2.0”时代，它们则直接代替了很多重要应用的关键组件。与“软件1.0”相比，“软件2.0”最大的不同在于谁来指定程序具体干什么。在过去，是程序员，而现在，则变成了数据。这一巨大的转变，对程序推理技术的发展既带来了机遇，也带了挑战。一方面，和很多计算机技术领域相同，由于机器学习技术的长足进步，程序推理技术可以借鉴其想法和技术，开发新的算法和系统。另一方面，随着机器学习正承担着越来越重要的角色，如何保障他们的质量已成为了急需解决的问题。

张昕老师的工作主要针对这两个方面，在程序推理和机器学习的交叉方向展开研究。

首先，他首先提出了逻辑与概率相结合的贝叶斯程序分析。传统程序分析大多以逻辑规则表示，因为逻辑规则能精准的表达分析设计者的意图，且能提供严格的正确性保证，然而逻辑规则并不能处理不确定性。这就造成了传统程序分析在处理规约模糊、代码缺失、平衡精度与速度等方面的不足。为了解决这一问题，张昕老师首先在逻辑程序分析中引入了概率。在保留传统逻辑表达的优点的同时，又靠概率解决了处理不确定性的难题。在逻辑与概率的统一程序分析框架下，他提出了自适应性程序分析、基于用户反馈的程序分析等自框架，极大提升了程序分析的可用性。此外，为了支持这些用例，他也在探究针对逻辑与概率这一表达的高效推导和学习算法。

然后，他也在探究如何用程序推理技术去解决机器学习的重要问题。比如，他提出了基于修改的可解释性机器学习。由于现代机器学习模型（如深度学习模型等）的不透明性，如何解释他们产生某种结果背后的原因，已成为急需解决的问题。由于缺乏可解释性，人们不知道是否能相信机器学习程序所作出的决策，在机器学习程序给出负面决策时，人们也不知道如何应对。此外，张昕老师也研究机器学习程序的公平性问题。人们使用自动算法替代人做决策的一个初衷是消除人在决策中所存在的偏见。然而，机器学习程序往往从数据中继承了来自人的偏见。针对这一问题，张昕老师研究如何验证、调试、修复一个程序的公平性。最后，张昕老师也关心如何克服现代机器学习程序缺乏模块化的问题，将传统程序分析扩展到它们上。

欢迎各位同学申请和张昕老师从事科研工作（博士和本科生科研为主）。不局限于以上方向，凡是和软件质量保证相关的，他都有着一定的兴趣。如果你有着对科学探索的渴望，耐得住寂寞的心态，改变世界的志向，扎实的数理和编程基础，请尽快联系张昕老师！