米兰·(milan)中国官方网站-迈向可验证的 AI: 形式化方法的五大挑战
作者 | Sanjit A. Seshia, Dorsa Sadigh, S. Shankar Sastry
编译 | 李梅、黄楠
编纂 | 陈彩娴
人工智能试图模拟人类智能的计较体系，包括人类一些与智能具备直不雅接洽的功效，例如进修、解决问题以和理性地思索及步履。于广义地注释上，AI 一词涵盖了很多紧密亲密相干的范畴如呆板进修。那些年夜量利用 AI 的体系于医疗保健、交通运输、金融、社交收集、电子商务及教诲等范畴都孕育发生了庞大的社会影响。
这类日趋增加的社会影响，也带来了一系列危害及担心，包括人工智能软件中的过错、收集进犯及人工智能体系安全等方面。是以，AI 体系的验证问题以和更广泛的可托 AI 的话题已经经最先引起研究界的存眷。“可验证 AI”已经经被确立为设计 AI 体系的方针，一个可验证的 AI 体系于特定的数学要求上具备强盛的、抱负环境下可证实的准确性包管。咱们如何才能实现这个方针？
近来，《ACM 通信》（The Co妹妹unications of ACM）上的一篇综述文章，试图从情势验证的角度来思索可证验 AI 面对的挑战，并给出了一些原则性的解决方案。文章作者是加州伯克利分校电气工程与计较机科学系的主任 S. Shankar Sastry 及 Sanjit A. Seshia 传授，以和斯坦福年夜学计较机科学系助理传授 Dorsa Sadigh。
于计较机科学及工程范畴，情势要领触及体系的严酷的数学规范、设计及验证。其焦点于在，情势要领是关在证实的：制订形成证实义务的规范，设计体系以执行这些义务，并经由过程算法证实搜刮来验证体系确凿切合其规范。从规范驱动的测试及仿真到模子查抄及定理证实，一系列的情势化要领常被用在集成电路的计较机辅助设计，并已经广泛被用在发明软件中的过错，阐发收集物理体系，并发明安全缝隙。
本文回首了情势化要领传统的运用方式，指了然情势化要领于 AI 体系中的五个怪异挑战，包括：
开发关在情况的语言、算法
对于繁杂 ML 组件及体系举行抽象及暗示
为 AI 体系及数据提出新的规范情势化要领及属性
开发针对于主动推理的可扩大计较引擎
开发针对于建构中可托（trustworthy-by-construction）设计的算法及技能
于会商最新进展的基础上，作者提出相识决以上挑战的原则。本文不单单存眷特定类型的 AI 组件如深度神经收集，或者特定的要领如强化进修，而是试图涵盖更广泛的 AI 体系和其设计历程。此外，情势化要领只是通往可托 AI 的此中一种路子，以是本文的不雅点旨于对于来自其他范畴的要领加以增补。这些不雅点很年夜水平上来历在对于自立及半自立体系中利用 AI 所孕育发生的问题的思索，于这些体系中，安全性及验证性问题越发凸起。
1概述图 1 显示了情势验证、情势综合及情势引导的运行时弹性的典型历程。情势验证历程从三个输入最先：
图 1 ：用在验证、综合及运行时弹性的情势化要领要验证的体系模子 S
情况模子 E
待验证的属性 Φ
验证者天生“是”或者“否”的谜底作为输出，来注解 S 是否满意情况 E 中的属性 Φ。凡是，“否”输出陪同着反例，也称为过错跟踪（error trace），它是对于体系的履行，注解 Φ 是怎样被伪造的。一些验证东西还有包括带有“是”谜底的准确性证实或者证书。咱们对于情势要领采纳一种广泛的视角，包括利用情势规范、验证或者综合的某些方面的任何技能。例如，咱们席卷了基在仿真的硬件验证要领或者基在模子的软件测试要领，由于它们也利用正式的规范或者模子来引导仿真或者测试的历程。
要将情势验证运用在 AI 体系，必需可以或许以情势来暗示至少 S、E 及 Φ 这三个输入，抱负环境下，会存于有用的决议计划步伐往返答先前所描写的“是/否”问题。然而，纵然要对于三个输入构建优良的暗示，也其实不是一件简朴的事，更不消说处置惩罚底层设计及验证问题的繁杂性了。
咱们这里经由过程半主动驾驶范畴的示例来讲明本文的不雅点。图 2 显示了一个 AI 体系的申明性示例：一个闭环 CPS，包括一辆带有呆板进修组件的半主动车辆和其情况。详细来讲，假定半主动的“自我”（ego）车辆有一个主动紧迫制动体系 (AEBS)，该体系试图对于前方的物体举行检测及分类，并于需要防止碰撞时启动制动器。图 2 中，一个 AEBS 包括一个由节制器（主动制动）、一个受控对于象（受控的车辆子体系，包括自立仓库的其他部门）及一个传感器（摄像头），以和一个利用 DNN 的感知组件。AEBS 与车辆情况相联合，形成一个闭环 CPS。“自我”车辆的情况包括车辆外部（其他车辆、行人等）以和车辆内部（例如驾驶员）的代办署理及对于象。这类闭环体系的安全要求可以非情势地描画为以一种属性，即于挪动的“自我”车辆与门路上的任何其他代办署理或者物体之间连结安全间隔。然而，这类体系于规范、建模及验证方面存于很多细微不同。
图 2：包罗呆板进修组件的闭环 CPS 示例
第一，思量对于半主动车辆的情况举行建模。纵然是情况中有几多及哪些代办署理（包括人类及非人类）如许的问题，也可能存于相称年夜的不确定性，更不消说它们的属性及举动了。第二，利用 AI 或者 ML 的感知使命纵然不是不成能，也很难情势化地加以划定。第三，诸如 DNN 之类的组件多是于繁杂、高维输入空间上运行的繁杂、高维对于象。是以，于天生情势验证历程的三个输入 S、E、Φ 时，即便采用一种可以或许使验证易在处置惩罚的情势，也十分具备挑战性。
假如有人解决了这个问题，那就碰面临一项艰难的使命，即验证一个如图 2 那样繁杂的基在 AI 的 CPS。于如许的 CPS 中，组合（模块化）要领对于在可扩大性来讲至关主要，但它会因为组合规范的难度之类的因素而难以实行。末了，建构中批改的要领（correct-by-construction,CBC）有望实现可验证 AI，但它还有处在起步阶段，很是依靠在规范及验证方面的前进。图 3 总结了可验证 AI 的五个挑战性范畴。对于在每一个范畴，咱们将今朝有远景的要领提炼成降服挑战的三个原则，用节点暗示。节点之间的边沿显示了可验证 AI 的哪些原则彼此依靠，配合的依靠线程由单一颜色暗示。下文将具体论述这些挑战及响应的原则。
图 3：可验证 AI 的 5 个挑战范畴总结
2情况建模基在 AI/ML 的体系所运行的情况凡是很繁杂， 好比对于主动驾驶汽车运行的各类都会交通情况的建模。事实上，AI/ML 常常被引入这些体系中以应答情况的繁杂性及不确定性。当前的 ML 设计流程凡是利用数据来隐性地划定情况。很多 AI 体系的方针是于其运行历程中发明并理解其情况，这与为先验指定的情况设计的传统体系差别。然而，所有情势验证及综合都与一个情况模子有关。是以，必需将有关输入数据的假定及属性注释到情况模子中。咱们将这类二分法提炼为 AI 体系情况建模的三个挑战，并制订响应的原则来解决这些挑战。
2.1 建模不确定性
于情势验证的传统用法中，一种习以为常的做法是将情况建模为受约束的非确定性历程，或者者“滋扰”。这类“过分类似”的情况建模可以或许答应人们更为守旧地捕获情况的不确定性，而无需过在具体的模子，这类模子的推理是很不高效的。然而，对于在基在 AI 的自立性，纯粹的非确定性建模可能会孕育发生太多虚伪的过错陈诉，从而使验证历程于实践中变患上毫无用场。例如于对于一辆主动驾驶汽车的周围车辆举动的建模中，周围车辆的举动多种多样，假如采用纯粹的非确定性建模，就思量不到老是不测发生的变乱。此外，很多 AI/ML 体系隐式或者显式地对于来自情况的数据或者举动做出漫衍假定，从而需要举行几率建模。因为很难正确地确定潜于的漫衍，以是不克不及假设天生的几率模子是完善的，而且必需于模子自己中对于建模历程中的不确定性加以表征。
几率情势建模。为了应答这一挑战，咱们建议利用联合几率建模及非确定性建模的情势。于可以或许靠得住地指定或者预计几率漫衍的环境下，可使用几率建模。于其他环境下，非确定性建模可用在对于情况举动举行过分类似。虽然诸如马尔可夫决议计划历程之类的情势主义已经经提供了一种混淆几率及非确定性的要领，但咱们信赖，更富厚的情势主义如几率计划范式，可以提供一种更具表达力及步伐化的方式来对于情况举行建模。咱们猜测，于很多环境下，此类几率步伐需要（部门地）从数据中举行进修或者合成。此时，进修参数中的任何不确定性都必需流传到体系的其余部门，并于几率模子中加以暗示。例如，凸马尔可夫决议计划历程提供了一种要领来暗示进修改变几率值的不确定性，并扩大了用在验证及节制的算法来注释这类不确定性。
2.2 未知的变量
于传统的情势验证范畴如验证装备驱动步伐中，体系 S 与其情况 E 之间的接口界说优良，E 只能经由过程该接口与 S 举行交互。对于在基在 AI 的自立性而言，该接口是不完美的，它由传感器及感知组件划定，这些组件只能部门且嘈杂地捕获情况，并且没法捕捕获 S 及 E 之间的所有交互。所有情况的变量（特性）都是已经知的，更不消说被感知到的变量。纵然于情况变量已经知的受限场景中，也较着缺少有关其蜕变的信息，特别是于设计的时辰。此外，代表情况接口的激光雷达等传感器建模也是一项庞大的技能挑战。
自察情况建模。咱们建议经由过程开发自察的设计及验证要领来解决这个问题，也就是说，于体系 S 中举行自察，来对于关在情况 E 的假定 A 举行算法上的辨认，该假定足以包管满意规范 Φ。抱负环境下，A 必需是此类假定中最弱的一个，而且还有必需充足高效，以便于设计时天生、并于运行时监控可用传感器及有关情况的其他信息源，以和利便于假定被违背时可以采纳减缓办法。此外，假如触及人类操作员，人们可能但愿 A 可以翻译成可理解的注释，也就是说 S 可以向人类“注释”为何它可能没法满意规范 Φ。处置惩罚这些多主要求以和对于优良传感器模子的需求，使患上自察情况建模成为一个很是主要的问题。开端的事情注解，这类可监控假定的提取于简朴的环境下是可行的，虽然需要做更多的事情才能让它具备实用性。
2.3 模仿人类举动
对于在很多 AI 体系，例如半主动驾驶汽车，人类代办署理是情况及体系的要害部门。关在人类的人工模子没法充实捕获人类举动的可变性及不确定性。另外一方面，用在建模人类举动的数据驱动要领可能对于 ML 模子利用的特性的表达能力及数据质量敏感。为了实现人类 AI 体系的高度包管，咱们必需解决当前人类建模技能的局限性，并为其猜测正确性及收敛性提供保障。
自动的数据驱动建模。咱们信赖，人类建模需要一种自动的数据驱动要领，模子布局及以数学情势暗示的特性合适利用情势要领。人类建模的一个要害部门是捕获人类用意。咱们提出了一个三管齐下的要领：基在专家常识来界说模子的模板或者特性，用离线进修来完成模子以供设计时利用，以和于运行时经由过程监控及与情况交互来进修及更新情况模子。例如，已经经有研究注解，经由过程人类受试者试验从驾驶模仿器网络的数据，可用在天生人类驾驶员的举动模子，这些模子可用在验证及节制主动驾驶汽车。此外，计较机安全范畴的匹敌性练习及进犯技能可用在人类模子的自动进修，并可针对于致使不安全举动的特定人类动作来进一步设计模子。这些技能可以帮忙开发 human-AI 体系的验证算法。
3情势化规范情势化验证严峻依靠在情势化规范——即对于体系应该做甚么的切确的数学陈述。纵然于情势化要领已经经取患上相称年夜乐成的范畴，提出高质量的情势化规范也是一项挑战，而 AI 体系特别面对着怪异的挑战。
3.1 难以情势化的使命
图 2 中 AEBS 节制器中的感知模块必需检测及分类对于象，从而将车辆及行人与其他实体区别开来。于经典的情势要领意义上，这个模块的正确性要求对于每一种类型的门路利用者及对于象举行情势界说，这是极为坚苦的。这类问题存于在这个感知模块的所有实现中，而不单单呈现于基在深度进修的要领中。其他触及感知及交流的使命也会呈现近似的问题，好比天然语言处置惩罚。那末，咱们怎样为如许的模块指定精度属性呢？规范语言应该是甚么？咱们可使用哪些东西来构建规范？
端到端/体系程度的规范（End-to-end/system-level specifications）。为了应答上述挑战，咱们可以对于这个问题略加变通。与其直接对于难以情势化的使命举行规范，不如起首专注在切确地指定 AI 体系的端到端举动。从这类体系程度的规范中，可以得到对于难以情势化的组件的输入-输出接口的约束。这些约束用作一个组件程度（component-level ）的规范，这个规范与整个 AI 体系的上下文相干。对于在图 2 中的 AEBS 示例，这触及对于属性 Φ 的划定，该属性即于运动历程中与任何对于象都连结最小间隔，从中咱们可患上出对于 DNN 输入空间的约束，于匹敌阐发中捕获语义上成心义的输入空间。
3.2 定量规范 vs. 布尔规范
传统上，情势规范往往是布尔型的，它将给定的体系举动映照为“真”或者“假”。然而，于 AI 及 ML 中，规范凡是作为规范成本或者奖励的方针函数给出。此外，可能有多个方针，此中一些必需一路满意，而另外一些则可能需要于某些情况中彼此衡量。同一布尔及定量两种规范要领的最好方式是甚么？是否有可以或许同一捕获 AI 组件常见属性（如鲁棒性及公允性）的情势？
混淆定量及布尔规范。布尔规范及定量规范都有其长处：布尔规范更易组合，但方针函数有助在用基在优化的技能举行验证及综合，并界说更邃密的属性满意粒度。填补这一差距的一种要领是转向定量规范语言，例如利用具备布尔及定量语义的逻辑（如器量时序逻辑），或者将主动机与 RL 的奖励函数相联合。另外一种要领是将布尔及定量规范组合成一个通用的规范布局，例如一本法则手册 ，手册中的规范可以按条理布局举行构造、比力及汇总。有研究已经经确定了 AI 体系的几类属性，包括鲁棒性、公允性、隐私性、问责性及透明度。研究者正于提出新的情势主义，将情势要领及 ML 的思惟接洽起来，以对于这些属性的变体（如语义鲁棒性）举行建模。
3.3 数据 vs. 情势要求
“数据即规范”的不雅点于呆板进修中很常见。有限输入集上标志的“真实”数据凡是是关在准确举动的独一规范。这与情势化要领很是差别，情势化要领凡是以逻辑或者主动机的情势给出，它界说了遍历所有可能输入的准确举动的调集。数据及规范之间的差距值患上留意，特别是当数占有限、有成见或者来自非专家时。咱们需要技能来对于数据的属性举行情势化，包括于设计时可用的数据及还没有碰到的数据。
规范挖掘(Specification mining)。 为了弥合数据及情势规范之间的差距，咱们建议利用算法从数据及其他不雅察中来揣度规范——即所谓的规范挖掘技能。此类要领凡是可用在 ML 组件，包括感知组件，由于于很多环境下，它不需要具备切确的规范某人类可读的规范。咱们还有可使用规范挖掘要领，从演示或者更繁杂的多个代办署理（人类及人工智能）之间的交互情势来揣度人类用意及其他属性。
4进修体系的建模于情势验证的年夜大都传统运用中，体系 S 于设计时是固定的且已经知的，好比它可所以一个步伐，或者者一个用编程语言或者硬件描写语言来描写的电路。体系建模问题重要触及的，是经由过程抽象失不相干的细节，来将 S 减小到更容易在处置惩罚的巨细。AI 体系给体系建模带来了很是差别的挑战，这重要源在呆板进修的利用：
高维输入空间
用在感知的 ML 组件凡是于很是高维的输入空间上运行。好比，一个输入的RGB 图象可所以 1000 x 600 像素，它包罗256((1000x600x3)) 个元素，输入凡是就是如许的高维向量流。只管研究职员已经经对于高维输入空间（如于数字电路中）利用了情势化要领，但基在 ML 的感知输入空间的性子是差别的，它不彻底是布尔值，而是混淆的，包括离散变量及持续变量。
高维参数/状况空间
深度神经收集等 ML 组件具备数千到数百万个模子参数及原始组件。例如，图 2 中利用的开始进的 DNN 有多达 6000 万个参数及数十层组件。这就孕育发生了巨年夜的验证搜刮空间，抽象历程需要很是细心。
于线顺应及进化
一些进修体系如利用 RL 的呆板人，会跟着它们碰到的新数据及新环境而发生进化。对于在如许的体系，设计时的验证必需思量体系举动的将来蜕变，或者者跟着进修体系的成长慢慢地于线履行。
于上下文中建模体系
对于在很多 AI/ML 组件，它们的规范仅仅由上下文来界说。例如，要验证图 2 中基在 DNN 的体系的安全性，就需要对于情况举行建模。咱们需要对于 ML 组件和其上下文举行建模的技能，以即可以验证于语义上成心义的属性。
最近几年来，很多事情都专注在提高效率，来验证 DNN 的鲁棒性及输入-输出属性。然而，这还有不敷，咱们还有需要于如下三个方面取患上进展：
主动抽象及高效暗示
主动天生体系的抽象一直是情势要领的要害，它于将情势要领的规模扩大到年夜型硬件及软件体系方面阐扬着至关主要的作用。为相识决基在 ML 的体系的超高维混淆状况空间及输入空间方面的挑战，咱们需要开发有用的技能来将 ML 模子抽象为更容易在情势阐发的、更简朴的模子。一些有但愿的标的目的包括：利用抽象注释来阐发 DNN，开发用在伪造有 ML 组件的收集物理体系的抽象，以和设计用在验证的新暗示（好比星集）。
注释与因果
假如进修者于其猜测中附上关在猜测是怎样从数据及配景常识中孕育发生的的注释，那咱们就能够简化对于进修体系举行建模的使命。这个设法其实不新鲜，ML 社区已经经对于诸如“基在注释的泛化”等术语举行了研究，可是近来，人们正于对于利用逻辑来注释进修体系的输出从头孕育发生了兴致。注释天生有助在于设计时调试设计及规范，并有助在合成鲁棒的 AI 体系以于运行时提供保障。包罗因果推理及反事实推理的 ML 还有可以帮忙天生用在情势要领的注释。
语义特性空间
当天生的匹敌性输入及反例于所利用的 ML 模子的上下文中具备语义意义时，ML 模子的匹敌性阐发及情势验证就更成心义。例如，针对于汽车颜色或者一天中时间的微小变化来阐发 DNN 对于象检测器的技能，比向极少量肆意选择的像素添加噪声的技能更有效。当前，年夜大都的要领于这一点上都还有达不到要求。咱们需要语义匹敌阐发，即于ML 模子所属体系的上下文中对于它们举行阐发。此中额的一个要害步调，是暗示对于 ML 体系运行的情况建模的语义特性空间，而不是为 ML 模子界说输入空间的详细特性空间。这是切合直觉的，即与完备的详细特性空间比拟，详细特性空间于语义上成心义的部门（如交通场景图象）所形成的潜于空间要低患上多。图 2 中的语义特性空间是代表主动驾驶汽车周围 3D 世界的低维空间，而详细的特性空间是高维像素空间。因为语义特性空间的维数较低，是以可以更易地举行搜刮。可是，咱们还有需要一个“衬着器”，将语义特性空间中的一个点映照到详细特性空间中的一个点。衬着器的属性如可微性（differentiability），可以更易地运用情势化要领来履行语义特性空间的方针导向搜刮。
5用在设计及验证的计较引擎硬件及软件体系情势化要领的有用性，是由底层“计较引擎”的前进鞭策的——例如，布尔可满意性求解 (SAT)、可满意性模理论 (SMT) 及模子查抄。鉴在 AI/ML 体系范围、情况繁杂性及所触及的新型规范，需要一类新的计较引擎来举行高效且可扩大的练习、测试、设计及验证，实现这些前进必需降服的要害挑战。
5.1 数据集设计
数据是呆板进修的基本出发点，提高 ML 体系质量就必需提高它所进修数据的质量。情势化要领怎样帮忙 ML 数据体系地选择、设计及扩充？
ML 的数据天生与硬件及软件的测试天生问题有相似的地方。情势化要领已经被证实对于体系的、基在约束的测试天生是有用的，但这与对于人工智能体系的要求差别，约束类型可能要繁杂患上多——例如，对于利用传感器从繁杂情况（如交通状态）捕捉的数据的“真实性”举行编码要求。咱们不仅需要天生具备特定特性的数据项（如发明过错的测试），还有需要天生满意漫衍约束的调集；数据天生必需满意数据集巨细及多样性的方针，以举行有用的练习及泛化。这些要求都需要开发一套新的情势化技能。
情势要领中的受控随机化。数据集设计的这个问题有许多方面，起首必需界说“正当”输入的空间，以便按照运用步伐语义准确形成示例；其次，需要捕捉与实际世界数据相似性器量的约束；第三，凡是需要对于天生的示例的漫衍举行约束，以得到进修算法收敛到真实观点的包管。
咱们信赖这些方面可以经由过程随机情势要领来解决——用在天生受情势约束及漫衍要求的数据的随机算法。一类称为节制即兴创作的新技能是颇有远景的，即兴创作的天生要满意三个约束的随机字符串（示例）x：
界说正当x空间的硬约束
一个软约束，界说天生的x必需怎样与真实世界的示例相似
界说输出漫衍约束的随机性要求
今朝，节制即兴理论仍处在起步阶段，咱们才方才最先相识计较繁杂性并设计有用的算法。反过来，即兴创作依靠在计较问题的最新进展，例践约束随机抽样、模子计数及基在几率编程的天生要领。
5.2 定量验证
除了了经由过程传统指标（状况空间维度、组件数目等）权衡AI 体系范围以外，组件的类型可能要繁杂患上多。例如，自立及半自立车辆和其节制器必需建模为混淆动力体系，联合离散及持续动力学；此外，情况中的代表（人类、其他车辆）可能需要建模为几率历程。末了，需求可能不仅触及传统关在安全性及活性的布尔规范，还有包括对于体系鲁棒性及机能的定量要求，然而年夜大都现有的验证要领，都是针对于回覆布尔验证问题。为相识决这一差距，必需开发用在定量验证的新可扩大引擎。
定量语义阐发。一般来讲，人工智能体系的繁杂性及异构性象征着，规范的情势验证（布尔或者定量）是不成判断的——例如，即即是确定线性混淆体系的状况是否可达，也是不成判断的。为了降服计较繁杂性带来的这一障碍，人们必需于语义特性空间上利用几率及定量验证的新技能，以加强本节前面会商的抽象及建模要领。对于在同时具备布尔及定量语义的规范情势，于诸如器量时间逻辑之类的情势中，将验证表述为优化，对于在同一来自情势要领的计较要领及来自优化文献的计较要领至关主要。例如于基在模仿的时间逻辑证伪中，只管它们必需运用在语义特性空间以提高效率，这类伪造技能也可用在体系地、匹敌性地天生 ML 组件的练习数据。几率验证的技能应该逾越传统的情势，如马尔科夫链或者MDPs，以验证语义特性空间上的几率步伐。一样，关在SMT求解的事情必需扩大到更有用地处置惩罚成本约束--换句话说，将SMT求解与优化要领相联合。
咱们需要相识于设计时可以包管甚么，设计历程怎样有助在运行时的安全操作，以和设计时及运行时技能怎样有用地互操作。5.3 AI/ML 的组合推理
对于在扩大到年夜型体系的正式要领，组合（模块化）推理是必不成少的。于组合验证中，一个年夜型体系（例如，步伐）被拆分为它的组件（例如，步伐），每一个组件都按照规范举行验证，然后组件规范一路孕育发生体系级规范。组合验证的一个常见要领是利用假定-包管合同，例如一个历程假定一些关在它的最先状况（前置前提），反过来又包管其竣事状况（后置前提），近似的假定-包管范式已经被开发并运用在并发的软件及硬件体系。
然而，这些范式其实不涵盖人工智能体系，这于很年夜水平上是因为 情势化规范 一节中会商的人工智能体系的规范化挑战。组合式验证需要组合式规范——也就是说，组件必需是可情势化的。然而，正如“情势化规范”中所述，可能没法正式指定一个感知组件的准确举动。是以，挑战之一就是开发不依靠在有完备组合规范的组合推理技能。此外，人工智能体系的定量及几率性子，要求将组合推理的理论扩大到定量体系及规范。
揣度组件合同。人工智能体系的组合式设计及阐发需要于多个方面取患上进展。起首，需要于一些有远景的开端事情基础上，为这些体系的语义空间开发几率包管设计及验证的理论。第二，必需设计出新的概括技能，以算法方式天生假定-包管合同，削减规范承担并促成组合推理。第三，为了处置惩罚诸如感知等没有切确正式规格的组件的环境，咱们提出了从体系级阐发中揣度组件级约束的技能，并利用这类约束将组件级阐发，包括匹敌性阐发，集中于搜刮输入空间的 相干 部门。
6建构中批改智能体系于抱负的世界中，验证将与设计历程相联合，是以体系是“于建构中批改的”。例如，验证可以与编译/合成步调交错举行，假定于集成电路中常见的寄放器传输级（RTL）设计流程中，也许它可以被集成到合成算法中，以确保实现满意规范。咱们能不克不及为人工智能体系设计一个适合的于建构中慢慢批改的设计流程？
6.1 ML 组件的规范驱动设计
给定一个正式的规范，咱们可否设计一个可证实满意该规范的呆板进修组件（模子）？这类全新的 ML 组件设计有许多方面：（1）设计数据集，（2） 综合模子的布局，（3）天生一组有代表性的特性，（4） 综合超参数及 ML 算法选择的其他方面，以和（5）于综合掉败时主动化调试 ML 模子或者规范的技能。
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 体系的五个重要挑战，并对于这五项挑战中的每一一项都制订了三项设计及验证原则，这些原则有但愿解决这个挑战。
图 3 中的边显示了这些原则之间的依靠瓜葛，例如运行时包管依靠在自省及数据驱动的情况建模，以提取可监测的假定及情况模子。一样，为了举行体系级阐发，咱们需要举行组合推理及抽象，此中一些 AI 组件可能需要挖掘规范，而其他组件则经由过程情势化的概括构建天生准确的布局。
自 2016 年以来，包括作者于内的几位研究职员一直致力在应答这些挑战，其时本文已经发表的原始版本先容了一些样本进展。咱们已经经开发了开源东西 VerifAI 及 Scenic，它们实现了基在本文所述原则的技能，并已经运用在主动驾驶及航空航天范畴的工业范围体系。这些结果只是一个最先，还有有许多工作要做。于将来的几年里，可验证 AI 有望继承成为一个富有成效的研究范畴。
原文链接：https://cacm.acm.org/magazines/2022/7/262079-toward-verified-artificial-intelligence/fulltext
雷峰网(公家号：雷峰网)雷峰网版权文章，未经授权禁止转载。详情见转载须知。
-米兰·(milan)中国官方网站
