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

5.3 AI/ML 的组合推理 对于扩展到大型系统的正式方法，组合（模块化）推理是必不可少的。在组合验证中，一个大型系统（例如，程序）被拆分为它的组件（例如，程序），每个组件都根据规范进行验证，然后组件规范一起产生系统级规范。组合验证的一个常见方法是使用假设-保证合同，例如一个过程假设一些关于它的开始状态（前置条件），反过来又保证其结束状态（后置条件），类似的假设-保证范式已被开发并应用于并发的软件和硬件系统。 然而，这些范式并不涵盖人工智能系统，这在很大程度上是由于 "形式化规范 "一节中讨论的人工智能系统的规范化挑战。组合式验证需要组合式规范——也就是说，组件必须是可形式化的。然而，正如“形式化规范”中所述，可能无法正式指定一个感知组件的正确行为。因此，挑战之一就是开发不依赖于有完整组合规范的组合推理技术。此外，人工智能系统的定量和概率性质，要求将组合推理的理论扩展到定量系统和规范。 推断组件合同。人工智能系统的组合式设计和分析需要在多个方面取得进展。首先，需要在一些有前景的初步工作基础上，为这些系统的语义空间开发概率保证设计和验证的理论。第二，必须设计出新的归纳综合技术，以算法方式生成假设-保证合同，减少规范负担并促进组合推理。第三，为了处理诸如感知等没有精确正式规格的组件的情况，我们提出了从系统级分析中推断组件级约束的技术，并使用这种约束将组件级分析，包括对抗性分析，集中在搜索输入空间的 "相关 "部分。

建构中修正智能系统

在理想的世界中，验证将与设计过程相结合，因此系统是“在建构中修正的”。例如，验证可以与编译/合成步骤交错进行，假设在集成电路中常见的寄存器传输级（RTL）设计流程中，或许它可以被集成到合成算法中，以确保实现满足规范。我们能不能为人工智能系统设计一个合适的在建构中逐步修正的设计流程？ 6.1 ML 组件的规范驱动设计 给定一个正式的规范，我们能否设计一个可证明满足该规范的机器学习组件（模型）？这种全新的 ML 组件设计有很多方面：（1）设计数据集；（2） 综合模型的结构；（3）生成一组有代表性的特征；（4） 综合超参数和 ML 算法选择的其他方面；（5）在综合失败时自动化调试 ML 模型或规范的技术。 ML 组件的正式合成。解决前面所列出一些问题的解决方案正在出现，可以使用语义损失函数或通过认证的鲁棒性在 ML 模型上强制执行属性，这些技术可以与神经架构搜索等方法相结合，以生成正确构建的 DNN。另一种方法是基于新兴的形式归纳综合理论，即从满足形式化规范的程序实例中进行综合。解决形式归纳综合问题的最常见方法是使用 oracle-guided 方法，其中将学习者与回答查询的 oracle 配对；如示例中图2，oracle 可以是一个伪造者，它生成反例，显示学习组件的故障如何违反系统级规范。最后，使用定理证明来确保用于训练 ML 模型的算法的正确性，也是朝着建构修正的 ML 组件迈出的重要一步。 6.2 基于机器学习的系统设计 第二个挑战，是设计一个包含学习和非学习组件的整体系统。目前已经出现的几个研究问题：我们能否计算出可以限制 ML 组件运行的安全范围？我们能否设计一种控制或规划算法来克服它接收输入的基于 ML 感知组件的限制？我们可以为人工智能系统设计组合设计理论吗？当两个 ML 模型用于感知两种不同类型的传感器数据（例如，LiDAR 和视觉图像），并且每个模型在某些假设下都满足其规范，那么二者在什么条件下可以一起使用、以提高可靠性整体系统？ 在这一挑战上，取得进展的一个突出例子是基于安全学习的控制的工作。这种方法预先计算了一个安全包络线，并使用学习算法在该包络线内调整控制器，需要基于例如可达性分析、来有效计算此类安全包络的技术；同样，安全 RL 领域也取得了显着进展。 然而，这些并没有完全解决机器学习对感知和预测带来的挑战——例如，可证明安全的端到端深度强化学习尚未实现。 6.3 为弹性 AI 桥接设计时间和运行时间 正如“环境建模”部分所讨论的那样，许多 AI 系统在无法先验指定的环境中运行，因此总会有无法保证正确性的环境。在运行时实现容错和错误恢复的技术，对人工智能系统具有重要作用。我们需要系统地理解在设计时可以保证什么，设计过程如何有助于人工智能系统在运行时的安全和正确运行，以及设计时和运行时技术如何有效地互操作。 对此，关于容错和可靠系统的文献为我们提供了开发运行时保证技术的基础——即运行时验证和缓解技术；例如 Simplex 方法，就提供了一种将复杂但容易出错的模块与安全的、正式验证的备份模块相结合的方法。最近，结合设计时和运行时保证方法的技术显示了未验证的组件、包括那些基于人工智能和 ML 的组件，可以被包裹在运行时保证框架中，以提供安全运行的保证。但目前这些仅限于特定类别的系统，或者它们需要手动设计运行时监视器和缓解策略，在诸如内省环境建模、人工智能的监测器和安全回退策略的合成等方法上，还有更多的工作需要做。 此处讨论的建构中修正智能系统的设计方法可能会引入开销，使其更难以满足性能和实时要求。但我们相信（也许是非直觉的），在以下意义上，形式化方法甚至可以帮助提高系统的性能或能源效率。 传统的性能调优往往与上下文无关——例如，任务需要独立于它们运行的环境来满足最后期限。但如果设计时就对这些环境进行正式表征，并在运行时对其进行监控，如果其系统运行经过正式验证是安全的，那么在这种环境下，ML 模型就可以用准确性来换取更高的效率。这种权衡可能是未来研究的一个富有成果的领域。