走向可验证的人工智能：形式方法的五大挑战

本文约10500字，建议阅读20分钟，本文回顾了形式化方法的传统应用方式，给出了形式化方法在AI系统中的五个独特挑战。

人工智能试图模仿人类智能的计算系统，包括学习、解决问题、理性思考和行为等与人类智能直观相关的功能。

从广义上来说，AI一词涵盖了机器学习等密切相关的许多领域。

大量使用AI的系统在医疗、交通运输、金融、社交网络、电子商务、教育等领域产生了巨大的社会影响。

这种日益增长的社会影响带来了一系列的风险和担忧，包括人工智能软件中的错误、网络攻击和人工智能系统的安全。

因此，AI系统的验证问题以及更广泛的可信AI话题开始引起研究界的关注。

“可验证AI”已被确立为设计AI系统的目标，可验证AI系统对特定数学要求具有强大、理想的可证明准确性保证。

怎样才能实现这个目标？ 最近，在《ACM 通讯》 ( thecommunicationsofacm )上刊登的综述文章，从形式验证的角度来考虑可验证的AI所面临的课题，试图提出几个原则上的解决方案。

作者是加州伯克利分校电气工程与计算机科学系主任S. Shankar Sastry和Sanjit A. Seshia教授、斯坦福大学计算机科学系助理教授Dorsa Sadigh。

在计算机科学和工程领域，形式方法涉及系统的严格数学规范、设计和验证。

其核心是形式方法涉及证明。 制定形成证明义务的规范，设计系统以履行这些义务，通过算法证明检索验证系统确实符合该规范。

从规范驱动的测试和仿真到模型检验和定理证明，一系列形式化方法常用于集成电路的计算机辅助设计，广泛用于发现软件中的错误，分析网络物理系统，发现安全漏洞。

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

开发环境的语言、算法抽象出复杂的ML组件和系统，对AI系统和数据提出了新的规范形式化方法和属性，开发了用于自动推理的可扩展计算引擎，是构建中的可靠( trustworthy-by-construction )

本文试图涵盖更广泛的AI系统及其设计过程，而不仅仅关注特定类型的AI组件(如深度神经网络)或特定方法(如增强学习)。

另外，形式化方法只是通向可靠AI的途径之一，所以本文的观点以补充来自其他领域的方法为目的。

这些观点很大程度上源于对在自主和半自主系统中使用AI所产生的问题的思考，在这些系统中安全性和验证性问题更加突出。

摘要图1展示了执行形式验证、形式集成和形式指导时灵活性的典型过程。

格式验证过程从以下三个输入开始：

图1 :验证、集成和运行时灵活性的形式化方法

验证的系统模型s环境模型e验证的属性验证者生成“是”或“否”的回答作为输出，指示s是否满足环境e中的属性。

通常，“否”的输出伴随反例，也称为error trace，是表示是如何伪造的系统的执行。

一些验证工具还包括回答“是”的准确性证书或证书。

我们对形式方法有广泛的观点，包括使用形式规范、验证或综合的几个方面的技术。

例如，它还包括基于模拟的硬件验证方法和基于模型的软件测试方法。 这是为了使用正式的规格和模型来指导模拟和测试的过程。

要将形式验证应用于AI系统，至少需要能够以形式表示s、e、这3个输入，理想情况下存在回答上述yes/no问题的有效决策过程。

但是，即使试图为三个输入构建良好的显示，也不是一件简单的事情，更不用说处理基础设计和验证问题的复杂性了。

这里通过半自动驾驶领域的例子说明本文的观点。

图2显示了AI系统的一个示例。 闭环CPS，包括配备机器学习组件的半自动车辆及其环境。

具体来说，假设半自动的“自我”( ego )车辆有自动紧急制动系统( AEBS )，它能检测和分类前方物体，并在需要避免碰撞时启动制动器。

在图2中，AEBS包括使用DNN的感测组件(受控车辆子系统)和传感器(传感器)，该受控车辆子系统包括控制器(自动制动)和受控堆叠的其他部分。

ABS与车辆环境结合形成一个闭环CPS。

“自己”车辆环境包括车辆外部(其他车辆、行人等)和车辆内部(例如驾驶员)的代理和对象。

这种闭环系统的安全要求可以非形式地描绘为在移动的“自己”车辆与道路上的其他代理或物体之间保持安全距离的属性。

但是，这类系统在规范化、建模、验证方面存在许多微妙差异。

图2 )包含机器学习组件的闭环CPS的示例首先考虑对半自动车辆的环境进行建模。

无论是环境中有多少行为者和哪些行为者(包括人和非人)的问题，属性和行为都可能存在相当大的不确定性。

第二，使用AI和ML的感知任务即使不是不可能的，也很难在形式上规定。

第三，DNN等组件可能是在复杂的高维输入空间上运行的复杂的高维对象。

因此，在生成形式验证过程的3个输入s、e、时，即使采用使验证容易处理的形式，也非常困难。

如果有人解决了这个问题，就会面临验证如图2所示的复杂的基于AI的CPS的困难。

在这样的CPS中，为了扩展性，组合(模块化)方法很重要，但是由于组合规格的难度等因素，安装变得困难。

最后，构建中的修正方法( correct-by-construction，CBC )有望实现可验证的AI，但仍处于起步阶段，很大程度上依赖于规范和验证方面的进步。

图3总结了可以验证AI的五个挑战性领域。

对于各个领域，我们将目前有前途的方法提炼为克服挑战的三个原则，并用节点表示。

节点间的边缘表示可以验证AI的哪个原则是相互依存的，共同的依存线程用单一的颜色表示。

我将详细阐述这些挑战和相应的原则。

图3 :可验证ai的五个挑战领域总结

环境建模基于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系统的验证算法。

形式化规范的形式化验证很大程度上依赖于形式化规范——，即系统应该做什么的准确数学描述。

即使在形式化方法相当成功的领域，提出高质量的形式化规范也是一个挑战，AI系统面临着特别独特的挑战。

3.1难以形式化的任务图2的AEBS控制器的感知模块必须对对象进行检测和分类，从而将车辆和行人与其他实体区分开来。

从经典形式方法的意义上讲，要实现该模块的正确性，很难根据道路使用者和对象的种类进行形式定义。

这种问题不仅存在于基于深度学习的方法中，而且存在于该感知模块的所有实现中。

其他涉及感知和交流的任务，例如自然语言处理，也会出现同样的问题。

那么，如何为此类模块指定精度属性呢？ 规范语言是什么？ 可用于构建规范的工具是什么？ 端到端/系统级规范(端对端/系统级规范)。

为了应对这种挑战，我们可以在这个问题上做点变通。

与其直接规范不易形式化的任务，不如首先专注于准确指定AI系统的端到端行为。

从这样的系统级规格中，可以得到对难以形式化的组件的输入输出接口的制约。

这些约束被用作与整个AI系统上下文相关的组件级规范。

在图2的AEBS的例子中，关于运动中与任何对象保持最小距离的属性的规定，得到对DNN输入空间的制约，可以在对抗分析中捕捉意义上的输入空间。

3.2定量规范vs .布尔规范传统上，形式规范多为布尔型，它将给定的系统行为映射为“真”或“假”。

但是，在AI和ML中，规范通常是作为规范成本或报酬的目标函数给出的。

此外，可能有多个目标。 其中有些必须一起满足，有些环境需要权衡。

统一布尔和定量两种规范方法的最佳方法是什么？ 有统一捕捉鲁棒性和公平性等AI组件常见属性的形式吗？ 混合定量和布尔规范。

布尔规格和定量规格都有优点。 布尔规范易于组合，但目标函数通过基于优化的技术进行验证和集成，有助于定义更精细的属性以满足粒度。

填补这一差距的一种方法是转向定量规范语言，例如使用布尔和具有定量意义的逻辑(例如测量时间序列逻辑)，或结合机器人和RL的报酬函数。

另一种方法是将布尔和定量规范组合到一个通用的规范结构中。 例如，像规则手册一样，手册中的规范按层次结构进行组织、比较和总结。

一项研究确定了AI系统的若干属性，包括鲁棒性、公平性、隐私性、问责制和透明度。

研究人员结合形式方法和ML思想提出了一种新的形式主义，用于对语义鲁棒性等属性变体建模。

3.3数据vs .形式要求“数据即规范”的观点在机器学习中很常见。

标记在有限输入集中的“真”数据通常是正确行为的唯一规范。

这与形式化方法非常不同，形式化方法通常以逻辑或自动机的形式给出，定义所有可输入的正确行为的集合。

数据与规范之间的差距应特别关注数据有限、有偏见或来自非专业人士的情况。

需要用于格式化数据属性的技术，例如设计时可用的数据和尚未遇到的数据。

《规范挖掘》。

为了弥补数据与形式规范之间的差距，建议采用算法从数据和其他观察中推断规范——，即所谓的规范挖掘技术。

这种方法经常用于包含感知组件的ML组件中，因为它们通常不需要精确或人可读的规范。

它还可以使用规范挖掘方法，通过演示和更复杂的多个代理(人与人工智能)之间的交互来推断人的意图和其他属性。

学习系统的建模在形式验证的许多传统应用中，系统s在设计时是固定的，是已知的。 例如，它也可以是程序，也可以是用编程语言或硬件描述语言记述的电路。

系统建模问题主要涉及通过抽象无关细节，将s缩小到更容易处理的大小。

AI系统给系统建模带来了非常不同的挑战。 这主要来源于机器学习的使用。 用于感知高维输入空间的ML组件通常在非常高维的输入空间上工作。

例如，输入的RGB图像为1000 x 600像素，包含256((10006003) ) )的元素，输入通常就是这样的高维向量流。

研究者们在数字电路等高维输入空间中使用了形式化方法，但是基于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 )之类的渲染器属性，可以方便地应用形式化方法执行语义特征空间的面向目标搜索。

用于设计和验证的计算引擎软硬件系统形式化方法的有效性在于，由基础“计算引擎”的进步推动的——，例如布尔可满足性求解( SAT )、可满足性模型理论)、模型检查。

考虑到AI/ML系统的规模、环境复杂性和相关新规范，新计算机将进行高效、可扩展的培训、测试、设计和验证，以解决实现这些进步必须克服的关键挑战

5.1数据集设计数据是机器学习的基本起点，要提高ML系统的质量必须提高学习数据的质量。

形式化方法如何有助于ML数据的系统选择、设计和扩展？ ML的数据生成与软硬件测试生成问题相似。

形式化方法被证明对基于系统约束的测试生成是有效的，但这不同于对人工智能系统的要求，约束类型可能比——复杂得多。 例如，对使用传感器从交通状况等复杂环境中捕获的数据的“真实性”进行编码的要求。

除了生成具有特定特征的数据项(如发现错误的测试)外，还必须生成满足分布约束的集合。数据生成必须满足数据集大小和多样性的目标才能进行有效的训练和泛化。

这些要求都需要开发新的形式化技术。

用形式方法随机化控制。

数据集设计的这个问题有很多方面。 首先，必须定义“合法”的输入空间，以便根据APP语义正确形成示例。 其次，需要捕捉与现实世界数据的相似性测量的制约第三，为了得到学习算法收敛于真实概念的保证，通常需要制约生成的样本的分布。

认为这些方面可以以随机方式解决——用于生成形式约束和分布所要求的数据的随机算法。

被称为控制即兴创作新技术的类很有前途，即兴创作的生成需要满足3个条件的随机字符串(例) x :

定义合法x空间硬约束的软约束，定义生成的x必须如何与真实世界例子相似定义输出分布约束的随机性要求目前控制即兴理论还处于起步阶段，了解计算复杂性，设计有效算法才刚刚开始

相反，即兴创作取决于计算问题的最新进展，包括约束随机抽样、模型计数和基于概率编程的生成方法。

5.2定量验证除了用传统的指标(状态空间维度、组件数量等)来衡量AI系统的规模外，组件的类型可能要复杂得多。

例如，自主车辆和半自主车辆及其控制器应当建模为混合动力系统，并结合离散动力学和连续动力学； 此外，环境中的代表(人和其他车辆)可能需要作为概率过程进行建模。

最后，需求不仅包括传统的安全性和活性布尔规范，还可能包括对系统鲁棒性和性能的定量要求，但许多现有的验证方法都是对布尔验证问题的回答。

为了解决这一差距，需要开发用于定量验证的新的可扩展引擎。

定量语义分析。

一般地，人工智能系统的复杂性和异构性意味着规范的形式化验证(布尔或定量)是不可判定的，例如，即使确定线性混合系统的状态是否可能，也不可判定。

为了克服计算复杂性带来的这一障碍，为了强化本节中先前讨论的抽象和建模方法，有必要在语义特征空间中使用概率和定量验证的新技术。

对于布尔和具有定量意义的规范形式，以测量时间逻辑的形式将验证表现为最优化，对于统一形式方法的计算方法和最优化文献的计算方法是重要的。

例如，在基于模拟的时间逻辑证据的情况下，为了提高效率，有必要将其应用于语义特征空间，但这种伪造技术也可以用于系统且抵触地生成ML组件的训练数据。

概率验证技术应该超越马尔可夫链和MDPs等传统形式，验证语义特征空间上的概率过程。

同样，有关SMT解决方案的工作必须扩展，以更有效地处理成本限制。 这意味着SMT解决方案必须与优化方法相结合。

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

5.3 AI/ML的组合推理，在扩展到大系统的正式方法中，组合(模块化)推理是不可缺少的。

在组合验证中，大型系统(例如程序)被划分为其组件(例如程序)，每个组件根据规范进行验证，并与组件规范一起生成系统级规范。

组合验证的一种常用方法是使用假设-保证合同。 例如，进程就其开始状态(前置条件)而言，相反会保证其结束状态(后置条件)。 类似假设-保证范式已经开发并应用于并发的软件和硬件系统。

但是，这些范式并不涵盖人工智能系统，这在很大程度上是由于“形式化规范”一节中讨论的人工智能系统规范化的课题。

组合验证需要组合规格——。 这意味着组件必须是可形式化的。

然而，如“形式化规范”中所述，可能无法正式指定感知组件的正确行为。

因此，课题之一是开发不依赖于完整组合规范的组合推理技术。

此外，人工智能系统的定量和概率性质要求将组合推理的理论扩展到定量系统和规范。

推定汇编合同。

人工智能系统组合设计与分析需要在多方面取得进展。

首先，需要在一些有前景的初步工作的基础上为这些系统的语义空间开发概率保证设计和验证的理论。

第二，要设计新的归纳综合技术，以算法方式生成假设-保证合同，减少规范负担，促进组合推理。

第三，为了处理感知等没有正确正式规格的组件，提出了从系统级分析中推断组件级约束的技术，利用该约束将包括抗性分析在内的组件级分析集中在检索输入空间的“相关”部分。

在构建中修正智能系统的理想世界中，由于验证与设计过程相结合，系统“在构建过程中被修正”。

例如，验证可以与编译/合成步骤交互，如果集成电路中常见的RTL(registertransferlanguage )设计过程可以集成到合成算法中以确保满足规范

能否为人工智能系统设计在正确构建过程中逐步修改的设计流程？ 如果在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模型可以换取更高的效率，从而获得正确性。

这种权衡可能是未来研究成果的领域。

结论从形式化方法的角度，我们分析了设计高保障人工智能系统的问题。

如图3所示，我们确定了将形式化方法应用于AI系统的五个主要挑战，并针对这五个挑战分别制定了三个设计和验证原则。 这些原则希望解决这一挑战。

图3示出了这些原则之间的依赖关系，例如，为了提取可监视假设和环境模型，确保在运行时依赖于反射和数据驱动的环境建模。

同样，为了进行系统级分析，需要进行组合推理和抽象。 其中一些需要挖掘规范，而另一些则通过形式化的归纳集成构建生成正确的结构。

2016年以来，包括作者在内的几位研究人员致力于这些课题。 当时，本文发表的原始版本介绍了一些样本的进展。

我们已经开发了开源工具VerifAI和Scenic，它们实现了基于本文所述原则的技术，并应用于自动驾驶和航空航天领域的工业规模系统。

这些成就仅仅是一个开始，还有许多工作要做。

验证了在未来几年，AI有望继续成为有效的研究领域。

原文链接： https://cacm.ACM.org/magazines/2022/7/262079-toward-verified-artificial-intelligence/full text