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

概述

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

要验证的系统模型 S

环境模型 E

待验证的属性 Φ

验证者生成“是”或“否”的答案作为输出，来表明 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 个挑战领域总结