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 条
  • [41] Ordering in automated theorem proving of differential geometry
    Li Hongbo
    Cheng Minteh
    Acta Mathematicae Applicatae Sinica, 1998, 14 (4) : 358 - 362
  • [42] Automated Theorem Proving in Euler Diagram Systems
    Gem Stapleton
    Judith Masthoff
    Jean Flower
    Andrew Fish
    Jane Southern
    Journal of Automated Reasoning, 2007, 39 : 431 - 470
  • [43] Dealing with Degeneracies in Automated Theorem Proving in Geometry
    Kovacs, Zoltan
    Recio, Tomas
    Tabera, Luis F.
    Pilar Velez, M.
    MATHEMATICS, 2021, 9 (16)
  • [44] Automated Theorem Proving for General Game Playing
    Schiffel, Stephan
    Thielscher, Michael
    21ST INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI-09), PROCEEDINGS, 2009, : 911 - 916
  • [45] Automated theorem proving in quasigroup and loop theory
    Phillips, J. D.
    Stanovsky, David
    AI COMMUNICATIONS, 2010, 23 (2-3) : 267 - 283
  • [46] Combining formal derivation search procedures and natural theorem proving techniques in an automated theorem proving system
    Atayan, VV
    Morokhovets, MK
    CYBERNETICS AND SYSTEMS ANALYSIS, 1996, 32 (03) : 442 - 465
  • [47] Software Reliability through Theorem Proving
    Murthy, S. G. K.
    Sekharam, K. Raja
    DEFENCE SCIENCE JOURNAL, 2009, 59 (03) : 314 - 317
  • [48] Machine Learning for Inductive Theorem Proving
    Jiang, Yaqing
    Papapanagiotou, Petros
    Fleuriot, Jacques
    ARTIFICIAL INTELLIGENCE AND SYMBOLIC COMPUTATION (AISC 2018), 2018, 11110 : 87 - 103
  • [49] Proof procedures for an automated theorem-proving program
    Kim, SW
    Kim, SM
    KYBERNETES, 1998, 27 (8-9) : 1075 - +
  • [50] Another look at automated theorem-proving II
    Koblitz, Neal
    JOURNAL OF MATHEMATICAL CRYPTOLOGY, 2011, 5 (3-4) : 205 - 224