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

3.3数据vs.形式要求
“数据即规范”的观点在机器学习中很常见。有限输入集上标记的“真实”数据通常是关于正确行为的唯一规范。这与形式化方法非常不同，形式化方法通常以逻辑或自动机的形式给出，它定义了遍历所有可能输入的正确行为的集合。数据和规范之间的差距值得注意，尤其是当数据有限、有偏见或来自非专家时。我们需要技术来对数据的属性进行形式化，包括在设计时可用的数据和尚未遇到的数据。
规范挖掘(Specificationmining) 。为了弥合数据和形式规范之间的差距，我们建议使用算法从数据和其他观察中来推断规范——即所谓的规范挖掘技术。此类方法通常可用于ML组件，包括感知组件，因为在许多情况下，它不需要具有精确的规范或人类可读的规范。我们还可以使用规范挖掘方法，从演示或更复杂的多个代理（人类和人工智能）之间的交互形式来推断人类意图和其他属性。
4学习系统的建模在形式验证的大多数传统应用中，系统S在设计时是固定的且已知的，比如它可以是一个程序，或者一个用编程语言或硬件描述语言来描述的电路。系统建模问题主要涉及的，是通过抽象掉不相关的细节，来将S减小到更易于处理的大小。 AI系统给系统建模带来了非常不同的挑战，这主要源于机器学习的使用：
高维输入空间
用于感知的ML组件通常在非常高维的输入空间上运行。比如，一个输入的RGB图像可以是1000x600像素，它包含256((1000x600x3))个元素，输入通常就是这样的高维向量流。尽管研究人员已经对高维输入空间（如在数字电路中）使用了形式化方法，但基于ML的感知输入空间的性质是不同的，它不完全是布尔值，而是混合的，包括离散变量和连续变量。
高维参数/状态空间
深度神经网络等ML组件具有数千到数百万个模型参数和原始组件。例如，图2中使用的最先进的DNN有多达6000万个参数和数十层组件。这就产生了巨大的验证搜索空间，抽象过程需要非常仔细。
在线适应和进化
一些学习系统如使用RL的机器人，会随着它们遇到的新数据和新情况而发生进化。对于这样的系统，设计时的验证必须考虑系统行为的未来演变，或者随着学习系统的发展逐步地在线执行。
在上下文中建模系统
对于许多AI/ML组件，它们的规范仅仅由上下文来定义。例如，要验证图2中基于DNN的系统的安全性，就需要对环境进行建模。我们需要对ML组件及其上下文进行建模的技术，以便可以验证在语义上有意义的属性。
近年来，许多工作都专注于提高效率，来验证DNN的鲁棒性和输入-输出属性。然而，这还不够，我们还需要在以下三个方面取得进展：
自动抽象和高效表示
自动生成系统的抽象一直是形式方法的关键，它在将形式方法的范围扩展到大型硬件和软件系统方面发挥着至关重要的作用。为了解决基于ML的系统的超高维混合状态空间和输入空间方面的挑战，我们需要开发有效的技术来将ML模型抽象为更易于形式分析的、更简单的模型。一些有希望的方向包括：使用抽象解释来分析DNN ，开发用于伪造有ML组件的网络物理系统的抽象，以及设计用于验证的新表示（比如星集）。
解释与因果
如果学习者在其预测中附上关于预测是如何从数据和背景知识中产生的的解释，那我们就可以简化对学习系统进行建模的任务。这个想法并不新鲜， ML社区已经对诸如“基于解释的泛化”等术语进行了研究，但是最近，人们正在对使用逻辑来解释学习系统的输出重新产生了兴趣。解释生成有助于在设计时调试设计和规范，并有助于合成鲁棒的AI系统以在运行时提供保障。包含因果推理和反事实推理的ML还可以帮助生成用于形式方法的解释。