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

环境建模

基于 AI/ML 的系统所运行的环境通常很复杂， 比如对自动驾驶汽车运行的各种城市交通环境的建模。事实上，AI/ML 经常被引入这些系统中以应对环境的复杂性和不确定性。当前的 ML 设计流程通常使用数据来隐性地规定环境。许多 AI 系统的目标是在其运行过程中发现并理解其环境，这与为先验指定的环境设计的传统系统不同。然而，所有形式验证和综合都与一个环境模型有关。因此，必须将有关输入数据的假设和属性解释到环境模型中。我们将这种二分法提炼为 AI 系统环境建模的三个挑战，并制定相应的原则来解决这些挑战。 2.1 建模不确定性 在形式验证的传统用法中，一种司空见惯的做法是将环境建模为受约束的非确定性过程，或者“干扰”。这种“过度近似”的环境建模能够允许人们更为保守地捕捉环境的不确定性，而无需过于详细的模型，这种模型的推理是很不高效的。然而，对于基于 AI 的自主性，纯粹的非确定性建模可能会产生太多虚假的错误报告，从而使验证过程在实践中变得毫无用处。例如在对一辆自动驾驶汽车的周围车辆行为的建模中，周围车辆的行为多种多样，如果采用纯粹的非确定性建模，就考虑不到总是意外发生的事故。此外，许多 AI/ML 系统隐式或显式地对来自环境的数据或行为做出分布假设，从而需要进行概率建模。由于很难准确地确定潜在的分布，所以不能假定生成的概率模型是完美的，并且必须在模型本身中对建模过程中的不确定性加以表征。 概率形式建模。为了应对这一挑战，我们建议使用结合概率建模和非确定性建模的形式。在能够可靠地指定或估计概率分布的情况下，可以使用概率建模。在其他情况下，非确定性建模可用于对环境行为进行过度近似。虽然诸如马尔可夫决策过程之类的形式主义已经提供了一种混合概率和非确定性的方法，但我们相信，更丰富的形式主义如概率规划范式，可以提供一种更具表达力和程序化的方式来对环境进行建模。我们预测，在许多情况下，此类概率程序需要（部分地）从数据中进行学习或合成。此时，学习参数中的任何不确定性都必须传播到系统的其余部分，并在概率模型中加以表示。例如，凸马尔可夫决策过程提供了一种方法来表示学习转变概率值的不确定性，并扩展了用于验证和控制的算法来解释这种不确定性。 2.2 未知的变量 在传统的形式验证领域如验证设备驱动程序中，系统 S 与其环境 E 之间的接口定义良好，E 只能通过该接口与 S 进行交互。对于基于 AI 的自主性而言，该接口是不完善的，它由传感器和感知组件规定，这些组件只能部分且嘈杂地捕捉环境，而且无法捕捉 S 和 E 之间的所有交互。所有环境的变量（特征）都是已知的，更不用说被感知到的变量。即使在环境变量已知的受限场景中，也明显缺乏有关其演变的信息，尤其是在设计的时候。此外，代表环境接口的激光雷达等传感器建模也是一项重大的技术挑战。 内省环境建模。我们建议通过开发内省的设计和验证方法来解决这个问题，也就是说，在系统 S 中进行内省，来对关于环境 E 的假设 A 进行算法上的识别，该假设足以保证满足规范 Φ。理想情况下，A 必须是此类假设中最弱的一个，并且还必须足够高效，以便在设计时生成、并在运行时监控可用传感器和有关环境的其他信息源，以及方便在假设被违反时可以采取缓解措施。此外，如果涉及人类操作员，人们可能希望 A 可以翻译成可理解的解释，也就是说 S 可以向人类“解释”为什么它可能无法满足规范 Φ。处理这些多重要求以及对良好传感器模型的需求，使得内省环境建模成为一个非常重要的问题。初步的工作表明，这种可监控假设的提取在简单的情况下是可行的，虽然需要做更多的工作才能让它具有实用性。 2.3 模拟人类行为 对于许多 AI 系统，例如半自动驾驶汽车，人类代理是环境和系统的关键部分。关于人类的人工模型无法充分捕捉人类行为的可变性和不确定性。另一方面，用于建模人类行为的数据驱动方法可能对 ML 模型使用的特征的表达能力和数据质量敏感。为了实现人类 AI 系统的高度保证，我们必须解决当前人类建模技术的局限性，并为其预测准确性和收敛性提供保障。 主动的数据驱动建模。我们相信，人类建模需要一种主动的数据驱动方法，模型结构和以数学形式表示的特征适合使用形式方法。人类建模的一个关键部分是捕捉人类意图。我们提出了一个三管齐下的方法：基于专家知识来定义模型的模板或特征，用离线学习来完成模型以供设计时使用，以及在运行时通过监控和与环境交互来学习和更新环境模型。例如，已经有研究表明，通过人类受试者实验从驾驶模拟器收集的数据，可用于生成人类驾驶员的行为模型，这些模型可用于验证和控制自动驾驶汽车。此外，计算机安全领域的对抗性训练和攻击技术可用于人类模型的主动学习，并可针对导致不安全行为的特定人类动作来进一步设计模型。这些技术可以帮助开发 human-AI 系统的验证算法。