Michael Fisher对自动系统的验证亚博体育苹果app官方下载

路加福音Muehlhauser:在“验证自治系统亚博体育苹果app官方下载(2013)，你和你的合著者总结了一些最近正式验证自主系统的方法。亚博体育苹果app官方下载有一次，你写道:

许多自主系统，包括无人驾驶飞机、亚博体育苹果app官方下载机器人、卫星，甚至纯软件应用，都具有类似的结构，即如图1所示的分层结构。虽然纯粹的连接主义/次符号架构在一些领域(如机器人)仍然很流行，但有一个广泛的认识，即将重要/困难的选择分离到一个可识别的实体中，对于开发、调试和分析非常有用。虽然这种分层架构已经被研究了很多年，但它们在自治系统中越来越普遍。亚博体育苹果app官方下载

附图为:

你认为“典型的混合自主系统架构”有多普遍?亚博体育苹果app官方下载例如，你认为这种架构在大约20个不同的现实世界的应用程序中使用，还是在大约200个不同的现实世界的应用程序中使用，或者更多?你认为有一种倾向于这样的架构吗?你认为在机器人领域是否也会出现这样的架构趋势?

迈克尔·费雪很难获得关于自主系统的内部架构的确切证据，尤其是商业系统，所以我只有关于以这种方式构建的系统的轶事信息。亚博体育苹果app官方下载然而，从我与学术界和工业界(航空航天和汽车)的工程师的讨论来看，这类架构的使用似乎正在增加。它可能不被称为“代理体系结构”，实际上“决策者”可能根本就不被称为“代理”，但具有一个单独的“执行”或“控制模块”的系统，显式地处理高层决策，适合我们的模型。亚博体育苹果app官方下载

我不确定机器人架构是否也在朝着这个方向发展，但似乎有一个主题是增加一个“监视器”或“管理者”，可以在机器人采取行动之前评估拟议行动的安全性或道德性^1，2．这也可以看作是另一个做高级决策的代理(允许什么，阻止什么)，因此这种方法也可以看作是各种混合代理体系结构。

路加福音在同一篇论文中，你和你的合著者解释了这一点

由于自动软件必须自己做决定，因此不仅要知道软件做什么、什么时候做，而且还要知道它在做什么为什么软件选择这样做。

在复杂的动态系统中捕捉这种自主行为的一个非常有用的抽象就是代理的概念。亚博体育苹果app官方下载自20世纪80年代代理概念崭露头角以来，在学术界和产业界都有了长足的发展。很明显，这个代理的比喻对于捕捉包含灵活、自治和分布式组件的复杂系统的许多实际情况非常有用。亚博体育苹果app官方下载从本质上说，代理必须从根本上具备灵活自主行动的能力。

然而，事实证明，仅凭“代理”的概念是不够的!亚博体育苹果app官方下载由神经网络、遗传算法和复杂控制系统等控制的系统都可以自主行动，因此被称为代理，但它们行动的原因往往相当不透明。正因为如此，这样的系统很难开发、控制和分析。亚博体育苹果app官方下载

a的概念理性的代理变得越来越受欢迎。这里有很多变化，但我们认为这是一种动因有明确的理由做出选择，并应能够解释这些，如果必要的话．

我之前探讨了不同AI方法的相对透明度安全关键系统的透明度亚博体育苹果app官方下载我问:

方法的透明度如何随比例变化?200条规则的逻辑AI可能比200个节点的贝叶斯网络更透明，但如果我们比较100000条规则和100000个节点呢?至少我们可以查询贝叶斯网络询问“它相信X的什么”，而我们在基于逻辑的系统中不一定能做到这一点。亚博体育苹果app官方下载

您对Rational Agent模型透明度将缩放的透明度有何看法是什么？或者，您认为未来自治系统的“理性代理”部分将保持相当小的（例如，实现透明度和验证），即使架构中的较低“层”的子系统可能会在复杂性亚博体育苹果app官方下载中大规模生长？

迈克尔我想说的是，即使在理性个体数量增加的情况下，理性个体内部的高层规则仍然相对透明。只是证明/分析机制的伸缩性不是很好。

所以，正如你所说，目的是让理性主体部分尽可能小。正式的核查是相当昂贵的，因此任何对非常大的代理人的核查都可能是不可行的。

通过只处理高层次的、理性的agent决策，我们的目标是避免处理整个系统的巨大状态空间。亚博体育苹果app官方下载逻辑(特别是BDI)规则的使用将我们从许多低级细节中抽象出来。

关于你关于“100,000规则vs. 100,000节点”的问题，我希望所使用的符号逻辑语言能够帮助我们将规则减少到1000甚至100条(vs. 100,000节点)。

路加福音:你的层级自治系统方法，在“顶部”有一个信念-愿望-意图的理性代理，是否亚博体育苹果app官方下载与混合动力系统控亚博体育苹果app官方下载制方法，或者它会成为混合系统控制方法的替代品?亚博体育苹果app官方下载

迈克尔是的，它与混合系统方法相结合，当然，连续和随机方面对于模拟真实世界的交互亚博体育苹果app官方下载作用很重要。你可以看到我们的方法提供了更多关于混合系统中离散步骤的细节。亚博体育苹果app官方下载

路加福音:在未来，你认为在层次自治系统中扮演顶级角色的逻辑代理规范最终需要被一种更灵活、概率/模糊的推理方法所取代，从而更好地匹配环境吗?亚博体育苹果app官方下载或者，逻辑代理规范能否在我们构建接近人类的系统(从现在起几十年)时发挥这种作用?亚博体育苹果app官方下载

迈克尔:后者。我们正致力于能够在这个顶层指定和验证概率的，甚至是实时的代理行为。(目前我们既可以做代理验证也可以做概率验证，但我们正在开发组合机制。)随着应用程序的复杂化，高级代理可能会变得越来越复杂，并可能很好地包含不同的推理和决策组件。我们目前的方法是将规划组件放在独立的、低级的模块中。代理只是调用这些，然后在产生的计划选项之间做出决定。

路加福音:有趣。你能多谈谈你正在开发的组合机制吗?

迈克尔:形式上验证基本逻辑属性已经很困难了。然而，一旦我们处理了可能在现实情况中使用的自治系统，那么我们通常会遇到亚博体育苹果app官方下载更复杂的逻辑查询。例如，假设我们希望验证一个属性，例如

当被问到这个问题时，机器人在30秒内回答的概率至少是80%

我们已经超越了基本属性，合并了概率(>80%)和实时方面(30秒内)。但是，对于自主系统，我们不仅要验证系统(例亚博体育苹果app官方下载如机器人)的功能，还要验证它的意图和信念。我们甚至需要验证一下

当被询问时，机器人相信请求已经发出并打算在30秒内回复的概率至少为80%

这里的问题是，我们需要用来描述这些需求的逻辑框架已经相当复杂了。逻辑的组合往往是难以处理的，概率、实时性、意图、信念等逻辑的组合还没有进行详细的研究。

我们的目的是发展和扩展一些理论我们一直在做的工作对复杂逻辑组合的模型检查，以解决这一问题，更全面的自主系统验证。亚博体育苹果app官方下载

路加福音:谢谢,迈克尔!

1. 阿金,r .”控制致命行为:将伦理嵌入混合型深思/反应型机器人架构”。技术报告GIT-GVU-07-11，佐治亚理工学院，2007。↩
2. 伍德曼，R，温菲尔德，A，哈珀，c和弗雷泽，m。构建更安全的机器人:安全驱动控制”。机械工程学报，31(5):591 - 594,2012。亚博体育官网↩