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

用于设计和验证的计算引擎

硬件和软件系统形式化方法的有效性，是由底层“计算引擎”的进步推动的——例如，布尔可满足性求解 (SAT)、可满足性模理论 (SMT) 和模型检查。鉴于 AI/ML 系统规模、环境复杂性和所涉及的新型规范，需要一类新的计算引擎来进行高效且可扩展的训练、测试、设计和验证，实现这些进步必须克服的关键挑战。 5.1 数据集设计 数据是机器学习的基本起点，提高 ML 系统质量就必须提高它所学习数据的质量。形式化方法如何帮助 ML 数据系统地选择、设计和扩充？ ML 的数据生成与硬件和软件的测试生成问题有相似之处。形式化方法已被证明对系统的、基于约束的测试生成是有效的，但这与对人工智能系统的要求不同，约束类型可能要复杂得多——例如，对使用传感器从复杂环境（如交通状况）捕获的数据的“真实性”进行编码要求。我们不仅需要生成具有特定特征的数据项（如发现错误的测试），还需要生成满足分布约束的集合；数据生成必须满足数据集大小和多样性的目标，以进行有效的训练和泛化。这些要求都需要开发一套新的形式化技术。 形式方法中的受控随机化。数据集设计的这个问题有很多方面，首先必须定义“合法”输入的空间，以便根据应用程序语义正确形成示例；其次，需要捕获与现实世界数据相似性度量的约束；第三，通常需要对生成的示例的分布进行约束，以获得学习算法收敛到真实概念的保证。 我们相信这些方面可以通过随机形式方法来解决——用于生成受形式约束和分布要求的数据的随机算法。一类称为控制即兴创作的新技术是很有前景的，即兴创作的生成要满足三个约束的随机字符串（示例）x：

定义合法x空间的硬约束

一个软约束，定义生成的x必须如何与真实世界的示例相似

定义输出分布约束的随机性要求

目前，控制即兴理论仍处于起步阶段，我们才刚刚开始了解计算复杂性并设计有效的算法。反过来，即兴创作依赖于计算问题的最新进展，例如约束随机抽样、模型计数和基于概率编程的生成方法。 5.2 定量验证 除了通过传统指标（状态空间维度、组件数量等）衡量AI 系统规模之外，组件的类型可能要复杂得多。例如，自主和半自主车辆及其控制器必须建模为混合动力系统，结合离散和连续动力学；此外，环境中的代表（人类、其他车辆）可能需要建模为概率过程。最后，需求可能不仅涉及传统关于安全性和活性的布尔规范，还包括对系统鲁棒性和性能的定量要求，然而大多数现有的验证方法，都是针对回答布尔验证问题。为了解决这一差距，必须开发用于定量验证的新可扩展引擎。 定量语义分析。一般来说，人工智能系统的复杂性和异构性意味着，规范的形式验证（布尔或定量）是不可判定的——例如，即便是确定线性混合系统的状态是否可达，也是不可判定的。为了克服计算复杂性带来的这一障碍，人们必须在语义特征空间上使用概率和定量验证的新技术，以增强本节前面讨论的抽象和建模方法。对于同时具有布尔和定量语义的规范形式，在诸如度量时间逻辑之类的形式中，将验证表述为优化，对于统一来自形式方法的计算方法和来自优化文献的计算方法至关重要。例如在基于模拟的时间逻辑证伪中，尽管它们必须应用于语义特征空间以提高效率，这种伪造技术也可用于系统地、对抗性地生成 ML 组件的训练数据。概率验证的技术应该超越传统的形式，如马尔科夫链或MDPs，以验证语义特征空间上的概率程序。同样，关于SMT求解的工作必须扩展到更有效地处理成本约束--换句话说，将SMT求解与优化方法相结合。 我们需要了解在设计时可以保证什么，设计过程如何有助于运行时的安全操作，以及设计时和运行时技术如何有效地互操作。