麻省理工学院林肯实验室的一项研究表明，尽管形式规范具有数学精度，但对人类来说不一定是可理解的。参与者努力使用这些规范来验证人工智能行为，这表明理论主张与实际理解之间存在差异。研究结果强调，需要对人工智能的可解释性进行更现实的评估。

一些研究人员将正式规范视为汽车的一种方式向人类“解释自己”的无名系统。但一项新的研究发现，我们并没有理解这一点。

随着自主系统和人工智能在日常生活中变得越来越普遍，帮助人类检查这些系统是否按预期运行的新方法正在出现。一种称为形式规范的方法使用可以翻译成自然语言表达式的数学公式。一些研究人员声称，这种方法可以用来阐明人工智能将以人类可理解的方式做出的决定。

可解释性研究成果

麻省理工学院林肯实验室的研究人员想要验证这种可解释性的说法。他们的发现指向了相反的方向:人类似乎无法解释正式的规范。在该团队的研究中，参与者被要求检查人工智能代理的计划是否会在虚拟游戏中成功。在计划的正式说明面前，参与者的正确率不到一半。

一项研究发现，人类很难理解正式规范的输出，一些研究人员声称，这种方法可以用来让人工智能的决策对人类来说是可解释的。来源:Bryan Mastergeorge

对于那些一直声称形式方法赋予系统可解释性的研究人员来说，这一结果是个坏消息。在某些有限和抽象的意义上，这可能是正确的，但对于任何接近实际系统验证的东西来说，这都是不正确的，”该实验室人工智能技术小组的研究员霍西·肖(Hosea Siu)说。该小组的论文被本月早些时候举行的2023年智能机器人与系统国际会议接受。

的即时通讯可解释性的重要性

可解释性很重要，因为它允许人们在现实世界中使用机器时信任机器。如果机器人或人工智能可以解释自己的行为，那么人类就可以决定它是否需要调整，或者是否可以信任它做出公平的决定。可解释的系统还使技术的用户(不仅仅是开发人员)能够理解并信任其功能。然而，可解释性一直是人工智能和自治领域的一个挑战。机器学习过程发生在“黑匣子”中，因此模型开发人员通常无法解释系统为什么或如何做出特定决定。

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

翻译规范的挑战

在他们的实验中，研究人员试图确定正式规范是否使系统的行为更易于解释。他们关注的是人们使用这些规范来验证系统的能力——也就是说，了解系统是否总是满足用户的目标。

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

“研究人员混淆了正式规范具有精确语义的事实，以及它们对人类的可解释性。这不是一回事。”“我们意识到，几乎没有人检查人们是否真正理解了输出。”

在团队的实验中，参与者被要求验证一组相当简单的行为，让机器人玩夺旗游戏，基本上是回答一个问题:“如果机器人严格遵守这些规则，它是否总是赢?”

参与者包括正式方法方面的专家和非专家。他们以三种方式获得正式的规范——一个“原始的”逻辑公式，一个被翻译成更接近自然语言的单词的公式，以及一个决策树格式。在人工智能领域，决策树通常被认为是一种人类可解释的方式，用于展示人工智能或机器人的决策。

结果是:“验证的表现总体上非常糟糕，准确率在45%左右，无论演示类型如何，”Siu说。

校检自信和误解

那些之前接受过正式规范培训的人只比新手稍微好一点。然而，专家们对他们的答案更有信心，不管他们是否正确。总的来说，人们倾向于过度信任摆在他们面前的规范的正确性，这意味着他们忽略了可能导致游戏失败的规则集。研究人员说，这种确认偏差对于系统验证尤其令人担忧，因为人们更有可能忽略失效模式。

“我们不认为这个结果意味着我们应该放弃作为向人们解释系统行为的一种方式的正式规范。但我们确实认为，在设计如何将它们呈现给人们以及人们使用它们的工作流程方面，还需要做更多的工作。”

在考虑为什么结果如此糟糕时，Siu认识到，即使是研究正式方法的人也没有受过足够的培训，无法按照实验要求检查规范。而且，考虑一套规则的所有可能结果是困难的。即便如此，向参与者展示的规则集也很短，相当于不超过一段文字，“比你在任何真实系统中遇到的任何规则都短得多，”Siu说。

该团队并没有试图将他们的结果直接与人类在现实世界机器人验证中的表现联系起来。相反，他们的目标是将结果作为一个起点，考虑形式逻辑团体在声称可解释性时可能遗漏了什么，以及这种说法如何在现实世界中发挥作用。

未来影响及研究

这项研究是Siu和他的队友们正在进行的一个更大项目的一部分，该项目旨在改善机器人和人类操作员之间的关系，尤其是在军队中。机器人编程的过程常常会让操作员置身于循环之外。为了提高可解释性和信任度，该项目正试图让操作员以类似于训练人类的方式，直接向机器人传授任务。这样既可以提高操作者对机器人的信心，又可以提高机器人的适应性。

最终，他们希望这项研究的结果以及他们正在进行的研究可以更好地应用自主性，因为它越来越融入人类生活和决策。

Siu补充说:“我们的研究结果推动了对某些系统、自主和人工智能概念进行人类评估的必要性，而不是对它们对人类的效用提出太多的要求。”

参考:“STL:令人惊讶的复杂逻辑(用于系统验证)”，作者:Ho Chit Siu, Kevin Leahy和Makai Mann, 2023年5月26日，计算机科学b>人工智能。arXiv: 2305.17258

分享 推特 REDDIT 电子邮件 分享

更多关于sciitechdaily

技术

---

生物学

---

健康

---

空间

---

地球

---

技术

---

科学

---

技术

---