研究发现，形式规范这种方法可能并不容易被人们理解，而一些研究人员声称这种方法可以使人类能够解释人工智能的决策。麻省理工学院的研究人员对这种可解释性的说法进行了验证，结果恰恰相反：形式规范似乎不容易被人类理解。在研究中，参与者被要求判断一个人工智能代理的计划是否能在虚拟游戏中成功。当参与者对形式规范做出判断时，他们的正确率不到一半。

该实验室人工智能技术小组的研究员Hosea Siu说：“这些结果对那些一直声称形式规范为系统提供了可解释性的研究人员来说是个坏消息。在某种程度和意义上形式规范可能能够让人类理解，但从实际系统验证来说这种方法并不准确。”

实际应用中的可解释性很重要，因为它可以使人们信任使用的机器。如果机器人或人工智能可以解释自己的行为，人类就可以决定是否需要进行调整或者是否可以信任其做出的决策。可解释的系统也能够使技术的用户（不仅仅是开发者）理解并信任其能力。然而，可解释性长期以来一直是人工智能和自主性领域面临的挑战。机器学习是在一个“黑盒子”中进行的，因此模型的开发者通常无法解释系统为什么或者如何做出某个决策。

“当研究人员说‘我们的机器学习系统是准确的’时，我们会问‘准确程度如何？’和‘使用什么数据？’如果没有提供这些信息，我们会拒绝这个说法。当研究人员说‘我们的机器学习系统是可解释的’时，我们需要开始对这些说法进行更多的审查，”Siu说。

迷失在翻译中

在他们的实验中，研究人员希望确定形式规范是否使系统的行为更具可解释性。他们关注的是人们使用此类规范来验证系统的能力，也就是说，了解系统是否始终满足用户的目标。

为此目的应用形式规范本质上是其原始用途的副产品。形式规范是形式方法的一部分，使用逻辑表达式作为数学框架来描述模型的行为。由于模型是基于逻辑流程构建的，工程师可以使用“模型检查器”来从数学上证明系统的事实，包括系统何时能够完成任务或不能完成任务。现在，研究人员正试图将这个框架作为人类的翻译工具。

Siu说：“研究人员混淆了形式规范具有精确语义和能够被人类解释，事实上，这两者不是一回事。”“我们意识到，几乎没有人检查人们是否真的理解了输出。”

参与者包括形式规范方面的专家和非专家。他们通过三种方式获得形式规范——“原始”逻辑公式、翻译成更接近自然语言的单词的公式和决策树格式。决策树经常被认为是一种能够被人类解读的展示人工智能或机器人决策过程的方式。

结果是：“无论演示类型如何，验证性能总体上都非常糟糕，准确率约为45%，”Siu说。

自信地错了

那些之前接受过形式规范培训的人，与新手相比只表现得稍微好一点。然而，无论他们的答案正确与否，专家们都表现出更高的自信。总的来说，人们倾向于过度相信摆在他们面前的规范的正确性，从而忽视了允许失败的规则集。研究人员表示，这种确认偏差对系统验证特别令人担忧，因为人们更有可能忽视失败模式。

“我们不认为这个研究结果意味着我们应该放弃使用形式规范来向人们解释系统的行为。但我们确实认为，在向人们展示规范的方式以及人们使用它们的工作流程方面，还需要进行更多的设计工作，”Siu补充道。

在考虑为什么结果如此糟糕时，Siu认识到，即使是从事形式规范工作的人也没有被训练得能够像实验要求的那样检查规范。而且，考虑到一个规则集的所有可能结果是困难的。即便展示给参与者的规则集很短，不超过一段文字的长度，“比你在任何真实系统中遇到的任何东西都短得多，”Siu说。

该团队并未试图直接将他们的结果与人类在现实世界中的机器人验证表现联系起来。相反，他们的目标是以此为起点，思考形式逻辑社区在声称可解释性时可能会忽视哪些因素，以及这样的声称可能在现实世界中如何发挥作用。

这项研究是Siu和他的团队为改善机器人与人类操作员之间的关系而进行的大型项目的一部分，尤其是那些在军事领域工作的人。编程机器人的过程通常会将操作员排除在外。该项目旨在提高可机器人的解释性和可信度，让操作员直接教授任务给机器人，类似于培训人类。这样的过程可以提高操作员对机器人的信心和机器人的适应性。

最终，他们希望这项研究的结果和他们正在进行的研究能够更好地应用自主性，随着它在人类生活和决策中的嵌入变得更加普遍。

“我们的研究结果强调了在对自主性和人工智能的某些系统和概念进行过多宣传之前，需要对其实用性进行人类评估的必要性，”Siu补充道。