随着自主系统和人工智能在日常生活中变得越来越普遍，新的方法正在出现，以帮助人类检查这些系统是否按预期运行。一种方法称为形式规范，它使用可以转换为自然语言表达式的数学公式。一些研究人员声称，这种方法可用于阐明人工智能将以人类可解释的方式做出的决定。
麻省理工学院林肯实验室的研究人员希望验证这种可解释性的说法。他们的研究结果恰恰相反：人类似乎无法解释形式规范。在该团队的研究中，参与者被要求检查人工智能代理的计划是否会在虚拟游戏中成功。在出示计划的正式规范时，参与者只有不到一半的时间是正确的。
“对于一直声称形式化方法为系统提供可解释性的研究人员来说，这些结果是个坏消息。在某种受限制和抽象的意义上，它可能是正确的，但对于任何接近实际系统验证的东西来说，都不是这样，“该实验室人工智能技术小组的研究员Hosea Siu说。该小组的论文被本月早些时候举行的2023年智能机器人与系统国际会议接受。
可解释性很重要，因为它允许人类在现实世界中使用机器时信任机器。如果机器人或人工智能可以解释其行为，那么人类就可以决定它是否需要调整，或者可以信任它做出公平的决定。可解释的系统还使技术用户（而不仅仅是开发人员）能够理解和信任其功能。然而，可解释性长期以来一直是人工智能和自主领域的一个挑战。机器学习过程发生在一个“黑匣子”中，因此模型开发人员通常无法解释系统为什么或如何做出某个决定。
“当研究人员说'我们的机器学习系统是准确的'时，我们会问'有多准确？'和'使用什么数据？'如果没有提供这些信息，我们就会拒绝这种说法。当研究人员说'我们的机器学习系统是可解释的'时，我们并没有做那么多，我们需要开始对这些说法进行更多的审查，“Siu说。
迷失在翻译中
在他们的实验中，研究人员试图确定形式规范是否使系统的行为更具可解释性。他们关注的是人们使用这些规范来验证系统的能力，也就是说，了解系统是否总是满足用户的目标。
为此目的应用正式规范本质上是其原始用途的副产品。形式规范是一组更广泛的形式化方法的一部分，这些方法使用逻辑表达式作为数学框架来描述模型的行为。由于模型是建立在逻辑流之上的，因此工程师可以使用“模型检查器”以数学方式证明有关系统的事实，包括系统何时可以或不可能完成任务。现在，研究人员正试图使用相同的框架作为人类的翻译工具。
“研究人员混淆了这样一个事实，即形式规范具有精确的语义，而它们可以被人类解释。这些不是一回事，“萧说。“我们意识到，几乎没有人在检查人们是否真正理解了输出。
在团队的实验中，参与者被要求用机器人玩夺旗游戏来验证一组相当简单的行为，基本上回答了“如果机器人完全遵循这些规则，它总是赢吗？
与会者包括正规方法的专家和非专家。他们以三种方式获得正式规范——“原始”逻辑公式、翻译成更接近自然语言的单词的公式以及决策树格式。特别是决策树，在人工智能世界中通常被认为是一种人类可解释的方式来展示人工智能或机器人的决策。
结果：“总体上，验证性能非常糟糕，无论演示类型如何，准确率都在 45% 左右，”Siu 说。
自信地错了
那些以前接受过正式规范培训的人只比新手做得稍微好一点。然而，专家们报告说，无论他们的答案是否正确，他们的信心都要大得多。总体而言，人们倾向于过度信任摆在他们面前的规范的正确性，这意味着他们忽略了允许游戏失败的规则集。研究人员说，这种确认偏差对系统验证尤其令人担忧，因为人们更有可能忽略故障模式。
“我们不认为这个结果意味着我们应该放弃正式规范作为向人们解释系统行为的一种方式。但我们确实认为，在设计它们如何呈现给人们以及人们使用它们的工作流程方面，需要做更多的工作，“Siu补充道。
在考虑为什么结果如此糟糕时，Siu认识到，即使是从事形式化方法研究的人也没有完全按照实验的要求检查规范。而且，考虑一套规则的所有可能结果是困难的。即便如此，向参与者展示的规则集也很短，相当于不超过一段文字，“比你在任何真实系统中遇到的任何东西都要短得多，”Siu说。
该团队并没有试图将他们的结果直接与人类在现实世界机器人验证中的表现联系起来。相反，他们的目标是以结果为起点，考虑形式逻辑社区在声明可解释性时可能缺少什么，以及这些声明在现实世界中如何发挥作用。
这项研究是Siu和队友们正在研究的一个更大项目的一部分，该项目旨在改善机器人与人类操作员之间的关系，尤其是军队中的机器人。机器人编程过程通常会使操作员置身事外。为了提高可解释性和信任度，该项目正试图允许操作员以类似于训练人类的方式直接向机器人传授任务。这样的过程可以提高操作员对机器人的信心和机器人的适应性。
最终，他们希望这项研究的结果和他们正在进行的研究能够更好地应用自主性，因为它越来越深入人类生活和决策。
“我们的研究结果推动需要对某些系统以及自主和人工智能的概念进行人工评估，然后再对它们对人类的效用提出太多要求，”Siu补充道。