麻省理工学院林肯实验室的一项研究表明，尽管形式规范具有数学精度，但人类不一定可以解释它。
人类很难使用形式规范来验证人工智能行为，这表明理论主张与实际理解之间存在差异。
研究结果强调需要对人工智能的可解释性进行更现实的评估。
随着自主系统和人工智能在日常生活中变得越来越普遍，新的方法正在出现，帮助人类检查这些系统是否按预期运行。
有一种称为形式化规范的方法：使用可以转换为自然语言表达式的数学公式。
一些研究人员声称，这种方法可以用来以人类可以解释的方式阐明人工智能将做出的决定。
麻省理工学院林肯实验室的研究人员表明了相反的观点：形式化规范似乎无法被人类解释。该小组的论文被本月初举行的 2023 年智能机器人与系统国际会议接收。
可解释性
可解释性很重要，因为它让人类在现实世界中使用机器时能够信任机器。如果机器人或人工智能可以解释其行为，那么人类就可以决定是否需要调整或可以相信它会做出公平的决定。
然而，可解释性长期以来一直是人工智能和自治领域的一个挑战。机器学习过程发生在“黑匣子”中，因此模型开发人员通常无法解释系统为何或如何做出特定决策。
形式规范
形式规范是更广泛的形式方法集的一部分，这些方法使用逻辑表达式作为数学框架来描述模型的行为。
由于模型是建立在逻辑流程上的，因此工程师可以使用“模型检查器”以数学方式证明有关系统的事实，包括系统何时可能或不可能完成任务。
但是这些研究人员混淆了形式规范具有精确语义和人类可以解释的事实，两者不是同一回事。