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

结论

从形式化方法的角度来看，我们剖析了设计高保证人工智能系统的问题。如图3所示，我们确定了将形式化方法应用于 AI 系统的五个主要挑战，并对这五项挑战中的每一项都制定了三项设计和验证原则，这些原则有希望解决这个挑战。 图 3 中的边显示了这些原则之间的依赖关系，例如运行时保证依赖于自省和数据驱动的环境建模，以提取可监测的假设和环境模型。同样，为了进行系统级分析，我们需要进行组合推理和抽象，其中一些 AI 组件可能需要挖掘规范，而其他组件则通过形式化的归纳综合构建生成正确的结构。 自 2016 年以来，包括作者在内的几位研究人员一直致力于应对这些挑战，当时本文已发表的原始版本介绍了一些样本进展。我们已经开发了开源工具 VerifAI 和 Scenic，它们实现了基于本文所述原则的技术，并已应用于自动驾驶和航空航天领域的工业规模系统。这些成果只是一个开始，还有很多事情要做。在未来的几年里，可验证 AI 有望继续成为一个富有成效的研究领域。