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

定量语义分析。一般来说，人工智能系统的复杂性和异构性意味着，规范的形式验证（布尔或定量）是不可判定的——例如，即便是确定线性混合系统的状态是否可达，也是不可判定的。为了克服计算复杂性带来的这一障碍，人们必须在语义特征空间上使用概率和定量验证的新技术，以增强本节前面讨论的抽象和建模方法。对于同时具有布尔和定量语义的规范形式，在诸如度量时间逻辑之类的形式中，将验证表述为优化，对于统一来自形式方法的计算方法和来自优化文献的计算方法至关重要。例如在基于模拟的时间逻辑证伪中，尽管它们必须应用于语义特征空间以提高效率，这种伪造技术也可用于系统地、对抗性地生成ML组件的训练数据。概率验证的技术应该超越传统的形式，如马尔科夫链或MDPs ，以验证语义特征空间上的概率程序。同样，关于SMT求解的工作必须扩展到更有效地处理成本约束--换句话说，将SMT求解与优化方法相结合。
我们需要了解在设计时可以保证什么，设计过程如何有助于运行时的安全操作，以及设计时和运行时技术如何有效地互操作。5.3AI/ML的组合推理
对于扩展到大型系统的正式方法，组合（模块化）推理是必不可少的。在组合验证中，一个大型系统（例如，程序）被拆分为它的组件（例如，程序），每个组件都根据规范进行验证，然后组件规范一起产生系统级规范。组合验证的一个常见方法是使用假设-保证合同，例如一个过程假设一些关于它的开始状态（前置条件），反过来又保证其结束状态（后置条件），类似的假设-保证范式已被开发并应用于并发的软件和硬件系统。
然而，这些范式并不涵盖人工智能系统，这在很大程度上是由于"形式化规范"一节中讨论的人工智能系统的规范化挑战。组合式验证需要组合式规范——也就是说，组件必须是可形式化的。然而，正如“形式化规范”中所述，可能无法正式指定一个感知组件的正确行为。因此，挑战之一就是开发不依赖于有完整组合规范的组合推理技术。此外，人工智能系统的定量和概率性质，要求将组合推理的理论扩展到定量系统和规范。
推断组件合同。人工智能系统的组合式设计和分析需要在多个方面取得进展。首先，需要在一些有前景的初步工作基础上，为这些系统的语义空间开发概率保证设计和验证的理论。第二，必须设计出新的归纳综合技术，以算法方式生成假设-保证合同，减少规范负担并促进组合推理。第三，为了处理诸如感知等没有精确正式规格的组件的情况，我们提出了从系统级分析中推断组件级约束的技术，并使用这种约束将组件级分析，包括对抗性分析，集中在搜索输入空间的"相关"部分。
6建构中修正智能系统在理想的世界中，验证将与设计过程相结合，因此系统是“在建构中修正的” 。例如，验证可以与编译/合成步骤交错进行，假设在集成电路中常见的寄存器传输级（RTL）设计流程中，或许它可以被集成到合成算法中，以确保实现满足规范。我们能不能为人工智能系统设计一个合适的在建构中逐步修正的设计流程？
6.1ML组件的规范驱动设计
给定一个正式的规范，我们能否设计一个可证明满足该规范的机器学习组件（模型）？这种全新的ML组件设计有很多方面：（1）设计数据集，（2）综合模型的结构，（3）生成一组有代表性的特征，（4）综合超参数和ML算法选择的其他方面，以及（5）在综合失败时自动化调试ML模型或规范的技术。