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

形式化规范

形式化验证严重依赖于形式化规范——即对系统应该做什么的精确的数学陈述。即使在形式化方法已经取得相当大成功的领域，提出高质量的形式化规范也是一项挑战，而 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 组件，包括感知组件，因为在许多情况下，它不需要具有精确的规范或人类可读的规范。我们还可以使用规范挖掘方法，从演示或更复杂的多个代理（人类和人工智能）之间的交互形式来推断人类意图和其他属性。