迈向可验证的 AI：形式化方法的五大挑战
发布时间：2022-07-30 12:44:06 所属栏目：大数据 来源：互联网
导读：人工智能试图模仿人类智能的计算系统，包括人类一些与智能具有直观联系的功能，例如学习、解决问题以及理性地思考和行动。在广义地解释上，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 所产生的问题的思考，在这些系统中，安全性和验证性问题更加突出。 概述 图 1 显示了形式验证、形式综合和形式指导的运行时弹性的典型过程。形式验证过程从三个输入开始： 要验证的系统模型 S 环境模型 E 待验证的属性 Φ 验证者生成“是”或“否”的答案作为输出，来表明 S 是否满足环境 E 中的属性 Φ。通常，“否”输出伴随着反例，也称为错误跟踪（error trace），它是对系统的执行，表明 Φ 是如何被伪造的。一些验证工具还包括带有“是”答案的正确性证明或证书。我们对形式方法采取一种广泛的视角，包括使用形式规范、验证或综合的某些方面的任何技术。例如，我们囊括了基于仿真的硬件验证方法或基于模型的软件测试方法，因为它们也使用正式的规范或模型来指导仿真或测试的过程。 要将形式验证应用于 AI 系统，必须能够以形式来表示至少 S、E 和 Φ 这三个输入，理想情况下，会存在有效的决策程序来回答先前所描述的“是/否”问题。然而，即使要对三个输入构建良好的表示，也并不是一件简单的事，更不用说处理底层设计和验证问题的复杂性了。 我们这里通过半自动驾驶领域的示例来说明本文的观点。图 2 显示了一个 AI 系统的说明性示例：一个闭环 CPS，包括一辆带有机器学习组件的半自动车辆及其环境。具体来说，假设半自动的“自我”（ego）车辆有一个自动紧急制动系统 (AEBS)，该系统试图对前方的物体进行检测和分类，并在需要避免碰撞时启动制动器。图 2 中，一个 AEBS 包括一个由控制器（自动制动）、一个受控对象（受控的车辆子系统，包括自主堆栈的其他部分）和一个传感器（摄像头），以及一个使用 DNN 的感知组件。AEBS 与车辆环境相结合，形成一个闭环 CPS。“自我”车辆的环境包括车辆外部（其他车辆、行人等）以及车辆内部（例如驾驶员）的代理和对象。这种闭环系统的安全要求可以非形式地刻画为以一种属性，即在移动的“自我”车辆与道路上的任何其他代理或物体之间保持安全距离。然而，这种系统在规范、建模和验证方面存在许多细微差别。 第一，考虑对半自动车辆的环境进行建模。即使是环境中有多少和哪些代理（包括人类和非人类）这样的问题，也可能存在相当大的不确定性，更不用说它们的属性和行为了。第二，使用 AI 或 ML 的感知任务即使不是不可能，也很难形式化地加以规定。第三，诸如 DNN 之类的组件可能是在复杂、高维输入空间上运行的复杂、高维对象。因此，在生成形式验证过程的三个输入 S、E、Φ 时，即便采用一种能够使验证易于处理的形式，也十分具有挑战性。 如果有人解决了这个问题，那就会面临一项艰巨的任务，即验证一个如图 2 那样复杂的基于 AI 的 CPS。在这样的 CPS 中，组合（模块化）方法对于可扩展性来说至关重要，但它会由于组合规范的难度之类的因素而难以实施。最后，建构中修正的方法（correct-by-construction,CBC）有望实现可验证 AI，但它还处于起步阶段，非常依赖于规范和验证方面的进步。图 3 总结了可验证 AI 的五个挑战性领域。对于每个领域，我们将目前有前景的方法提炼成克服挑战的三个原则，用节点表示。节点之间的边缘显示了可验证 AI 的哪些原则相互依赖，共同的依赖线程由单一颜色表示。下文将详细阐述这些挑战和相应的原则。 环境建模 基于 AI/ML 的系统所运行的环境通常很复杂， 比如对自动驾驶汽车运行的各种城市交通环境的建模。事实上，AI/ML 经常被引入这些系统中以应对环境的复杂性和不确定性。当前的 ML 设计流程通常使用数据来隐性地规定环境。许多 AI 系统的目标是在其运行过程中发现并理解其环境，这与为先验指定的环境设计的传统系统不同。然而，所有形式验证和综合都与一个环境模型有关。因此，必须将有关输入数据的假设和属性解释到环境模型中。我们将这种二分法提炼为 AI 系统环境建模的三个挑战，并制定相应的原则来解决这些挑战。 2.1 建模不确定性 在形式验证的传统用法中，一种司空见惯的做法是将环境建模为受约束的非确定性过程，或者“干扰”。这种“过度近似”的环境建模能够允许人们更为保守地捕捉环境的不确定性，而无需过于详细的模型，这种模型的推理是很不高效的。然而，对于基于 AI 的自主性，纯粹的非确定性建模可能会产生太多虚假的错误报告，从而使验证过程在实践中变得毫无用处。例如在对一辆自动驾驶汽车的周围车辆行为的建模中，周围车辆的行为多种多样，如果采用纯粹的非确定性建模，就考虑不到总是意外发生的事故。此外，许多 AI/ML 系统隐式或显式地对来自环境的数据或行为做出分布假设，从而需要进行概率建模。由于很难准确地确定潜在的分布，所以不能假定生成的概率模型是完美的，并且必须在模型本身中对建模过程中的不确定性加以表征。 概率形式建模。为了应对这一挑战，我们建议使用结合概率建模和非确定性建模的形式。在能够可靠地指定或估计概率分布的情况下，可以使用概率建模。在其他情况下，非确定性建模可用于对环境行为进行过度近似。虽然诸如马尔可夫决策过程之类的形式主义已经提供了一种混合概率和非确定性的方法，但我们相信，更丰富的形式主义如概率规划范式，可以提供一种更具表达力和程序化的方式来对环境进行建模。我们预测，在许多情况下，此类概率程序需要（部分地）从数据中进行学习或合成。此时，学习参数中的任何不确定性都必须传播到系统的其余部分，并在概率模型中加以表示。例如，凸马尔可夫决策过程提供了一种方法来表示学习转变概率值的不确定性，并扩展了用于验证和控制的算法来解释这种不确定性。 （编辑：开发网_郴州站长网） 【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容! |
浙公网安备 33038102330466号