Learning Normative Behaviour Through Automated Theorem Proving

被引:1
|
作者
Neufeld, Emery A. [1 ]
机构
[1] Vienna Univ Technol, Vienna, Austria
来源
KUNSTLICHE INTELLIGENZ | 2024年 / 38卷 / 1-2期
关键词
Theorem proving; Defeasible deontic logic; Ethical reinforcement learning; LOGIC;
D O I
10.1007/s13218-024-00844-x
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
Reinforcement learning (RL) is a powerful tool for teaching agents goal-directed behaviour in stochastic environments, and many proposed applications involve adopting societal roles which have ethical, legal, or social norms attached to them. Though multiple approaches exist for teaching RL agents norm-compliant behaviour, there are limitations on what normative systems they can accommodate. In this paper we analyse and improve the techniques proposed for use with the Normative Supervisor (Neufeld, et al., 2021)-a module which uses conclusions gleaned from a defeasible deontic logic theorem prover to restrict the behaviour of RL agents. First, we propose a supplementary technique we call violation counting to broaden the range of normative systems we can learn from, thus covering normative conflicts and contrary-to-duty norms. Additionally, we propose an algorithm for constructing a "normative filter", a function that can be used to implement the addressed techniques without requiring the theorem prover to be run at each step during training or operation, significantly decreasing the overall computational overhead of using the normative supervisor. In order to demonstrate these contributions, we use a computer game-based case study, and thereafter discuss remaining problems to be solved in the conclusion.
引用
收藏
页码:25 / 43
页数:19
相关论文
共 50 条
  • [1] Automated theorem proving
    Li, HB
    GEOMETRIC ALGEBRA WITH APPLICATIONS IN SCIENCE AND ENGINEERING, 2001, : 110 - +
  • [2] Automated theorem proving
    Plaisted, David A.
    WILEY INTERDISCIPLINARY REVIEWS-COGNITIVE SCIENCE, 2014, 5 (02) : 115 - 128
  • [3] Machine Learning for Automated Theorem Proving: Learning to Solve SAT and QSAT
    Holden, Sean B.
    FOUNDATIONS AND TRENDS IN MACHINE LEARNING, 2021, 14 (06): : 807 - 989
  • [4] ON AUTOMATED THEOREM-PROVING
    RUSSELL, S
    WHEELER, T
    ANNALS OF THE NEW YORK ACADEMY OF SCIENCES, 1992, 661 : 160 - 173
  • [5] On Interpolation in Automated Theorem Proving
    Maria Paola Bonacina
    Moa Johansson
    Journal of Automated Reasoning, 2015, 54 : 69 - 97
  • [6] Directed automated theorem proving
    Edelkamp, S
    Leven, P
    LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, 2002, 2514 : 145 - 159
  • [7] Orderings in automated theorem proving
    Kirchner, H
    MATHEMATICAL ASPECTS OF ARTIFICIAL INTELLIGENCE, 1998, 55 : 55 - 95
  • [8] Automated Theorem Proving in the Classroom
    Windsteiger, Wolfgang
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2021, (352): : 54 - 63
  • [9] Automated theorem proving: An overview
    Maghrabi, TH
    ARABIAN JOURNAL FOR SCIENCE AND ENGINEERING, 1997, 22 (2B): : 245 - 258
  • [10] On Interpolation in Automated Theorem Proving
    Bonacina, Maria Paola
    Johansson, Moa
    JOURNAL OF AUTOMATED REASONING, 2015, 54 (01) : 69 - 97