迈向可验证的AI：形式化方法的五大挑战

作者 | Sanjit A. Seshia, Dorsa Sadigh, S. Shankar Sastry

编译 | 李梅、黄楠

编辑 | 陈彩娴

人工智能试图模仿人类智能的计算系统，包括人类一些与智能具有直观联系的功能，例如学习、解决问题以及理性地思考和行动。在广义地解释上，AI 一词涵盖了许多密切相关的领域如机器学习。那些大量使用 AI 的系统在医疗保健、交通运输、金融、社交网络、电子商务和教育等领域都产生了重大的社会影响。

这种日益增长的社会影响，也带来了一系列风险和担忧，包括人工智能软件中的错误、网络攻击和人工智能系统安全等方面。因此，AI 系统的验证问题以及更广泛的可信 AI 的话题已经开始引起研究界的关注。“可验证 AI”已经被确立为设计 AI 系统的目标，一个可验证的 AI 系统在特定的数学要求上具有强大的、理想情况下可证明的正确性保证。我们怎样才能实现这个目标？

最近，《ACM 通讯》（The Communications of ACM）上的一篇综述文章，试图从形式验证的角度来思考可证验 AI 面临的挑战，并给出了一些原则性的解决方案。文章作者是加州伯克利分校电气工程与计算机科学系的主任 S. Shankar Sastry 和 Sanjit A. Seshia 教授，以及斯坦福大学计算机科学系助理教授 Dorsa Sadigh。

在计算机科学和工程领域，形式方法涉及系统的严格的数学规范、设计和验证。其核心在于，形式方法是关于证明的：制定形成证明义务的规范，设计系统以履行这些义务，并通过算法证明搜索来验证系统确实符合其规范。从规范驱动的测试和仿真到模型检查和定理证明，一系列的形式化方法常被用于集成电路的计算机辅助设计，并已广泛被用于发现软件中的错误，分析网络物理系统，并发现安全漏洞。

本文回顾了形式化方法传统的应用方式，指明了形式化方法在 AI 系统中的五个独特挑战，包括：

• 开发关于环境的语言、算法

• 对复杂 ML 组件和系统进行抽象和表示

• 为 AI 系统和数据提出新的规范形式化方法和属性

• 开发针对自动推理的可扩展计算引擎

• 开发针对建构中可信（trustworthy-by-construction）设计的算法和技术

在讨论最新进展的基础上，作者提出了解决以上挑战的原则。本文不仅仅关注特定类型的 AI 组件如深度神经网络，或特定的方法如强化学习，而是试图涵盖更广泛的 AI 系统及其设计过程。此外，形式化方法只是通往可信 AI 的其中一种途径，所以本文的观点旨在对来自其他领域的方法加以补充。这些观点很大程度上来源于对自主和半自主系统中使用 AI 所产生的问题的思考，在这些系统中，安全性和验证性问题更加突出。

1 概述

图 1 显示了形式验证、形式综合和形式指导的运行时弹性的典型过程。形式验证过程从三个输入开始：

图 1 ：用于验证、综合和运行时弹性的形式化方法

1. 要验证的系统模型 S

2. 环境模型 E

3. 待验证的属性 Φ

验证者生成“是”或“否”的答案作为输出，来表明 S 是否满足环境 E 中的属性 Φ。通常，“否”输出伴随着反例，也称为错误跟踪（error trace），它是对系统的执行，表明 Φ 是如何被伪造的。一些验证工具还包括带有“是”答案的正确性证明或证书。我们对形式方法采取一种广泛的视角，包括使用形式规范、验证或综合的某些方面的任何技术。例如，我们囊括了基于仿真的硬件验证方法或基于模型的软件测试方法，因为它们也使用正式的规范或模型来指导仿真或测试的过程。

要将形式验证应用于 AI 系统，必须能够以形式来表示至少 S、E 和 Φ 这三个输入，理想情况下，会存在有效的决策程序来回答先前所描述的“是/否”问题。然而，即使要对三个输入构建良好的表示，也并不是一件简单的事，更不用说处理底层设计和验证问题的复杂性了。

我们这里通过半自动驾驶领域的示例来说明本文的观点。图 2 显示了一个 AI 系统的说明性示例：一个闭环 CPS，包括一辆带有机器学习组件的半自动车辆及其环境。具体来说，假设半自动的“自我”（ego）车辆有一个自动紧急制动系统 (AEBS)，该系统试图对前方的物体进行检测和分类，并在需要避免碰撞时启动制动器。图 2 中，一个 AEBS 包括一个由控制器（自动制动）、一个受控对象（受控的车辆子系统，包括自主堆栈的其他部分）和一个传感器（摄像头），以及一个使用 DNN 的感知组件。AEBS 与车辆环境相结合，形成一个闭环 CPS。“自我”车辆的环境包括车辆外部（其他车辆、行人等）以及车辆内部（例如驾驶员）的代理和对象。这种闭环系统的安全要求可以非形式地刻画为以一种属性，即在移动的“自我”车辆与道路上的任何其他代理或物体之间保持安全距离。然而，这种系统在规范、建模和验证方面存在许多细微差别。

图 2：包含机器学习组件的闭环 CPS 示例

第一，考虑对半自动车辆的环境进行建模。即使是环境中有多少和哪些代理（包括人类和非人类）这样的问题，也可能存在相当大的不确定性，更不用说它们的属性和行为了。第二，使用 AI 或 ML 的感知任务即使不是不可能，也很难形式化地加以规定。第三，诸如 DNN 之类的组件可能是在复杂、高维输入空间上运行的复杂、高维对象。因此，在生成形式验证过程的三个输入 S、E、Φ 时，即便采用一种能够使验证易于处理的形式，也十分具有挑战性。

如果有人解决了这个问题，那就会面临一项艰巨的任务，即验证一个如图 2 那样复杂的基于 AI 的 CPS。在这样的 CPS 中，组合（模块化）方法对于可扩展性来说至关重要，但它会由于组合规范的难度之类的因素而难以实施。最后，建构中修正的方法（correct-by-construction,CBC）有望实现可验证 AI，但它还处于起步阶段，非常依赖于规范和验证方面的进步。图 3 总结了可验证 AI 的五个挑战性领域。对于每个领域，我们将目前有前景的方法提炼成克服挑战的三个原则，用节点表示。节点之间的边缘显示了可验证 AI 的哪些原则相互依赖，共同的依赖线程由单一颜色表示。下文将详细阐述这些挑战和相应的原则。

图 3：可验证 AI 的 5 个挑战领域总结

2 环境建模

基于 AI/ML 的系统所运行的环境通常很复杂， 比如对自动驾驶汽车运行的各种城市交通环境的建模。事实上，AI/ML 经常被引入这些系统中以应对环境的复杂性和不确定性。当前的 ML 设计流程通常使用数据来隐性地规定环境。许多 AI 系统的目标是在其运行过程中发现并理解其环境，这与为先验指定的环境设计的传统系统不同。然而，所有形式验证和综合都与一个环境模型有关。因此，必须将有关输入数据的假设和属性解释到环境模型中。我们将这种二分法提炼为 AI 系统环境建模的三个挑战，并制定相应的原则来解决这些挑战。

2.1 建模不确定性

在形式验证的传统用法中，一种司空见惯的做法是将环境建模为受约束的非确定性过程，或者“干扰”。这种“过度近似”的环境建模能够允许人们更为保守地捕捉环境的不确定性，而无需过于详细的模型，这种模型的推理是很不高效的。然而，对于基于 AI 的自主性，纯粹的非确定性建模可能会产生太多虚假的错误报告，从而使验证过程在实践中变得毫无用处。例如在对一辆自动驾驶汽车的周围车辆行为的建模中，周围车辆的行为多种多样，如果采用纯粹的非确定性建模，就考虑不到总是意外发生的事故。此外，许多 AI/ML 系统隐式或显式地对来自环境的数据或行为做出分布假设，从而需要进行概率建模。由于很难准确地确定潜在的分布，所以不能假定生成的概率模型是完美的，并且必须在模型本身中对建模过程中的不确定性加以表征。

概率形式建模。为了应对这一挑战，我们建议使用结合概率建模和非确定性建模的形式。在能够可靠地指定或估计概率分布的情况下，可以使用概率建模。在其他情况下，非确定性建模可用于对环境行为进行过度近似。虽然诸如马尔可夫决策过程之类的形式主义已经提供了一种混合概率和非确定性的方法，但我们相信，更丰富的形式主义如概率规划范式，可以提供一种更具表达力和程序化的方式来对环境进行建模。我们预测，在许多情况下，此类概率程序需要（部分地）从数据中进行学习或合成。此时，学习参数中的任何不确定性都必须传播到系统的其余部分，并在概率模型中加以表示。例如，凸马尔可夫决策过程提供了一种方法来表示学习转变概率值的不确定性，并扩展了用于验证和控制的算法来解释这种不确定性。

2.2 未知的变量

在传统的形式验证领域如验证设备驱动程序中，系统 S 与其环境 E 之间的接口定义良好，E 只能通过该接口与 S 进行交互。对于基于 AI 的自主性而言，该接口是不完善的，它由传感器和感知组件规定，这些组件只能部分且嘈杂地捕捉环境，而且无法捕捕捉 S 和 E 之间的所有交互。所有环境的变量（特征）都是已知的，更不用说被感知到的变量。即使在环境变量已知的受限场景中，也明显缺乏有关其演变的信息，尤其是在设计的时候。此外，代表环境接口的激光雷达等传感器建模也是一项重大的技术挑战。

内省环境建模。我们建议通过开发内省的设计和验证方法来解决这个问题，也就是说，在系统 S 中进行内省，来对关于环境 E 的假设 A 进行算法上的识别，该假设足以保证满足规范 Φ。理想情况下，A 必须是此类假设中最弱的一个，并且还必须足够高效，以便在设计时生成、并在运行时监控可用传感器和有关环境的其他信息源，以及方便在假设被违反时可以采取缓解措施。此外，如果涉及人类操作员，人们可能希望 A 可以翻译成可理解的解释，也就是说 S 可以向人类“解释”为什么它可能无法满足规范 Φ。处理这些多重要求以及对良好传感器模型的需求，使得内省环境建模成为一个非常重要的问题。初步的工作表明，这种可监控假设的提取在简单的情况下是可行的，虽然需要做更多的工作才能让它具有实用性。

2.3 模拟人类行为

对于许多 AI 系统，例如半自动驾驶汽车，人类代理是环境和系统的关键部分。关于人类的人工模型无法充分捕捉人类行为的可变性和不确定性。另一方面，用于建模人类行为的数据驱动方法可能对 ML 模型使用的特征的表达能力和数据质量敏感。为了实现人类 AI 系统的高度保证，我们必须解决当前人类建模技术的局限性，并为其预测准确性和收敛性提供保障。

主动的数据驱动建模。我们相信，人类建模需要一种主动的数据驱动方法，模型结构和以数学形式表示的特征适合使用形式方法。人类建模的一个关键部分是捕捉人类意图。我们提出了一个三管齐下的方法：基于专家知识来定义模型的模板或特征，用离线学习来完成模型以供设计时使用，以及在运行时通过监控和与环境交互来学习和更新环境模型。例如，已经有研究表明，通过人类受试者实验从驾驶模拟器收集的数据，可用于生成人类驾驶员的行为模型，这些模型可用于验证和控制自动驾驶汽车。此外，计算机安全领域的对抗性训练和攻击技术可用于人类模型的主动学习，并可针对导致不安全行为的特定人类动作来进一步设计模型。这些技术可以帮助开发 human-AI 系统的验证算法。

3 形式化规范

形式化验证严重依赖于形式化规范——即对系统应该做什么的精确的数学陈述。即使在形式化方法已经取得相当大成功的领域，提出高质量的形式化规范也是一项挑战，而 AI 系统尤其面临着独特的挑战。

3.1 难以形式化的任务

图 2 中 AEBS 控制器中的感知模块必须检测和分类对象，从而将车辆和行人与其他实体区分开来。在经典的形式方法意义上，这个模块的准确性要求对每种类型的道路使用者和对象进行形式定义，这是极其困难的。这种问题存在于这个感知模块的所有实现中，而不仅仅出现在基于深度学习的方法中。其他涉及感知和交流的任务也会出现类似的问题，比如自然语言处理。那么，我们如何为这样的模块指定精度属性呢？规范语言应该是什么？我们可以使用哪些工具来构建规范？

端到端/系统水平的规范（End-to-end/system-level specifications）。为了应对上述挑战，我们可以对这个问题稍加变通。与其直接对难以形式化的任务进行规范，不如首先专注于精确地指定 AI 系统的端到端行为。从这种系统水平的规范中，可以获得对难以形式化的组件的输入-输出接口的约束。这些约束用作一个组件水平（component-level ）的规范，这个规范与整个 AI 系统的上下文相关。对于图 2 中的 AEBS 示例，这涉及对属性 Φ 的规定，该属性即在运动过程中与任何对象都保持最小距离，从中我们可得出对 DNN 输入空间的约束，在对抗分析中捕捉语义上有意义的输入空间。

3.2 定量规范 vs. 布尔规范

传统上，形式规范往往是布尔型的，它将给定的系统行为映射为“真”或“假”。然而，在 AI 和 ML 中，规范通常作为规范成本或奖励的目标函数给出。此外，可能有多个目标，其中一些必须一起满足，而另一些则可能需要在某些环境中相互权衡。统一布尔和定量两种规范方法的最佳方式是什么？是否有能够统一捕捉 AI 组件常见属性（如鲁棒性和公平性）的形式？

混合定量和布尔规范。布尔规范和定量规范都有其优点：布尔规范更容易组合，但目标函数有助于用基于优化的技术进行验证和综合，并定义更精细的属性满足粒度。弥补这一差距的一种方法是转向定量规范语言，例如使用具有布尔和定量语义的逻辑（如度量时序逻辑），或将自动机与 RL 的奖励函数相结合。另一种方法是将布尔和定量规范组合成一个通用的规范结构，例如一本规则手册 ，手册中的规范可以按层次结构进行组织、比较和汇总。有研究已经确定了 AI 系统的几类属性，包括鲁棒性、公平性、隐私性、问责性和透明度。研究者正在提出新的形式主义，将形式方法和 ML 的思想联系起来，以对这些属性的变体（如语义鲁棒性）进行建模。

3.3 数据 vs. 形式要求

“数据即规范”的观点在机器学习中很常见。有限输入集上标记的“真实”数据通常是关于正确行为的唯一规范。这与形式化方法非常不同，形式化方法通常以逻辑或自动机的形式给出，它定义了遍历所有可能输入的正确行为的集合。数据和规范之间的差距值得注意，尤其是当数据有限、有偏见或来自非专家时。我们需要技术来对数据的属性进行形式化，包括在设计时可用的数据和尚未遇到的数据。

规范挖掘(Specification mining)。 为了弥合数据和形式规范之间的差距，我们建议使用算法从数据和其他观察中来推断规范——即所谓的规范挖掘技术。此类方法通常可用于 ML 组件，包括感知组件，因为在许多情况下，它不需要具有精确的规范或人类可读的规范。我们还可以使用规范挖掘方法，从演示或更复杂的多个代理（人类和人工智能）之间的交互形式来推断人类意图和其他属性。

4 学习系统的建模

在形式验证的大多数传统应用中，系统 S 在设计时是固定的且已知的，比如它可以是一个程序，或者一个用编程语言或硬件描述语言来描述的电路。系统建模问题主要涉及的，是通过抽象掉不相关的细节，来将 S 减小到更易于处理的大小。AI 系统给系统建模带来了非常不同的挑战，这主要源于机器学习的使用：

高维输入空间

用于感知的 ML 组件通常在非常高维的输入空间上运行。比如，一个输入的RGB 图像可以是 1000 x 600 像素，它包含256((1000x600x3)) 个元素，输入通常就是这样的高维向量流。尽管研究人员已经对高维输入空间（如在数字电路中）使用了形式化方法，但基于 ML 的感知输入空间的性质是不同的，它不完全是布尔值，而是混合的，包括离散变量和连续变量。

高维参数/状态空间

深度神经网络等 ML 组件具有数千到数百万个模型参数和原始组件。例如，图 2 中使用的最先进的 DNN 有多达 6000 万个参数和数十层组件。这就产生了巨大的验证搜索空间，抽象过程需要非常仔细。

在线适应和进化

一些学习系统如使用 RL 的机器人，会随着它们遇到的新数据和新情况而发生进化。对于这样的系统，设计时的验证必须考虑系统行为的未来演变，或者随着学习系统的发展逐步地在线执行。

在上下文中建模系统

对于许多 AI/ML 组件，它们的规范仅仅由上下文来定义。例如，要验证图 2 中基于 DNN 的系统的安全性，就需要对环境进行建模。我们需要对 ML 组件及其上下文进行建模的技术，以便可以验证在语义上有意义的属性。

近年来，许多工作都专注于提高效率，来验证 DNN 的鲁棒性和输入-输出属性。然而，这还不够，我们还需要在以下三个方面取得进展：

自动抽象和高效表示

自动生成系统的抽象一直是形式方法的关键，它在将形式方法的范围扩展到大型硬件和软件系统方面发挥着至关重要的作用。为了解决基于 ML 的系统的超高维混合状态空间和输入空间方面的挑战，我们需要开发有效的技术来将 ML 模型抽象为更易于形式分析的、更简单的模型。一些有希望的方向包括：使用抽象解释来分析 DNN，开发用于伪造有 ML 组件的网络物理系统的抽象，以及设计用于验证的新表示（比如星集）。

解释与因果

如果学习者在其预测中附上关于预测是如何从数据和背景知识中产生的的解释，那我们就可以简化对学习系统进行建模的任务。这个想法并不新鲜，ML 社区已经对诸如“基于解释的泛化”等术语进行了研究，但是最近，人们正在对使用逻辑来解释学习系统的输出重新产生了兴趣。解释生成有助于在设计时调试设计和规范，并有助于合成鲁棒的 AI 系统以在运行时提供保障。包含因果推理和反事实推理的 ML 还可以帮助生成用于形式方法的解释。

语义特征空间

当生成的对抗性输入和反例在所使用的 ML 模型的上下文中具有语义意义时，ML 模型的对抗性分析和形式验证就更有意义。例如，针对汽车颜色或一天中时间的微小变化来分析 DNN 对象检测器的技术，比向少量任意选择的像素添加噪声的技术更有用。当前，大多数的方法在这一点上都还达不到要求。我们需要语义对抗分析，即在ML 模型所属系统的上下文中对它们进行分析。其中额的一个关键步骤，是表示对 ML 系统运行的环境建模的语义特征空间，而不是为 ML 模型定义输入空间的具体特征空间。这是符合直觉的，即与完整的具体特征空间相比，具体特征空间在语义上有意义的部分（如交通场景图像）所形成的潜在空间要低得多。图 2 中的语义特征空间是代表自动驾驶汽车周围 3D 世界的低维空间，而具体的特征空间是高维像素空间。由于语义特征空间的维数较低，因此可以更容易地进行搜索。但是，我们还需要一个“渲染器”，将语义特征空间中的一个点映射到具体特征空间中的一个点。渲染器的属性如可微性（differentiability），可以更容易地应用形式化方法来执行语义特征空间的目标导向搜索。

5 用于设计和验证的计算引擎

硬件和软件系统形式化方法的有效性，是由底层“计算引擎”的进步推动的——例如，布尔可满足性求解 (SAT)、可满足性模理论 (SMT) 和模型检查。鉴于 AI/ML 系统规模、环境复杂性和所涉及的新型规范，需要一类新的计算引擎来进行高效且可扩展的训练、测试、设计和验证，实现这些进步必须克服的关键挑战。

5.1 数据集设计

数据是机器学习的基本起点，提高 ML 系统质量就必须提高它所学习数据的质量。形式化方法如何帮助 ML 数据系统地选择、设计和扩充？

ML 的数据生成与硬件和软件的测试生成问题有相似之处。形式化方法已被证明对系统的、基于约束的测试生成是有效的，但这与对人工智能系统的要求不同，约束类型可能要复杂得多——例如，对使用传感器从复杂环境（如交通状况）捕获的数据的“真实性”进行编码要求。我们不仅需要生成具有特定特征的数据项（如发现错误的测试），还需要生成满足分布约束的集合；数据生成必须满足数据集大小和多样性的目标，以进行有效的训练和泛化。这些要求都需要开发一套新的形式化技术。

形式方法中的受控随机化。数据集设计的这个问题有很多方面，首先必须定义“合法”输入的空间，以便根据应用程序语义正确形成示例；其次，需要捕获与现实世界数据相似性度量的约束；第三，通常需要对生成的示例的分布进行约束，以获得学习算法收敛到真实概念的保证。

我们相信这些方面可以通过随机形式方法来解决——用于生成受形式约束和分布要求的数据的随机算法。一类称为控制即兴创作的新技术是很有前景的，即兴创作的生成要满足三个约束的随机字符串（示例）x：

• 定义合法x空间的硬约束

• 一个软约束，定义生成的x必须如何与真实世界的示例相似

• 定义输出分布约束的随机性要求

目前，控制即兴理论仍处于起步阶段，我们才刚刚开始了解计算复杂性并设计有效的算法。反过来，即兴创作依赖于计算问题的最新进展，例如约束随机抽样、模型计数和基于概率编程的生成方法。

5.2 定量验证

除了通过传统指标（状态空间维度、组件数量等）衡量AI 系统规模之外，组件的类型可能要复杂得多。例如，自主和半自主车辆及其控制器必须建模为混合动力系统，结合离散和连续动力学；此外，环境中的代表（人类、其他车辆）可能需要建模为概率过程。最后，需求可能不仅涉及传统关于安全性和活性的布尔规范，还包括对系统鲁棒性和性能的定量要求，然而大多数现有的验证方法，都是针对回答布尔验证问题。为了解决这一差距，必须开发用于定量验证的新可扩展引擎。

定量语义分析。一般来说，人工智能系统的复杂性和异构性意味着，规范的形式验证（布尔或定量）是不可判定的——例如，即便是确定线性混合系统的状态是否可达，也是不可判定的。为了克服计算复杂性带来的这一障碍，人们必须在语义特征空间上使用概率和定量验证的新技术，以增强本节前面讨论的抽象和建模方法。对于同时具有布尔和定量语义的规范形式，在诸如度量时间逻辑之类的形式中，将验证表述为优化，对于统一来自形式方法的计算方法和来自优化文献的计算方法至关重要。例如在基于模拟的时间逻辑证伪中，尽管它们必须应用于语义特征空间以提高效率，这种伪造技术也可用于系统地、对抗性地生成 ML 组件的训练数据。概率验证的技术应该超越传统的形式，如马尔科夫链或MDPs，以验证语义特征空间上的概率程序。同样，关于SMT求解的工作必须扩展到更有效地处理成本约束--换句话说，将SMT求解与优化方法相结合。

我们需要了解在设计时可以保证什么，设计过程如何有助于运行时的安全操作，以及设计时和运行时技术如何有效地互操作。

5.3 AI/ML 的组合推理

对于扩展到大型系统的正式方法，组合（模块化）推理是必不可少的。在组合验证中，一个大型系统（例如，程序）被拆分为它的组件（例如，程序），每个组件都根据规范进行验证，然后组件规范一起产生系统级规范。组合验证的一个常见方法是使用假设-保证合同，例如一个过程假设一些关于它的开始状态（前置条件），反过来又保证其结束状态（后置条件），类似的假设-保证范式已被开发并应用于并发的软件和硬件系统。

然而，这些范式并不涵盖人工智能系统，这在很大程度上是由于 "形式化规范 "一节中讨论的人工智能系统的规范化挑战。组合式验证需要组合式规范——也就是说，组件必须是可形式化的。然而，正如“形式化规范”中所述，可能无法正式指定一个感知组件的正确行为。因此，挑战之一就是开发不依赖于有完整组合规范的组合推理技术。此外，人工智能系统的定量和概率性质，要求将组合推理的理论扩展到定量系统和规范。

推断组件合同。人工智能系统的组合式设计和分析需要在多个方面取得进展。首先，需要在一些有前景的初步工作基础上，为这些系统的语义空间开发概率保证设计和验证的理论。第二，必须设计出新的归纳综合技术，以算法方式生成假设-保证合同，减少规范负担并促进组合推理。第三，为了处理诸如感知等没有精确正式规格的组件的情况，我们提出了从系统级分析中推断组件级约束的技术，并使用这种约束将组件级分析，包括对抗性分析，集中在搜索输入空间的 "相关 "部分。

6 建构中修正智能系统

在理想的世界中，验证将与设计过程相结合，因此系统是“在建构中修正的”。例如，验证可以与编译/合成步骤交错进行，假设在集成电路中常见的寄存器传输级（RTL）设计流程中，或许它可以被集成到合成算法中，以确保实现满足规范。我们能不能为人工智能系统设计一个合适的在建构中逐步修正的设计流程？

6.1 ML 组件的规范驱动设计

给定一个正式的规范，我们能否设计一个可证明满足该规范的机器学习组件（模型）？这种全新的 ML 组件设计有很多方面：（1）设计数据集，（2） 综合模型的结构，（3）生成一组有代表性的特征，（4） 综合超参数和 ML 算法选择的其他方面，以及（5）在综合失败时自动化调试 ML 模型或规范的技术。

ML 组件的正式合成。解决前面所列出一些问题的解决方案正在出现，可以使用语义损失函数或通过认证的鲁棒性在 ML 模型上强制执行属性，这些技术可以与神经架构搜索等方法相结合，以生成正确构建的 DNN。另一种方法是基于新兴的形式归纳综合理论，即从满足形式化规范的程序实例中进行综合。解决形式归纳综合问题的最常见方法是使用 oracle-guided 方法，其中将学习者与回答查询的 oracle 配对；如示例中图2，oracle 可以是一个伪造者，它生成反例，显示学习组件的故障如何违反系统级规范。最后，使用定理证明来确保用于训练 ML 模型的算法的正确性，也是朝着建构修正的 ML 组件迈出的重要一步。

6.2 基于机器学习的系统设计

第二个挑战，是设计一个包含学习和非学习组件的整体系统。目前已经出现的几个研究问题：我们能否计算出可以限制 ML 组件运行的安全范围？我们能否设计一种控制或规划算法来克服它接收输入的基于 ML 感知组件的限制？我们可以为人工智能系统设计组合设计理论吗？当两个 ML 模型用于感知两种不同类型的传感器数据（例如，LiDAR 和视觉图像），并且每个模型在某些假设下都满足其规范，那么二者在什么条件下可以一起使用、以提高可靠性整体系统？

在这一挑战上，取得进展的一个突出例子是基于安全学习的控制的工作。这种方法预先计算了一个安全包络线，并使用学习算法在该包络线内调整控制器，需要基于例如可达性分析、来有效计算此类安全包络的技术；同样，安全 RL 领域也取得了显着进展。

然而，这些并没有完全解决机器学习对感知和预测带来的挑战——例如，可证明安全的端到端深度强化学习尚未实现。

6.3 为弹性 AI 桥接设计时间和运行时间

正如“环境建模”部分所讨论的那样，许多 AI 系统在无法先验指定的环境中运行，因此总会有无法保证正确性的环境。在运行时实现容错和错误恢复的技术，对人工智能系统具有重要作用。我们需要系统地理解在设计时可以保证什么，设计过程如何有助于人工智能系统在运行时的安全和正确运行，以及设计时和运行时技术如何有效地互操作。

对此，关于容错和可靠系统的文献为我们提供了开发运行时保证技术的基础——即运行时验证和缓解技术；例如 Simplex 方法，就提供了一种将复杂但容易出错的模块与安全的、正式验证的备份模块相结合的方法。最近，结合设计时和运行时保证方法的技术显示了未验证的组件、包括那些基于人工智能和 ML 的组件，可以被包裹在运行时保证框架中，以提供安全运行的保证。但目前这些仅限于特定类别的系统，或者它们需要手动设计运行时监视器和缓解策略，在诸如内省环境建模、人工智能的监测器和安全回退策略的合成等方法上，还有更多的工作需要做。

此处讨论的建构中修正智能系统的设计方法可能会引入开销，使其更难以满足性能和实时要求。但我们相信（也许是非直觉的），在以下意义上，形式化方法甚至可以帮助提高系统的性能或能源效率。

传统的性能调优往往与上下文无关——例如，任务需要独立于它们运行的环境来满足最后期限。但如果设计时就对这些环境进行正式表征，并在运行时对其进行监控，如果其系统运行经过正式验证是安全的，那么在这种环境下，ML 模型就可以用准确性来换取更高的效率。这种权衡可能是未来研究的一个富有成果的领域。

7 结论

从形式化方法的角度来看，我们剖析了设计高保证人工智能系统的问题。如图3所示，我们确定了将形式化方法应用于 AI 系统的五个主要挑战，并对这五项挑战中的每一项都制定了三项设计和验证原则，这些原则有希望解决这个挑战。

图 3 中的边显示了这些原则之间的依赖关系，例如运行时保证依赖于自省和数据驱动的环境建模，以提取可监测的假设和环境模型。同样，为了进行系统级分析，我们需要进行组合推理和抽象，其中一些 AI 组件可能需要挖掘规范，而其他组件则通过形式化的归纳综合构建生成正确的结构。

自 2016 年以来，包括作者在内的几位研究人员一直致力于应对这些挑战，当时本文已发表的原始版本介绍了一些样本进展。我们已经开发了开源工具 VerifAI 和 Scenic，它们实现了基于本文所述原则的技术，并已应用于自动驾驶和航空航天领域的工业规模系统。这些成果只是一个开始，还有很多事情要做。在未来的几年里，可验证 AI 有望继续成为一个富有成效的研究领域。