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

主动的数据驱动建模。我们相信，人类建模需要一种主动的数据驱动方法，模型结构和以数学形式表示的特征适合使用形式方法。人类建模的一个关键部分是捕捉人类意图。我们提出了一个三管齐下的方法：基于专家知识来定义模型的模板或特征，用离线学习来完成模型以供设计时使用，以及在运行时通过监控和与环境交互来学习和更新环境模型。例如，已经有研究表明，通过人类受试者实验从驾驶模拟器收集的数据，可用于生成人类驾驶员的行为模型，这些模型可用于验证和控制自动驾驶汽车。此外，计算机安全领域的对抗性训练和攻击技术可用于人类模型的主动学习，并可针对导致不安全行为的特定人类动作来进一步设计模型。这些技术可以帮助开发human-AI系统的验证算法。
3形式化规范形式化验证严重依赖于形式化规范——即对系统应该做什么的精确的数学陈述。即使在形式化方法已经取得相当大成功的领域，提出高质量的形式化规范也是一项挑战，而AI系统尤其面临着独特的挑战。
3.1难以形式化的任务
图2中AEBS控制器中的感知模块必须检测和分类对象，从而将车辆和行人与其他实体区分开来。在经典的形式方法意义上，这个模块的准确性要求对每种类型的道路使用者和对象进行形式定义，这是极其困难的。这种问题存在于这个感知模块的所有实现中，而不仅仅出现在基于深度学习的方法中。其他涉及感知和交流的任务也会出现类似的问题，比如自然语言处理。那么，我们如何为这样的模块指定精度属性呢？规范语言应该是什么？我们可以使用哪些工具来构建规范？
端到端/系统水平的规范（End-to-end/system-levelspecifications）。为了应对上述挑战，我们可以对这个问题稍加变通。与其直接对难以形式化的任务进行规范，不如首先专注于精确地指定AI系统的端到端行为。从这种系统水平的规范中，可以获得对难以形式化的组件的输入-输出接口的约束。这些约束用作一个组件水平（component-level）的规范，这个规范与整个AI系统的上下文相关。对于图2中的AEBS示例，这涉及对属性Φ的规定，该属性即在运动过程中与任何对象都保持最小距离，从中我们可得出对DNN输入空间的约束，在对抗分析中捕捉语义上有意义的输入空间。
3.2定量规范vs.布尔规范
传统上，形式规范往往是布尔型的，它将给定的系统行为映射为“真”或“假” 。然而，在AI和ML中，规范通常作为规范成本或奖励的目标函数给出。此外，可能有多个目标，其中一些必须一起满足，而另一些则可能需要在某些环境中相互权衡。统一布尔和定量两种规范方法的最佳方式是什么？是否有能够统一捕捉AI组件常见属性（如鲁棒性和公平性）的形式？
混合定量和布尔规范。布尔规范和定量规范都有其优点：布尔规范更容易组合，但目标函数有助于用基于优化的技术进行验证和综合，并定义更精细的属性满足粒度。弥补这一差距的一种方法是转向定量规范语言，例如使用具有布尔和定量语义的逻辑（如度量时序逻辑），或将自动机与RL的奖励函数相结合。另一种方法是将布尔和定量规范组合成一个通用的规范结构，例如一本规则手册，手册中的规范可以按层次结构进行组织、比较和汇总。有研究已经确定了AI系统的几类属性，包括鲁棒性、公平性、隐私性、问责性和透明度。研究者正在提出新的形式主义，将形式方法和ML的思想联系起来，以对这些属性的变体（如语义鲁棒性）进行建模。