Formal verification of ethical choices in autonomous systems
Formal verification of ethical choices in autonomous systems
复制标题
DOI：
10.1016/j.robot.2015.11.012
复制
发表时间：
2016-03-01
影响因子：
4.3
通讯作者：
Webster, Matt
中科院分区：
文献类型：
--
作者：
Dennis, Louise;Fisher, Michael;Webster, Matt
无人驾驶汽车等自主系统开始在社会中运行。所有社会参与者都必须遵守具体的法规和法律。自治系统不能例外。不可避免的是，一个自治系统将发现自己处于这样一种境地：它不仅需要选择是否遵守规则，而且还需要做出复杂的道德决定。然而，没有明显的方法来实现人类对计算机道德行为的理解。即使我们使自治系统能够区分更多和更少的道德选择，我们如何确保它们会选择正确的？我们认为自治系统的混合体系结构，其中最高层次的推理是由一个理性（BDI）代理执行。对于这样一个系统，形式化验证已成功地用于证明在做出决策时遵守特定的行为规则。我们提出了一个理论框架，伦理计划选择，可以正式验证。我们实现了一个合理的代理，将一个给定的道德政策，在其计划选择，并表明我们可以正式验证代理选择执行，以最好的信念，最道德的可用计划。(C)2015作者由Elsevier B.V.发布，这是CC BY许可下的开放获取文章。
Autonomous systems such as unmanned vehicles are beginning to operate within society. All participants in society are required to follow specific regulations and laws. An autonomous system cannot be an exception. Inevitably an autonomous system will find itself in a situation in which it needs to not only choose to obey a rule or not, but also make a complex ethical decision. However, there exists no obvious way to implement the human understanding of ethical behaviour in computers. Even if we enable autonomous systems to distinguish between more and less ethical alternatives, how can we be sure that they would choose right? We consider autonomous systems with a hybrid architecture in which the highest level of reasoning is executed by a rational (BDI) agent. For such a system, formal verification has been used successfully to prove that specific rules of behaviour are observed when making decisions. We propose a theoretical framework for ethical plan selection that can be formally verified. We implement a rational agent that incorporates a given ethical policy in its plan selection and show that we can formally verify that the agent chooses to execute, to the best of its beliefs, the most ethical available plan. (C) 2015 The Authors. Published by Elsevier B.V. This is an open access article under the CC BY license.