迈向可验证的 AI: 形式化方法的五大挑战(5)

学习系统的建模

在形式验证的大多数传统应用中，系统 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），可以更容易地应用形式化方法来执行语义特征空间的目标导向搜索。