迈克尔费斯菲斯尔是一名计算机科学教授，专门从事逻辑方法和自动正式验证，以及多学科的主任自动系统技术中心金宝博官方在利物浦大学并且是逻辑和计算组在计算机科学系。
Fisher教授也是两个人BCS.和专业，也是英国计算研究委员会金宝博娱乐。他是该部门的主席工业联络委员会。
卢克·穆罕沃斯:在“验证自治系统金宝博官方“（2013年），您和您的共同作者总结了最近的一些方法来正式验证自治系统。金宝博官方在一个点，你写道：
许多自主系统，包括无人驾驶飞机，金宝博官方机器人，卫星，甚至纯粹的软件应用程序，具有类似的结构，即分层架构，如图1所示。虽然纯粹的连接主人/子符号架构在某些领域仍然普遍，例如机器人，广泛认识到将重要/困难的选择分成可识别的实体，对开发，调试和分析非常有用。虽然这样的分层架构已经被调查多年，但它们在自治系统中越来越常见。金宝博官方
附图为:
你认为“典型的混合自主系统架构”有多普遍?金宝博官方例如，你认为这种架构是在20个不同的现实世界应用程序中使用，还是200个不同的现实世界应用程序，或者可能更多?你认为现在有支持这种建筑的趋势吗?你认为在机器人领域是否也有这种架构的趋势?
迈克尔费斯菲斯尔：很难获得关于自治系统的内部架构的明确证据，特别是商业系统的内部架构，因此我只有有关以这种方式构建的系统的轶事信息。金宝博官方然而，从我与工程师（航空航天和汽车）的工程师的讨论来看，似乎这种建筑的使用正在增加。它可能不会被称为“代理架构”，实际上，“决策者”可能不会被称为“代理人”，而是具有单独的“执行”或“控制模块”的系统，该系统明确地处理高级决策，金宝博官方适合我们的模型。
我不确定机器人架构是否也在朝着这个方向发展，但似乎有一个主题是增加一个“监控器”或“管理者”，可以在机器人采取行动之前评估拟议行动的安全性或道德1那2。或者，这可以被视为制作高级决策的附加代理（该方法允许什么），因此这种方法也可以被视为各种混合代理架构。
路加福音：在同样的论文中，你和你的共同作者解释了这一点
因为自主软件必须自己做决定，所以不仅要知道软件做什么，什么时候做，还要知道它是什么为什么软件选择这样做。
在复杂的动态系统中捕捉这种自主行为的一个非常有用的抽象概念被证明是代理的概念。金宝博官方自从代理概念在20世纪80年代出现以来，在学术界和产业界都有了巨大的发展。现在已经很清楚了，这个代理比喻对于捕获许多实际情况非常有用，这些情况涉及由灵活、自治和分布式组件组成的复杂系统。金宝博官方本质上，主体必须从根本上具备灵活自主的行为能力。
但是，它依靠自己的“代理”概念仍然不够！金宝博官方由神经网络，遗传算法和复杂的控制系统控制的系统可以自主行动，从而称为代理，但他们行动的原因通常是不透明的。因此，这种系统非常难以开发，控制和分析。金宝博官方
所以，一个概念合理的代理人变得更受欢迎。再次，有许多变化，但我们认为这是一个代理人做出选择是否有明确的理由，如果有必要，是否应该解释这些原因。
我之前研究过不同AI方法的相对透明度安全关键系统中的透明度金宝博官方在那里我问:
方法的透明度如何随比例变化?一个有200个规则的逻辑AI可能比一个有200个节点的贝叶斯网络更透明，但是如果我们比较10万个规则和10万个节点呢?至少我们可以查询贝叶斯网问“它相信X的东西，”虽然我们不一定与基于逻辑的系统一起这样做。金宝博官方
你认为理性代理模型的透明度会有多大?或者，您是否认为未来自治系统的“理性代理”部分将保持相当小(例如，使其透明化和验证)，即使在体系结构中较低“层”的子系统可能会在金宝博官方复杂性上大幅增长?
迈克尔：我会说，即使他们的数字增加，理性代理商内的高级规则仍然相对透明。这只是证据/分析机制不太规划。
因此，如您所建议的那样，意图是保持理性代理部分尽可能小。正式验证非常昂贵，因此对非常大的代理商的任何验证都可能是不可行的。
通过只处理高级的、理性的代理决策，我们旨在避免处理整个系统的巨大状态空间。金宝博官方逻辑(特别是BDI)规则的使用将我们从低级别的细节中抽象出来。
关于您关于“100,000条规则vs. 100,000个节点”的问题，我希望所使用的符号逻辑语言能够帮助我们将规则减少到1000条，甚至100条(vs. 100,000个节点)。
路加福音：您的分层自治系统方法是否具有信念 - 欲望 - 意向理性的代理“顶部”金宝博官方，与混合动力系统控金宝博官方制方法，或者是混合系统控制方法的替代方案吗？金宝博官方
迈克尔是的，它与混合系统方法相结合，当然，连续和随机方面对于模拟现实世界的交互金宝博官方作用很重要。您可以将我们的方法看作是提供关于混合系统中离散步骤的进一步细节。金宝博官方
路加福音:在未来，您认为在层次自治系统的顶层角色中的逻辑代理规范最终需要被更灵活、概率/模糊的推理方法所取代，以更好地匹配环境吗?金宝博官方或者，当我们构建类似人类的、完全通用的推理和规划能力的系统(几十年后)时，逻辑代理规范能否扮演这个角色?金宝博官方
迈克尔： 后者。我们正在努力在这个顶级指定和验证概率，甚至是实时代理行为。（目前我们可以做代理验证或概率验证，但我们正在开发组合机制。）由于应用程序的复杂性发展，并且可能融合不同的推理和决策组件，高级代理可能会变得越来越复杂。我们目前的方法是规划组件在单独的低级，模块中。代理只是拨打这些，然后在制作的计划选项之间做出决定。
路加福音:有趣。你能说说你正在研究的组合机制吗?
迈克尔:正式验证基本逻辑属性已经很困难了。然而，一旦我们处理可能在实际情况中使用的自治系统，那么我们通常会导致更金宝博官方复杂的逻辑查询。例如，假设我们希望验证一个属性，例如
当被问及问题时，机器人在30秒内回复的概率至少为80%
我们已经超越了基本属性，融入了概率(>80%)和实时方面(30秒内)。但是，对于自主系统，我们不仅要验证系统(比金宝博官方如机器人)的功能，还要验证它的意图和信念。我们甚至可以验证一下
当被问及这个问题时，机器人认为已经发出请求并打算在30秒内回复的概率至少为80%
这里的问题是，我们需要描述这些需求的逻辑框架已经相当复杂了。逻辑的组合往往是很难处理的，概率、实时、意图、信念等逻辑的组合还没有得到很详细的研究。
我们旨在发展和扩展一些理论我们一直在做的工作论复杂逻辑组合的模型检查，以解决更全面的自主系统验证问题。金宝博官方
路加福音:谢谢,迈克尔!
- 阿金,r .”治理致命行为：在混合审议/反应机器人架构中嵌入道德”。技术报告Git-GVU-07-11，佐治亚理工学院，2007年。↩
- Woodman，R.，Winfield，A.，Harper，C.和Fraser，M。“构建更安全的机器人:安全驱动控制”。机械工程学报，37(12):1 - 6,2012。金宝博娱乐↩
你喜欢这个帖子吗?你可以享受我们的另一个谈话的帖子,包括:
