一个CM通信
贡献的文章
走向可验证的人工智能
图片来源:Peter Crowther Associates
人工智能(AI)是一个用来描述试图模仿人类智能方面的计算系统的术语，包括我们直觉上与智能有关的功能，如学习、解决问题、理性思考和行动——例如，参见罗素和诺维格。26我们对人工智能这个术语的解释很宽泛，包括了与之密切相关的领域，比如机器学习(ML)。大量使用人工智能的系统，因此被称为人工智能系统，在包括医疗保健、交通运输、金融、社交网络、电子商务和教育等领域产生了重大的社会影响。
关键的见解
这种日益增长的社会规模影响带来了一系列风险和担忧，包括人工智能软件的错误、网络攻击和人工智能系统的安全。4因此，人工智能系统的验证和验证问题，以及更广泛地说，实现可信的人工智能的问题，39已经开始要求学术界的关注。我们将“经过验证的AI”定义为，设计的AI系统具有强大的、理想的可证明的、与数学特定需求相关的正确性保证。我们如何才能实现这个目标?
在本文中，我们从形式化方法的角度来考虑已验证AI的挑战，形式化方法是计算机科学和工程的一个领域，涉及系统的严格数学规范、设计和验证。38形式化方法的核心是证明:形成证明义务的规范;设计符合这些义务的系统;并通过算法证明搜索，验证系统确实符合其规格。从规范驱动的测试和仿真到模型检查和定理证明，一系列形式化方法通常用于集成电路(ICs)的计算机辅助设计，并被广泛应用于发现软件bug、分析网络物理系统(CPS)和发现安全漏洞。我们回顾了传统上正式方法的应用方式，确定了AI系统中出现的独特挑战，并提出了克服这些挑战的想法和最近的进展。
本文试图解决的不仅仅是特定类型的AI组件，如深度神经网络(DNNs)，或特定方法，如强化学习(RL)。它试图涵盖广泛的人工智能系统及其设计过程。此外，我们认识到，正式的方法只能提供一种方法来实现值得信赖的人工智能，我们的观点是为了补充其他领域的观点。我们的观点在很大程度上是由在自主和半自主系统中使用人工智能所产生的问题所决定的，在这些系统中，对安全和正确性的担忧更为尖锐，尽管我们相信这里提出的想法适用范围更广。本文是为正式方法研究者和实践者以及更广泛的计算机科学社区编写的。对于前者，我们提出了关于真正的问题在哪里以及形式化方法如何产生最大影响的观点。对于后者，我们勾勒出形式化方法如何成为值得信赖的AI的关键推动者的愿景。
我们首先简要介绍形式验证的背景，一个说明性的例子，并总结本文的关键思想。然后，我们概述了验证型人工智能面临的五个挑战，讨论了最近的进展，并提出了应对这些挑战的原则。一个
概述
图1展示了正式验证、正式综合和正式指导的运行时弹性的典型过程。考虑正式的验证过程，它从三个输入开始:
图1。验证、合成和运行时弹性的正式方法。
- 一个待验证系统的模型，年代。
- 一个环境模型，E。
- 待验证的财产Φ。
验证器生成一个“是/否”的答案作为输出，表明是否年代在环境上满足物业ΦE。通常，“no”输出伴随一个反例，也称为错误跟踪，这是一个系统的执行，表明Φ是如何被伪造的。一些验证工具还包括带有“是”答案的正确性证明或证书。我们从广泛的角度看待形式方法，包括使用形式说明、验证或综合的某些方面的任何技术。例如，我们包括基于仿真的硬件验证方法或基于模型的软件测试方法，因为它们使用正式的规范或模型来指导仿真或测试的过程。
要将正式的验证应用于AI系统，一个人必须至少能够表示三种输入年代,E，和Φ在形式上(理想情况下)存在有效的决策程序来回答前面描述的“是/否”问题。然而，正如将要展示的，即使构造三个输入的良好表示也不是简单的，更不用说处理底层设计和验证问题的复杂性了。
我们将用半自动驾驶领域的例子来说明本文中的想法。图2展示了一个人工智能系统的示例:闭环CPS包括半自主车辆、ML组件及其环境。具体来说，假设半自主的“自我”汽车拥有自动紧急制动系统(AEBS)，该系统试图检测和分类前方的物体，并在需要避免碰撞时启动刹车。图2图中显示，AEBS是一个由控制器(自动制动)、设备(被控制的车辆子系统，包括自动系统堆栈的其他部分)、传感器(摄像机)以及使用DNN实现的感知组件组成的系统。当AEBS与车辆的环境相结合时，就形成了一个闭环CPS。自我车辆的环境包括车外的代理和物体(其他车辆、行人等)以及车内的物体，例如司机。这个闭环系统的安全要求可以非正式地描述为在移动的自我车辆和道路上任何其他代理或物体之间保持安全距离的特性。然而，这样一个系统的规范、建模和验证有许多细微差别。
图2。带有机器学习组件的闭环信息物理系统的例子(Dreossi等人介绍)。5)。
首先，考虑对半自动驾驶汽车的环境进行建模，在这种环境中，甚至包括环境中有多少和哪些代理(人类和非人类)都存在相当大的不确定性，更不用说它们的属性和行为了。其次，使用AI/ML的感知任务可能很难(如果不是不可能的话)正式指定。第三，像dnn这样的组件可以是复杂、高维的对象，它们在复杂、高维的输入空间上运行。因此，甚至生成三个输入年代，E， Φ以一种使验证可追溯的形式对正式的验证过程是具有挑战性的。
假设一个人解决了这个问题，那么他就面临着验证一个复杂的基于人工智能的CPS的艰巨任务图2，其中组合(模块化)方法对于可伸缩性至关重要，但难以实现—例如，由于组合规范的困难。最后，按构造正确的设计方法有望实现可验证的AI，但它们仍处于起步阶段，关键取决于规范和验证的进步。图3总结了验证人工智能面临的五个挑战领域。对于每个领域，我们将当前有希望的方法提炼为三个原则，以克服这一挑战，并将其描述为节点。节点之间的边表示已验证AI的哪些原则相互依赖，共同的依赖线用单一颜色表示;我们将在“结论”中概括这些依赖关系。本文的其余部分将详细阐述这些挑战和相应的原则。
图3。总结验证人工智能的五个挑战领域，为解决它们提出的15个相应原则，以及它们之间的联系和依赖关系(相同的颜色表示一个共同的依赖线程)。
环境建模
基于AI/ ml的系统运行的环境通常是复杂的。例如，考虑对自动驾驶汽车必须运行的各种城市交通环境进行建模。事实上，AI/ML经常被精确地引入这些系统，以处理这些复杂性和不确定性。当前的ML设计流程通常用数据隐式地指定环境。许多AI系统的设计目的是在其操作过程中发现并理解其环境，而传统系统则是为预先指定的环境设计的。然而，所有形式的验证和综合都是关于环境模型的。因此，必须在环境模型中解释输入数据的假设和属性。我们将这种二分法提炼为AI系统环境建模的三个挑战，并开发相应的原则来解决它们。
建模不确定性。在形式验证的传统使用中，通常将环境建模为受约束的不确定过程或“干扰”。这种“过度近似”的环境建模允许人们保守地捕捉环境的不确定性，而不需要过于详细的模型，因为这种模型可能无法进行有效的推理。然而，对于基于人工智能的自治，纯粹的非确定性建模很可能会产生太多虚假的bug报告，使得验证过程在实践中毫无用处。例如，考虑为自动驾驶汽车建模环境车辆的行为，其中可能的行为范围非常广泛，如果采用纯不确定性建模，总是可能发生事故。此外，许多AI/ML系统隐式或显式地对来自环境的数据或行为进行分布假设，从而产生了对概率建模的需求。由于很难准确地确定潜在的分布，因此不能假设由此产生的概率模型是“完美的”，建模过程中的不确定性必须在模型本身中表现出来。
概率正式建模。为了应对这一挑战，我们建议使用结合概率和非确定性建模的形式主义。当概率分布可以可靠地指定或估计时，可以使用概率建模。在其他地方，非确定性建模可以用于过度近似环境行为。虽然马尔可夫决策过程(MDPs)等形式主义已经提供了一种混合概率和非决定论的方法，但我们相信更丰富的形式主义，如概率规划的范式(例如，Fremont等人)。10和Milch等人。20.)，可以提供一种表达和编程的方式来建模环境。我们预计，在许多情况下，这种概率程序将需要从数据中学习/合成(部分)。在这种情况下，学习参数中的任何不确定性必须传播到系统的其余部分，并在概率模型中表示。例如，凸MDPs25提供一种用学习到的转移概率值来表示不确定性的方法，并扩展验证和控制算法来解释这种不确定性。
未知的变量。在传统的领域进行形式化的验证，如验证设备驱动程序，系统之间的接口年代及其环境E定义得很好，还有E只能与年代通过这个接口。对于基于人工智能的自治，如“概述”中的示例，接口是不完美的，由传感器和感知组件指定，只部分地和嘈杂地捕捉环境，它没有捕捉之间的所有交互年代而且E。不是所有的环境变量(特征)都是已知的，更不用说感知了。即使在已知环境变量的受限场景中，也明显缺乏关于它们演化的信息，特别是在设计时。此外，建模传感器，如激光雷达，代表了环境的接口，是一个主要的技术挑战。
内省环境建模。我们建议通过开发内省的设计和验证方法来解决这个问题——也就是说，它们会对系统进行内省年代通过算法来识别假设一个关于环境的E这足以保证该规格的满意Φ。31理想情况下,一个必须是此类假设中最薄弱的，而且必须足够高效，能够在设计时生成，并在运行时通过可用的传感器和其他环境信息来源进行监测，以便在违反这些信息时采取缓解措施。此外，如果涉及到人工操作，人们可能希望一个翻译成可以理解的解释，所以年代可以向人类“解释”为什么它可能不能满足规格Φ。这些多重需求的处理，以及对良好传感器模型的需求，使得内省环境建模成为一个非常不容易解决的问题。31初步工作表明，这种可监控假设的提取在简单情况下是可行的，17尽管这需要更多的工作来实现。
我们需要对ML组件及其上下文进行建模的技术，以便能够验证具有语义意义的属性。
人类行为建模。对于许多人工智能系统，如半自主车辆，人类代理是环境和/或系统的关键部分。手工制作的人类模型不能充分捕捉人类行为的可变性和不确定性。另一方面，数据驱动的人类行为建模方法对ML模型使用的特征的表达能力和数据的质量非常敏感。为了实现人类- ai系统的高保证，我们必须解决当前人类建模技术的局限性，并为其预测精度和收敛性提供保证。
活跃数据驱动建模。我们认为，人类建模需要一种主动的数据驱动方法，用数学形式表达模型结构和特征，以适应正式方法的使用。人类建模的一个关键方面是捕捉人类的意图。我们提出了一种三管齐下的方法:基于专家知识定义模型模板/特性，使用离线学习来完成设计时使用的模型，以及在运行时通过监测和与环境交互来学习和更新环境模型。例如，通过人体实验从驾驶模拟器中收集的数据可以用来生成人类驾驶员行为模型，这对自动驾驶车辆的验证和控制很有用。27，28此外，对抗性训练和攻击技术从计算机安全13可以用于人类模型的主动学习，并可以进一步针对导致不安全行为的特定人类行为设计。这些技术可以帮助开发人类-人工智能系统的验证算法。
正式规范
正式的验证在很大程度上依赖于有一个正式的规格说明——一个关于系统应该做什么的精确的、数学的陈述。即使在形式化方法已经取得相当成功的领域，提出高质量的形式化规范也是一项挑战，但对于AI系统来说，这一挑战有一些独特的方面，我们将在下面详细阐述。
Hard-to-formalize任务。中的感知模块图2该控制器必须对物体进行检测和分类，以便将车辆和行人从其他实体中区分出来。在经典的形式化方法意义上，这个模块的准确性需要对每一类道路用户和对象进行形式化定义，这是极其困难的，甚至是不可能的。这个问题存在于该感知模块的任何实现中，而不仅仅是基于深度学习的方法。类似的问题也出现在其他涉及感知和交流的任务中，比如自然语言处理。那么，我们如何为这样的模块指定精度属性呢?规范语言应该是什么，可以使用什么工具来构建规范?
端到端/系统级规范。为了解决上述挑战，我们稍微改变了这个问题。与其直接尝试对一项难以形式化的任务进行规范，不如首先专注于精确地指定AI系统的端到端行为。从这个“系统级”规范中，我们可以得到难以形式化组件的输入-输出接口上的约束。这些约束作为与整个AI系统环境相关的组件级规范。对于我们的AEBS例子(图2)，这涉及到指定属性Φ对应于在运动过程中保持与任何物体的最小距离，从中我们得出DNN的输入空间的约束，捕获一个语义上有意义的输入空间进行对抗性分析(见Dreossi等人)。5)。
定量与布尔规格。传统上，正式的规范往往是布尔型的，将给定的系统行为映射为“真”或“假”。然而，在AI和ML中，规格通常是作为指定成本或奖励的目标函数给出的。此外，游戏中可能存在多个目标，其中一些目标必须同时满足，而另一些目标则需要在特定环境中相互权衡。将布尔和定量方法统一到规格说明的最佳方法是什么?是否存在一种形式主义，可以以统一的方式捕捉AI组件的常见讨论属性，如健壮性和公平性?
混合quantitative-Boolean规范。布尔规范和定量规范都有它们的优点:布尔规范更容易组成，但是目标函数使自己适合基于优化的技术来验证和综合，并定义更细的性能满足粒度。弥合这一差距的一种方法是转向定量规范语言，例如同时使用布尔语义和定量语义的逻辑(例如，度量时态逻辑)22)或将自动机与奖励功能相结合的RL。15另一种方法是将布尔规范和定量规范结合到一个通用规范结构中，例如规则手册，1其中规范可以按层次结构组织、比较和聚合。翼39已经确定了人工智能系统的几类属性，包括健壮性、公平性、隐私性、问责性和透明度。将形式方法和ML思想连接起来的新型形式主义正在开发中，以对这些属性的变体进行建模，包括，例如，语义健壮性的概念。32
数据vs.形式需求。“数据就是规范”的观点在机器学习中很常见。在有限的输入集上标记为“地面真实”的数据通常是正确行为的唯一规范。这与形式化方法非常不同，在形式化方法中，规范通常以逻辑或自动机形式给出，定义所有可能输入的一组正确行为。这种差距可能会带来问题，尤其是当数据有限、有偏见或来自非专家时。我们需要技术来形式化数据的属性，包括设计时可用的数据和尚未遇到的数据。
规范开采。为了弥合数据和形式规范之间的差距，我们建议使用算法从数据和其他观察中推断规范——所谓的规范挖掘技术。这种方法通常可以用于ML组件，包括感知组件，因为在许多情况下，不需要有确切的规范或人类可读的规范。规范挖掘方法还可以用于从演示中推断人类的意图和其他属性37或更复杂形式的多个代理之间的互动，包括人类和人工智能。
学习系统建模
在大多数传统的形式化验证应用中，系统年代是固定的，并且在设计时就知道——例如，它是一个程序，或者是一个用编程语言或硬件描述语言描述的电路。系统建模问题主要是关于减小的大小年代把不相关的细节抽象化，变成一个更容易处理的问题。人工智能系统给系统建模带来了一个非常不同的挑战，主要源于机器学习的使用:
- 高维输入空间。用于感知的ML组件通常在非常高维的输入空间上操作。在Dreossi等人的例子中，5每个输入的RGB图像为1000 × 600像素，包含256个1000年x600x3元素，通常输入是一串这样的高维向量。尽管研究人员已经对高维输入空间使用了形式化的方法(例如，在数字电路中)，但基于ml的感知的输入空间的性质是不同的——不完全是布尔，而是混合的，包括离散变量和连续变量。
- 高维参数/状态空间。ML组件(如深度神经网络)拥有数千到数百万的模型参数和基本组件。例如，作者在实例中使用的最先进的dnn图2多达6000万参数，数十层。这为验证带来了巨大的搜索空间，需要仔细的抽象。
- 在线适应和进化。一些学习系统，比如使用RL的机器人，会在遇到新的数据和情况时进化。对于这样的系统，设计时验证必须考虑到系统行为的未来变化，或者随着学习系统的发展逐步在线执行。
- 在上下文中建模系统。对于许多AI/ML组件，它们的规范只由上下文定义。例如，验证安全性图2美国的基于dnn的系统需要其环境的模型。我们需要对ML组件及其上下文进行建模的技术，以便能够验证具有语义意义的属性。
近年来，许多工作都集中在提高工具验证dnn的鲁棒性和输入输出特性的效率上(见Liu等人)。18最近的调查)。然而，这还不够。需要在三个方面取得进展:
自动化的抽象和高效的表示。自动生成系统抽象的技术已经成为形式化方法的关键，在将形式化方法扩展到大型硬件和软件系统中扮演了关键的角色。为了解决基于ML系统的非常高维混合状态空间和输入空间的挑战，我们需要开发有效的技术，将ML模型抽象为更容易进行形式分析的更简单的模型。一些有前途的方向包括使用抽象解释来分析dnn(例如，Gehr等。12)，开发用ML组件伪造信息物理系统的抽象概念，5为验证设计新的表示(例如，星集和其他例子)36)。
解释和因果关系。如果学习者在预测的同时解释这些预测是如何从数据和背景知识中产生的，那么为学习系统建模的任务就可以简化。虽然这个想法并不新鲜，但ML社区已经在基于解释的泛化等术语下进行了研究21最近，人们对使用逻辑来解释学习系统的输出产生了新的兴趣(例如，Jha等人。16)。生成解释可以帮助在设计时调试设计和规范，并为运行时保证合成健壮的AI系统。包含因果推理和反事实推理的ML24还可以帮助生成使用正式方法的解释。
语义特征空间。敌对的分析13当生成的对抗输入和反例在使用ML模型的环境中具有语义意义时，ML模型的形式化验证更有意义。例如，根据汽车颜色或一天中的时间的微小变化分析DNN目标检测器的技术可以说比那些向少量任意选择的像素添加噪声的技术更有用。大多数当前的方法(例如Goodfellow等。13或Liu等人。18)在这方面做得不够。我们需要语义对抗性分析7在这种模式下，ML模型在它们所属的系统的上下文中进行分析。一个关键步骤是表示语义特征空间建模ML系统运行的环境，而不是定义ML模型输入空间的具体特征空间。这遵循了具象特征空间(例如，交通场景图像)中具有语义意义的部分形成了一个比完整具象特征空间低得多的潜在空间的直觉。图2的语义特征空间是代表自动驾驶汽车周围3D世界的低维空间，而具体特征空间是高维像素空间。由于语义特征空间是低维的，它可以更容易地搜索(参见，例如，Dreossi等。5或Huang等人。14)。然而，我们需要一个“渲染器”来将语义特征空间中的点映射到具体特征空间中的点。呈现器的属性，比如可微性，可以使应用形式化方法对语义特征空间进行目标定向搜索变得更容易。
设计与验证的计算引擎
硬件和软件系统的形式化方法的有效性是由潜在的“计算引擎”的进步驱动的——例如，布尔可满足性求解(SAT)、可满足性模理论(SMT)和模型检查。考虑到AI/ML系统的规模、环境的复杂性以及所涉及的新型规范，需要一种新型的计算引擎来进行高效、可扩展的培训、测试、设计和验证。我们确定了实现这些进展必须克服的关键挑战。
数据集的设计。数据是机器学习的基本出发点。任何提高ML系统质量的探索都必须提高它所学习数据的质量。形式化方法如何帮助系统地选择、设计和扩充用于ML的数据?
ML的数据生成与硬件和软件的测试生成问题有相似之处。形式化方法已被证明对系统的、基于约束的测试生成是有效的。但是，对人工智能系统的要求是不同的。约束的类型可能要复杂得多——例如，对使用传感器从复杂环境(如交通状况)捕获的数据的“真实性”进行编码的要求。我们不仅需要生成具有特定特征的数据项(比如发现bug的测试)，还需要生成满足分布约束的集合。数据生成还必须满足数据集大小和多样性的目标，以有效地训练和泛化。这些需求需要开发一套新的正式技术。
采用正规方法进行对照随机化。数据集设计的这个问题有很多方面。首先，必须定义“合法”输入的空间，以便根据应用程序语义良好地形成示例。其次，需要约束来捕捉与真实数据的相似性度量。第三，通常需要对生成的样例分布进行约束，以保证学习算法收敛到真实概念。
我们相信这些方面可以通过随机的形式化方法来解决——生成受形式化约束和分布要求约束的数据的随机算法。一种新的技术，称为控制即兴创作，9持有的承诺。即兴演奏是随机琴弦的产生器(举例)x满足三个约束条件:
- 定义法律空间的硬约束x
- 定义如何生成的软约束x必须与真实世界的例子相似吗
- 定义输出分布约束的随机性要求。
控制即兴理论仍处于起步阶段，我们刚刚开始了解计算的复杂性，并设计有效的算法。反过来，即兴创作依赖于最近在计算问题上的进展，如约束随机抽样和模型计数(例如，Meel等人)。19)和基于概率规划的生成方法(例如，Fremont等。10)。
定量验证。除了传统指标(状态空间维度、组件数量等)所衡量的AI系统规模之外，组件的类型可能要复杂得多。例如，自动驾驶和半自动驾驶汽车及其控制器必须建模为混合动力系统，结合离散和连续动力学。此外，环境中的代理(人类，其他车辆)可能需要建模为概率过程。最后，这些要求不仅包括传统的布尔安全性和活动性规范，还包括对系统鲁棒性和性能的定量要求。然而，现有的验证方法大多针对回答布尔验证问题。为了解决这一差距，必须开发新的可扩展的量化验证引擎。
量化语义分析。人工智能系统的复杂性和异质性意味着，一般来说，规范(布尔或定量)的正式验证是不可判定的——例如，甚至决定线性混合系统的状态是否可达也是不可判定的。为了克服计算复杂性造成的这一障碍，我们必须在本节前面讨论的抽象和建模方法中增加在语义特征空间上进行概率和定量验证的新技术。对于具有布尔和定量语义的规范形式主义，在诸如度量时间逻辑的形式主义中，作为优化的验证公式对于将形式方法的计算方法与优化文献中的方法统一起来至关重要，例如基于模拟的时间逻辑证伪(例如，Nghiem等人)。22)，尽管它们必须应用于语义特征空间以提高效率。6这种伪造技术也可用于ML组件训练数据的系统、对抗性生成。6概率验证技术应该超越传统的形式主义，如马尔可夫链或MDPs，在语义特征空间上验证概率程序。类似地，SMT求解工作必须扩展，以更有效地处理成本约束——换句话说，将SMT求解与优化方法相结合(例如，Shoukry等人)。34)。
我们需要了解在设计时可以保证什么，设计过程如何有助于在运行时安全操作，以及设计时和运行时技术如何有效地互操作。
AI/ML的合成推理。对于可扩展到大系统的形式化方法，组合(模块化)推理是必不可少的。在组合验证中，一个大型系统(例如，一个程序)被分解成它的组件(例如，过程)，每个组件根据一个规范进行验证，然后这些组件规范一起构成了系统级的规范。常用的合成验证方法是使用assume-guarantee合同。例如，一个过程假设它的开始状态(前置条件)，反过来又保证它的结束状态(后置条件)。类似的假设-保证范例已经为并发软件和硬件系统开发过。然而，这些范式并没有涵盖AI系统，这在很大程度上是由于在“正式规范”部分中讨论的指定AI系统的挑战。组合验证需要组合规范—也就是说，组件必须是正式指定的。然而，正如“形式化规范”中所指出的，形式化地指定感知组件的正确行为可能是不可能的。因此，我们面临的挑战之一就是开发不依赖于完整作曲规范的作曲推理技术。此外，人工智能系统的定量和概率性质要求将组成推理理论扩展到定量系统和规格。
推断部分合同。人工智能系统的组合设计和分析需要在多个方面取得进展。首先，需要在一些有前景的初始工作(例如，Nuzzo等人)的基础上，为此类系统的语义空间开发概率假设-保证设计和验证理论。23)。第二，归纳合成的新技术30.必须设计成以算法方式生成假定担保契约，以减少规范负担并促进组合推理。第三，为了处理组件(比如感知)没有精确的形式规范的情况，我们建议采用从系统级分析中推断组件级约束的技术(例如，Dreossi等人)。5)，并使用这些约束来将组件级分析(包括对抗性分析)的重点放在搜索输入空间的“相关”部分。
Correct-by-Construction智能系统
在理想的情况下，验证应该与设计过程相结合，这样系统就可以“根据构造而正确”。例如，验证可以与编译/合成步骤交织在一起，例如在集成电路中常见的寄存器-转移级(RTL)设计流程中，也可以将其集成到合成算法中，以确保实现满足规范要求。我们能否为AI系统设计一个合适的“施工正确”的设计流程?
ML组件的规范驱动设计。给定一个正式的规范，我们能设计一个机器学习组件(模型)证明满足该规范吗?这种全新的ML组件设计包括许多方面:(1)设计数据集，(2)合成模型的结构，(3)生成一组具有代表性的特征，(4)合成超参数和ML算法选择的其他方面，以及(5)在合成失败时自动化调试ML模型或规范的技术。
ML组分的形式合成。解决方案正在出现，解决了前面列出的一些方面。可以使用语义丢失函数(例如，Xu等人)在ML模型上强制属性。40)或通过认证的健壮性(例如，Cohen等人。2)。这些技术可以与神经结构搜索等方法相结合，产生按结构正确的dnn。另一种方法基于正在兴起的形式归纳综合理论，30.满足形式说明的程序实例的综合。解决正式归纳综合问题最常见的方法是使用oracle-guided方法，在这种方法中，学习者与回答查询的oracle配对。例如图2， oracle可以是一个伪造者，生成反例，显示已学习组件的故障如何违反系统级规范。最后，使用定理证明来确保用于训练ML模型的算法的正确性(例如，Selsam等。29)也是朝着构建正确的ML组件迈出的重要一步。
基于ml的系统设计。第二个挑战是设计一个包含学习和非学习部分的整体系统。几个研究问题出现了。我们能否计算出ML组件可以被约束在哪些安全范围内运行?我们能否设计出一种控制或规划算法，能够克服它接收输入的基于ml的感知组件的限制?我们能否为AI系统设计组合设计理论?例如，如果使用两种ML模型对两种不同类型的传感器数据(如LiDAR和视觉图像)进行感知，并且在一定的假设条件下，每种模型都满足其规格要求，那么在什么样的条件下它们可以一起使用来提高整个系统的可靠性呢?
安全学习。在这方面取得进展的一个突出例子是基于学习的安全控制方面的工作(例如，Fisac等人)。8)。在这种方法中，预先计算出一个安全包络线，并使用学习算法在该包络线内调整控制器。需要技术来有效地计算这种安全信封，例如，基于可达性分析。35同样，安全RL领域也取得了显著的进展(参见Garcia和Fernández11一项调查)。然而，这些还没有完全解决ML在感知和预测方面带来的挑战——例如，被证明是安全的、端到端、深度RL尚未实现。
桥接弹性AI的设计时间和运行时间。正如“环境建模”一节所讨论的那样，许多AI系统在无法预先指定的环境中运行，因此，总是会有我们无法证明其正确性的环境。因此，在运行时实现容错和抗错能力的技术对人工智能系统尤为重要。我们需要系统地理解在设计时可以保证什么，设计过程如何有助于在运行时安全、正确地操作AI系统，以及设计时和运行时技术如何有效地互操作。
运行时保证。关于容错和可靠系统的文献为我们开发运行时保证技术(即运行时验证和缓解技术)提供了基础。例如，单纯形法33提供一种将复杂但容易出错的模块与安全的、经过正式验证的备份模块组合在一起的方法。结合设计时和运行时保证方法的最新技术(例如，Desai等人)。3.)展示了未经验证的组件(包括基于AI和ML的组件)如何被包装在运行时保证框架中，以提供安全操作的保证。然而，这些目前仅限于特定类型的系统，或者它们需要手动设计运行时监视器和缓解策略。在内省环境建模等方法上还需要做更多的工作31以及人工智能的监视器和安全撤退策略的综合。
这里讨论的按构造正确设计方法可能会引入开销，从而更难满足性能和实时需求。然而，我们相信(也许不是直观地)正式的方法甚至可以帮助改善系统的性能或能源效率，在以下意义上。传统的性能调优往往是与上下文无关的—例如，任务需要满足期限，而不受其操作环境的影响。然而，在某些环境中，如果在设计时对这些环境进行正式的描述，并在运行时进行监视，并且在这些环境中进行的系统操作被正式验证为安全的，ML模型可能会以精度换取更高的效率。这种取舍可以成为未来研究的一个富有成效的领域。
结论
从形式化方法的角度，我们剖析了设计高保证AI系统的问题。总结如图3，我们确定了将形式化方法应用于AI系统的五个主要挑战。针对这五个挑战，我们制定了三个设计和验证原则，为应对这一挑战提供了希望。的边缘图3显示这些原则之间的依赖关系。例如，运行时保证依赖于自省和数据驱动的环境建模来提取可监控的假设和环境模型。类似地，为了执行系统级分析，我们需要组合推理和抽象，其中一些AI组件可能需要挖掘规范，而其他组件则通过正式的归纳合成来正确生成。
自2016年本文最初版本发表以来，包括作者在内的几名研究人员一直在致力于应对这些挑战;介绍了几个先进的样品。我们开发了开源工具VerifAI6和风景,10基于本文所述原理的实现技术已应用于自动驾驶和航空航天领域的工业规模系统。这些结果只是一个开始，还有许多工作要做。经过验证的人工智能有望在未来几年继续成为一个富有成果的研究领域。
致谢
我们的工作得到了国家科学基金会(NSF)、国防高级研究计划局(DARPA)、半导体研究公司(SRC)和一些行业赞助商的部分支持。我们感谢许多与我们对话和合作的人，他们帮助塑造了这篇文章。
数字观看作者对这部作品的独家讨论通信视频。//www.eqigeno.com/videos/toward-verified-ai
参考文献
1.Censi, A.， Slutsky, K.， Wongpiromsarn, T.， Yershov, D.， Pendleton, S.， Fu, J.和Frazzoli, E.使用规则书的责任，道德和文化意识行为规范。在2019年实习生。机器人与自动化研讨会IEEE 8536 - 8542。
2.Cohen, j.m.， Rosenfeld, E.和Kolter, J.Z.通过随机平滑认证对抗鲁棒性。在36年会议纪要th实习生。关于机器学习的讨论(2019), 1310 - 1320。
3.Desai, A.， Ghosh, S.， Seshia, s.a.， Shankar, N.，和Tiwari, A. SOTER:为编程安全机器人系统的运行时保证框架。在IEEE /联合会实习。关于可靠的系统和网络，请确认(2019), 138 - 150。
4.Dietterich, T.G.和Horvitz, E.J.对人工智能的关注上升:反思和方向。ACM通信58， 10(2015)， 38-40。
5.Dreossi, T.， Donze, A.和Seshia, S.A.用机器学习组件组成伪造信息物理系统。在美国宇航局正式方法会议论文集(计算机科学讲义)10227(2017), 357 - 372。
6.Dreossi, T.， Fremont, d.j.， Ghosh, S.， Kim, E.， Ravanbakhsh, H.， Vazquez-Chanlatte, M.，和Seshia, S.A. VerifAI:一个用于基于人工智能系统的正式设计和分析的工具包。在31圣实习生。计算机辅助验证研讨会(计算机科学课堂讲稿)11561(2017), 432 - 442。
7.Dreossi, T.， Jha, S.和Seshia, S.A.语义对抗性深度学习。在30.th实习生。计算机辅助验证研讨会(计算机科学课堂讲稿)10981(2018), 3-26。
8.Fisac, J.F.等人。不确定机器人系统中基于学习控制的一般安全框架。IEEE自动控制汇刊， 7(2018)， 2737-2752。
9.Fremont, d.j.， Donzé， A.， Seshia, s.a.，和Wessel, D. Control improvisation。在35th软件技术与理论计算机科学基础年会(2015), 463 - 474。
10.Fremont, d.j.， Dreossi, T.， Ghosh, S.， Yue, X.， Sangiovanni-Vincentelli, a.l.和Seshia, S.A.风景:场景说明和场景生成的语言。在40周年会议的会议记录th关于程序设计语言设计与实现的ACM年度SIGPLAN会议(2019)。
11.Garcia, J.和Fernández, F.关于安全强化学习的全面调查。16 .机器学习研究， 1(2015)， 1437-1480。
12.Gehr, T.， Mirman, M.， Drachsler-Cohen, D.， Tsankov, P.， Chaudhuri, S.，和Vechev, M. AI2:具有抽象解释的神经网络的安全性和鲁棒性认证。在IEEE安全与隐私研讨会(2018), 3-18。
13.Goodfellow, I.， McDaniel, P.和Papernot, N.使机器学习在对抗输入时具有鲁棒性。ACM的通信61， 7(2018)， 56-66。
14.黄晓明，Kwiatkowska, M.，王硕，Wu, M.深度神经网络的安全性验证。在实习生。关于计算机辅助验证的确认，施普林格，(2017)，3-29。
15.在强化学习中，奖励机制在高级任务规范和分解中的应用。实习生。机器学习(2018), 2107 - 2116。
16.Jha, S.， Sahai, T.， Raman, V.， Pinto, A.和Francis, M.使用学习稀疏布尔公式的有效方法解释AI决策。63 .选j， 4(2019)， 1055-1075。
17.Li, W.， Sadigh, D.， Sastry, s.s.，和Seshia, S.A.人在回路控制系统的合成。在20个会议的会议记录th实习生。关于构建和分析系统的工具和算法(2014), 470 - 484。
18.刘，C.等。用于验证深度神经网络的算法。优化的基础和趋势， 3-4(2021)， 244-404。
19.Meel, K.S.等人。约束抽样和计数:通用哈希满足SAT求解。在除了NP, 2016年AAAI研讨会的论文(2016年2月12日)。
20.Milch, B.， Marthi, B.， Russell, S.， Sontag, D.， Ong, d.l.和Kolobov, A. BLOG:未知对象的概率模型。统计关系学习(2007), 373。
21.Mitchell, t.m.， Keller, r.m.和Kedar-Cabelli, S.T.，基于解释的概括:一个统一的观点。机器学习1， 1(1986)， 47-80。
22.Nghiem, T.等人。非线性混合系统时间特性证伪的蒙特卡洛技术。在13年的会议记录thACM实习生。混合系统:计算与控制(2010), 211 - 220。
23.美国计算机学会嵌入式计算系统学报1，(2019年1月)。
24.因果推理的七个工具，以及对机器学习的反思。ACM的通信， 3(2019)， 54-60。
25.Puggelli, A.， Li, W.， Sangiovanni-Vincentelli, A. l .，和Seshia, S.A.。带有凸不确定性的MDPs的PCTL性质的多项式时间验证。在25年的会议记录th实习生。关于计算机辅助验证的确认(2013)。
26.Russell, S.J.和Norvig, P。人工智能:现代方法。普伦蒂斯霍尔(2010)。
27.Sadigh, D.等。数据驱动的人类驾驶员行为概率建模与验证。在人机系统的形式化验证与建模，学术研讨会(2014)。
28.Sadigh, D.，萨斯特里，塞希亚，s.a.，和Dragan，公元。在IEEE/RSJ实习生会议论文集。关于智能机器人和系统的讨论(2016)。
29.Selsam, D.， Liang, P.和Dill, D. l .用形式数学开发无bug的机器学习系统。在34年会议纪要th实习生。机器学习70(2017), 3047 - 3056。
30.结合用于验证和综合的归纳、演绎和结构。在IEEE 103论文集， 11(2015)， 2036-2051。
31.自省环境建模。19th实习生。在运行时验证上确认(2019), 15-26。
32.Seshia, S.A.等人。深度神经网络的形式化规范。在《实习生录》。计算机协会。验证和分析自动化技术(2018), 20 - 34。
33.用简单来控制复杂。IEEE软件18， 4(2001)， 20-28。
34.Shoukry, Y.等人。SMC:可满足模凸优化。在十届会议的会议记录th实习生。混合系统:计算与控制(2017)。
35.Tomlin, C.， Mitchell, I.， Bayen, a.m.和Oishi, M.验证混合系统的计算技术。在IEEE 91会议论文集， 7(2003)， 986-1001。
36.Tran H-D。，Xiang, W., and Johnson, T.T. Verification approaches for learning-enabled autonomous cyber-physical systems.IEEE设计与测试(2020年8月)。https://doi.org/10.1109/MDAT.2020.3015712．
37.Vazquez-Chanlatte, M.， Jha, S.， Tiwari, A.， Ho, m.k.，和Seshia, S.A.学习任务规格从演示。在神经信息处理系统研究进展(2018), 5372 - 5382。
38.对形式方法的介绍。IEEE计算机23， 9(1990年9月)，8-24。
39.值得信赖的人工智能。ACM通信64， 10(2021)， 64-71。
40.徐军，张志刚，梁永强，张志刚，一种基于符号知识的深度学习语义损失函数。在35年的会议记录th实习生。机器学习(2018), 5498 - 5507。
脚注
a.本文第一版于2016年7月在arXiv上发布，以响应2016 CMU AI安全与控制研讨会白皮书征集活动。此后已经完成了两次修订。这一最新版本反映了作者对经过验证的人工智能的观点的演变。自2016年以来，有关这一主题的文献大幅增长;然而,每通信我们的指南仅限于40篇参考文献，因此对该主题的全面调查超出了范围。
本作品授权于数字图书馆是由计算机协会出版的。版权所有©2022 ACM股份有限公司
没有发现记录