迈向可验证的 AI: 形式化方法的五大挑战( 二 ) 作者|SanjitA.Seshia|DorsaSadigh|S.S

要将形式验证应用于AI系统，必须能够以形式来表示至少S、E和Φ这三个输入，理想情况下，会存在有效的决策程序来回答先前所描述的“是/否”问题。然而，即使要对三个输入构建良好的表示，也并不是一件简单的事，更不用说处理底层设计和验证问题的复杂性了。
【迈向可验证的 AI: 形式化方法的五大挑战】我们这里通过半自动驾驶领域的示例来说明本文的观点。图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建模不确定性