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

本文回顾了形式化方法传统的应用方式，指明了形式化方法在 AI 系统中的五个独特挑战。 人工智能试图模仿人类智能的计算系统，包括人类一些与智能具有直观联系的功能，例如学习、解决问题以及理性地思考和行动。在广义地解释上，AI 一词涵盖了许多密切相关的领域如机器学习。那些大量使用 AI 的系统在医疗保健、交通运输、金融、社交网络、电子商务和教育等领域都产生了重大的社会影响。 这种日益增长的社会影响，也带来了一系列风险和担忧，包括人工智能软件中的错误、网络攻击和人工智能系统安全等方面。因此，AI 系统的验证问题以及更广泛的可信 AI 的话题已经开始引起研究界的关注。“可验证 AI”已经被确立为设计 AI 系统的目标，一个可验证的 AI 系统在特定的数学要求上具有强大的、理想情况下可证明的正确性保证。我们怎样才能实现这个目标？ 最近，《ACM 通讯》（The Communications of ACM）上的一篇综述文章，试图从形式验证的角度来思考可证验 AI 面临的挑战，并给出了一些原则性的解决方案。文章作者是加州伯克利分校电气工程与计算机科学系的主任 S. Shankar Sastry 和 Sanjit A. Seshia 教授，以及斯坦福大学计算机科学系助理教授 Dorsa Sadigh。 在计算机科学和工程领域，形式方法涉及系统的严格的数学规范、设计和验证。其核心在于，形式方法是关于证明的：制定形成证明义务的规范，设计系统以履行这些义务，并通过算法证明搜索来验证系统确实符合其规范。从规范驱动的测试和仿真到模型检查和定理证明，一系列的形式化方法常被用于集成电路的计算机辅助设计，并已广泛被用于发现软件中的错误，分析网络物理系统，并发现安全漏洞。 本文回顾了形式化方法传统的应用方式，指明了形式化方法在 AI 系统中的五个独特挑战，包括：

开发关于环境的语言、算法

对复杂 ML 组件和系统进行抽象和表示

为 AI 系统和数据提出新的规范形式化方法和属性

开发针对自动推理的可扩展计算引擎

开发针对建构中可信（trustworthy-by-construction）设计的算法和技术

在讨论最新进展的基础上，作者提出了解决以上挑战的原则。本文不仅仅关注特定类型的 AI 组件如深度神经网络，或特定的方法如强化学习，而是试图涵盖更广泛的 AI 系统及其设计过程。此外，形式化方法只是通往可信 AI 的其中一种途径，所以本文的观点旨在对来自其他领域的方法加以补充。这些观点很大程度上来源于对自主和半自主系统中使用 AI 所产生的问题的思考，在这些系统中，安全性和验证性问题更加突出。