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

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