Algorithmic Ethics: Formalization and Verification of Autonomous Vehicle Obligations
Algorithmic Ethics: Formalization and Verification of Autonomous Vehicle Obligations
复制标题
算法伦理：自动驾驶汽车义务的形式化和验证
DOI：
10.1145/3460975
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Houssam Abbas
中科院分区：
文献类型：
--
作者：
Colin Shea;Houssam Abbas
在本文中，我们开发了一个正式的框架，用于自动推理自主网络物理系统的义务，包括其社会和道德义务。义务、权限和禁止与系统的任务不同，是指定先进的、自适应人工智能系统的必要组成部分。他们需要专门的义务义务逻辑来将其形式化。大多数现有道义逻辑缺乏允许自动验证的相应算法和系统模型。我们展示了一种特殊的道义逻辑，即支配行为功利主义（DAU）[23]，如何成为正式确定自动驾驶汽车等自主系统义务的合适起点。我们通过在 DAU 中形式化责任敏感安全 (RSS) 的子集来证明其有用性； RSS 是一项关于自动驾驶汽车在交通中应该和不应该如何行为的工业提案。我们表明 RSS 的某些逻辑后果是不可取的，表明需要进一步完善该提案。我们还展示了义务如何随着时间的推移而变化，这对于长期自治是必要的。然后，我们演示了加权转换系统上 DAU 公式的模型检查算法，并通过文献中自动驾驶汽车控制器的模型检查义务来说明它。
In this article, we develop a formal framework for automatic reasoning about the obligations of autonomous cyber-physical systems, including their social and ethical obligations. Obligations, permissions, and prohibitions are distinct from a system's mission, and are a necessary part of specifying advanced, adaptive AI-equipped systems. They need a dedicated deontic logic of obligations to formalize them. Most existing deontic logics lack corresponding algorithms and system models that permit automatic verification. We demonstrate how a particular deontic logic, Dominance Act Utilitarianism (DAU) [23], is a suitable starting point for formalizing the obligations of autonomous systems like self-driving cars. We demonstrate its usefulness by formalizing a subset of Responsibility-Sensitive Safety (RSS) in DAU; RSS is an industrial proposal for how self-driving cars should and should not behave in traffic. We show that certain logical consequences of RSS are undesirable, indicating a need to further refine the proposal. We also demonstrate how obligations can change over time, which is necessary for long-term autonomy. We then demonstrate a model-checking algorithm for DAU formulas on weighted transition systems and illustrate it by model-checking obligations of a self-driving car controller from the literature.
DOI：
10.1145/3359986.3361203
发表时间：
2019-10
期刊：
Proceedings of the 17th ACM-IEEE International Conference on Formal Methods and Models for System Design
影响因子：
--
作者：
Mohammad Hekmatnejad;Shakiba Yaghoubi;Adel Dokhanchi;H. B. Amor;Aviral Shrivastava;Lina Karam;Georgios Fainekos
通讯作者：
Mohammad Hekmatnejad;Shakiba Yaghoubi;Adel Dokhanchi;H. B. Amor;Aviral Shrivastava;Lina Karam;Georgios Fainekos
使用学习稀疏布尔公式的有效方法解释人工智能决策
DOI：
10.1007/s10817-018-9499-8
发表时间：
2018
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
Jha, Susmit;Sahai, Tuhin;Raman, Vasumathi;Pinto, Alessandro;Francis, Michael
通讯作者：
Francis, Michael
DOI：
10.1007/s10009-015-0378-x
发表时间：
2017-02-01
影响因子：
1.5
作者：
Lomuscio, Alessio;Qu, Hongyang;Raimondi, Franco
通讯作者：
Raimondi, Franco