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

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