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 条
  • [31] Herbrand Constructivization for Automated Intuitionistic Theorem Proving
    Ebner, Gabriel
    AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, TABLEAUX 2019, 2019, 11714 : 355 - 373
  • [32] Zap: Automated theorem proving for software analysis
    Ball, T
    Lahiri, SK
    Musuvathi, M
    LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2005, 3835 : 2 - 22
  • [33] Automated theorem proving in euler diagram systems
    Stapleton, Gem
    Masthoff, Judith
    Flower, Jean
    Fish, Andrew
    Southern, Jane
    Journal of Automated Reasoning, 2007, 39 (04): : 431 - 470
  • [35] An integration of program analysis and automated theorem proving
    Ellis, BJ
    Ireland, A
    INTEGRATED FORMAL METHODS, PROCEEDINGS, 2004, 2999 : 67 - 86
  • [36] Application of theorem proving to automated diagnoses field
    Shen, J
    Zhu, BG
    Chen, Y
    Fang, Q
    PROCEEDINGS OF THE 4TH WORLD CONGRESS ON INTELLIGENT CONTROL AND AUTOMATION, VOLS 1-4, 2002, : 3202 - 3204
  • [37] Automated theorem proving in Euler diagram systems
    Stapleton, Gem
    Masthoff, Judith
    Flower, Jean
    Fish, Andrew
    Southern, Jane
    JOURNAL OF AUTOMATED REASONING, 2007, 39 (04) : 431 - 470
  • [38] Scheduling methods for parallel automated theorem proving
    Stenz, G
    Wolf, A
    ADVANCES IN ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2000, 1822 : 254 - 266
  • [39] METHODS FOR AUTOMATED THEOREM PROVING IN NONCLASSICAL LOGICS
    MORGAN, CG
    IEEE TRANSACTIONS ON COMPUTERS, 1976, 25 (08) : 852 - 862
  • [40] THE KRIPKE AUTOMATED THEOREM-PROVING SYSTEM
    THISTLEWAITE, PB
    MCROBBIE, MA
    MEYER, RK
    LECTURE NOTES IN COMPUTER SCIENCE, 1986, 230 : 705 - 706