Frits Vaandrager讨论“模型学习”(www.eqigeno.com/magazines/2017/2/212445),这是ACM 2017年2月通信中的一篇综述文章。
---
成绩单
00:00一个新的城市。当你停车时,你会看到一个陌生的停车计时器。你照着步骤做,也许会犯一些错误。最后,你会明白的。
00:17我们有解决停车计时器等谜题的神奇能力。现在,荷兰的一位教授教计算机也能做到这一点。
00:27Frits Vaandrager在《模型学习》中向我们展示了自动查询的组合是如何找出这些黑盒子机器是如何工作的。
00:37(介绍图形/音乐)
00:47就像停车计时器一样,这个咖啡设备是一个“状态机”,我们的行为将它从一个状态移动到另一个状态。
00:56VAANDRAGER博士:所以,作为人类,我们通过与设备交互,很快就会发现这种设备是如何工作的,我们在心理上构建了一个小的状态机模型;我们知道如何使用它。
01:07安全研究人员经常使用一种名为“模型检查”的过程来探测现实世界的系统,即向系统抛出输入,看看它将如何反应。但首先,他们需要创建该系统的理论版本。
01:21VAANDRAGER博士:你有一个系统的数学模型,你以某种方式构建了它,也许你是根据规格手工完成的,也许你是从软件中提取出来的。然后你要做的就是分析这个模型;您希望探索模型中的所有状态,可能有很多状态。
01:38但vanandrager博士发现同样的问题一次又一次地出现。
01:43VAANDRAGER博士:我经常注意到,我构建的模型并不能准确描述我想研究的系统. ...所以我对这个问题非常感兴趣:好吧,我们如何建立可靠的实现模型,真正描述这个实现在做什么的模型?这就是模型学习所提供的。
02:08该过程从探测系统开始。
02:11VAANDRAGER博士:在模型学习中,你在系统上做一些实验:你按下按钮,观察结果输出。然后系统地将这些观察记录在表格中。然后在某一时刻你会发现有一些有限自动机可以解释你要学习的系统的所有行为。然后你就形成了一个假设。
02:37通过迭代这些步骤,模型学习揭示了系统中隐藏的逻辑——它并不总是它的创建者所期望的逻辑。
02:45VAANDRAGER博士:例如,在SSL协议的情况下,我们研究了一系列的实现。我们发现所有这些协议实现的状态机都是不同的. ...有时也会出现错误。例如,在一个实现中,我们发现了一个严重的问题,同时已经修复,由于我们的努力,实现已经改变。
03:11这种方法被用于开发过时软件的新版本,甚至暴露出数百万人使用的银行卡系统的缺陷。
03:21范德雷格博士:模型学习吸引我的地方在于,你将优秀的理论——自动机理论非常优雅和优秀——和大量的应用结合在一起. ...因此,在支撑我们互联网的一些主要协议中找到错误,这是一个真正的应用程序。
03:44在ACM通信2017年2月号的评论文章,模型学习中获得所有细节。
03:52(结尾部分和学分)