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

语义特征空间
当生成的对抗性输入和反例在所使用的ML模型的上下文中具有语义意义时， ML模型的对抗性分析和形式验证就更有意义。例如，针对汽车颜色或一天中时间的微小变化来分析DNN对象检测器的技术，比向少量任意选择的像素添加噪声的技术更有用。当前，大多数的方法在这一点上都还达不到要求。我们需要语义对抗分析，即在ML模型所属系统的上下文中对它们进行分析。其中额的一个关键步骤，是表示对ML系统运行的环境建模的语义特征空间，而不是为ML模型定义输入空间的具体特征空间。这是符合直觉的，即与完整的具体特征空间相比，具体特征空间在语义上有意义的部分（如交通场景图像）所形成的潜在空间要低得多。图2中的语义特征空间是代表自动驾驶汽车周围3D世界的低维空间，而具体的特征空间是高维像素空间。由于语义特征空间的维数较低，因此可以更容易地进行搜索。但是，我们还需要一个“渲染器” ，将语义特征空间中的一个点映射到具体特征空间中的一个点。渲染器的属性如可微性（differentiability），可以更容易地应用形式化方法来执行语义特征空间的目标导向搜索。
5用于设计和验证的计算引擎硬件和软件系统形式化方法的有效性，是由底层“计算引擎”的进步推动的——例如，布尔可满足性求解(SAT)、可满足性模理论(SMT)和模型检查。鉴于AI/ML系统规模、环境复杂性和所涉及的新型规范，需要一类新的计算引擎来进行高效且可扩展的训练、测试、设计和验证，实现这些进步必须克服的关键挑战。
5.1数据集设计
数据是机器学习的基本起点，提高ML系统质量就必须提高它所学习数据的质量。形式化方法如何帮助ML数据系统地选择、设计和扩充？
ML的数据生成与硬件和软件的测试生成问题有相似之处。形式化方法已被证明对系统的、基于约束的测试生成是有效的，但这与对人工智能系统的要求不同，约束类型可能要复杂得多——例如，对使用传感器从复杂环境（如交通状况）捕获的数据的“真实性”进行编码要求。我们不仅需要生成具有特定特征的数据项（如发现错误的测试），还需要生成满足分布约束的集合；数据生成必须满足数据集大小和多样性的目标，以进行有效的训练和泛化。这些要求都需要开发一套新的形式化技术。
形式方法中的受控随机化。数据集设计的这个问题有很多方面，首先必须定义“合法”输入的空间，以便根据应用程序语义正确形成示例；其次，需要捕获与现实世界数据相似性度量的约束；第三，通常需要对生成的示例的分布进行约束，以获得学习算法收敛到真实概念的保证。
我们相信这些方面可以通过随机形式方法来解决——用于生成受形式约束和分布要求的数据的随机算法。一类称为控制即兴创作的新技术是很有前景的，即兴创作的生成要满足三个约束的随机字符串（示例）x：
定义合法x空间的硬约束
一个软约束，定义生成的x必须如何与真实世界的示例相似
定义输出分布约束的随机性要求
目前，控制即兴理论仍处于起步阶段，我们才刚刚开始了解计算复杂性并设计有效的算法。反过来，即兴创作依赖于计算问题的最新进展，例如约束随机抽样、模型计数和基于概率编程的生成方法。
5.2定量验证
除了通过传统指标（状态空间维度、组件数量等）衡量AI系统规模之外，组件的类型可能要复杂得多。例如，自主和半自主车辆及其控制器必须建模为混合动力系统，结合离散和连续动力学；此外，环境中的代表（人类、其他车辆）可能需要建模为概率过程。最后，需求可能不仅涉及传统关于安全性和活性的布尔规范，还包括对系统鲁棒性和性能的定量要求，然而大多数现有的验证方法，都是针对回答布尔验证问题。为了解决这一差距，必须开发用于定量验证的新可扩展引擎。