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

文章图片
作者|SanjitA.Seshia,DorsaSadigh,S.ShankarSastry
编译|李梅、黄楠
编辑|陈彩娴
人工智能试图模仿人类智能的计算系统，包括人类一些与智能具有直观联系的功能，例如学习、解决问题以及理性地思考和行动。在广义地解释上， AI一词涵盖了许多密切相关的领域如机器学习。那些大量使用AI的系统在医疗保健、交通运输、金融、社交网络、电子商务和教育等领域都产生了重大的社会影响。
这种日益增长的社会影响，也带来了一系列风险和担忧，包括人工智能软件中的错误、网络攻击和人工智能系统安全等方面。因此， AI系统的验证问题以及更广泛的可信AI的话题已经开始引起研究界的关注。 “可验证AI”已经被确立为设计AI系统的目标，一个可验证的AI系统在特定的数学要求上具有强大的、理想情况下可证明的正确性保证。我们怎样才能实现这个目标？
最近，《ACM通讯》（TheCommunicationsofACM）上的一篇综述文章，试图从形式验证的角度来思考可证验AI面临的挑战，并给出了一些原则性的解决方案。文章作者是加州伯克利分校电气工程与计算机科学系的主任S.ShankarSastry和SanjitA.Seshia教授，以及斯坦福大学计算机科学系助理教授DorsaSadigh 。
在计算机科学和工程领域，形式方法涉及系统的严格的数学规范、设计和验证。其核心在于，形式方法是关于证明的：制定形成证明义务的规范，设计系统以履行这些义务，并通过算法证明搜索来验证系统确实符合其规范。从规范驱动的测试和仿真到模型检查和定理证明，一系列的形式化方法常被用于集成电路的计算机辅助设计，并已广泛被用于发现软件中的错误，分析网络物理系统，并发现安全漏洞。
本文回顾了形式化方法传统的应用方式，指明了形式化方法在AI系统中的五个独特挑战，包括：
开发关于环境的语言、算法
对复杂ML组件和系统进行抽象和表示
为AI系统和数据提出新的规范形式化方法和属性
开发针对自动推理的可扩展计算引擎
开发针对建构中可信（trustworthy-by-construction）设计的算法和技术
在讨论最新进展的基础上，作者提出了解决以上挑战的原则。本文不仅仅关注特定类型的AI组件如深度神经网络，或特定的方法如强化学习，而是试图涵盖更广泛的AI系统及其设计过程。此外，形式化方法只是通往可信AI的其中一种途径，所以本文的观点旨在对来自其他领域的方法加以补充。这些观点很大程度上来源于对自主和半自主系统中使用AI所产生的问题的思考，在这些系统中，安全性和验证性问题更加突出。
1概述图1显示了形式验证、形式综合和形式指导的运行时弹性的典型过程。形式验证过程从三个输入开始：

文章图片
图1：用于验证、综合和运行时弹性的形式化方法要验证的系统模型S
环境模型E
待验证的属性Φ
验证者生成“是”或“否”的答案作为输出，来表明S是否满足环境E中的属性Φ 。通常， “否”输出伴随着反例，也称为错误跟踪（errortrace），它是对系统的执行，表明Φ是如何被伪造的。一些验证工具还包括带有“是”答案的正确性证明或证书。我们对形式方法采取一种广泛的视角，包括使用形式规范、验证或综合的某些方面的任何技术。例如，我们囊括了基于仿真的硬件验证方法或基于模型的软件测试方法，因为它们也使用正式的规范或模型来指导仿真或测试的过程。