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 条
  • [21] Automated theorem proving by test set induction
    Bouhoula, A
    JOURNAL OF SYMBOLIC COMPUTATION, 1997, 23 (01) : 47 - 77
  • [23] Automated Theorem Proving in GeoGebra: Current Achievements
    Francisco Botana
    Markus Hohenwarter
    Predrag Janičić
    Zoltán Kovács
    Ivan Petrović
    Tomás Recio
    Simon Weitzhofer
    Journal of Automated Reasoning, 2015, 55 : 39 - 59
  • [24] Recent advances in automated theorem proving on inequalities
    Yang L.
    Journal of Computer Science and Technology, 1999, 14 (5) : 434 - 446
  • [25] An Empirical Assessment of Progress in Automated Theorem Proving
    Sutcliffe, Geoff
    Suttner, Christian
    Kotthoff, Lars
    Perrault, C. Raymond
    Khalid, Zain
    AUTOMATED REASONING, IJCAR 2024, PT I, 2024, 14739 : 53 - 74
  • [26] Another look at automated theorem-proving
    Koblitz, Neal
    JOURNAL OF MATHEMATICAL CRYPTOLOGY, 2007, 1 (04) : 385 - 403
  • [27] Proof Documents for Automated Origami Theorem Proving
    Ghourabi, Fadoua
    Ida, Tetsuo
    Kasem, Asem
    AUTOMATED DEDUCTION IN GEOMETRY, 2011, 6877 : 78 - +
  • [28] Integration of automated and interactive theorem proving in ILF
    Dahn, BI
    Gehne, J
    Honigmann, T
    Wolf, A
    AUTOMATED DEDUCTION - CADE-14, 1997, 1249 : 57 - 60
  • [29] External Sources of Axioms in Automated Theorem Proving
    Suda, Martin
    Sutcliffe, Geoff
    Wischnewski, Patrick
    Lamotte-Schubert, Manuel
    de Melo, Gerard
    KI 2009: ADVANCES IN ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2009, 5803 : 281 - +
  • [30] Automated Theorem Proving in GeoGebra: Current Achievements
    Botana, Francisco
    Hohenwarter, Markus
    Janicic, Predrag
    Kovacs, Zoltan
    Petrovic, Ivan
    Recio, Tomas
    Weitzhofer, Simon
    JOURNAL OF AUTOMATED REASONING, 2015, 55 (01) : 39 - 59