Prolog Technology Reinforcement Learning Prover (System Description)

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F20%3A00346050" target="_blank" >RIV/68407700:21730/20:00346050 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1007/978-3-030-51054-1_33" target="_blank" >https://doi.org/10.1007/978-3-030-51054-1_33</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-51054-1_33" target="_blank" >10.1007/978-3-030-51054-1_33</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Prolog Technology Reinforcement Learning Prover (System Description)

Popis výsledku v původním jazyce

We present a reinforcement learning toolkit for experiments with guiding automated theorem proving in the connection calculus. The core of the toolkit is a compact and easy to extend Prolog-based automated theorem prover called plCoP. plCoP builds on the leanCoP Prolog implementation and adds learning-guided Monte-Carlo Tree Search as done in the rlCoP system. Other components include a Python interface to plCoP and machine learners, and an external proof checker that verifies the validity of plCoP proofs. The toolkit is evaluated on two benchmarks and we demonstrate its extendability by two additions: (1) guidance is extended to reduction steps and (2) the standard leanCoP calculus is extended with rewrite steps and their learned guidance. We argue that the Prolog setting is suitable for combining statistical and symbolic learning methods. The complete toolkit is publicly released.

Název v anglickém jazyce

Prolog Technology Reinforcement Learning Prover (System Description)

Popis výsledku anglicky

We present a reinforcement learning toolkit for experiments with guiding automated theorem proving in the connection calculus. The core of the toolkit is a compact and easy to extend Prolog-based automated theorem prover called plCoP. plCoP builds on the leanCoP Prolog implementation and adds learning-guided Monte-Carlo Tree Search as done in the rlCoP system. Other components include a Python interface to plCoP and machine learners, and an external proof checker that verifies the validity of plCoP proofs. The toolkit is evaluated on two benchmarks and we demonstrate its extendability by two additions: (1) guidance is extended to reduction steps and (2) the standard leanCoP calculus is extended with rewrite steps and their learned guidance. We argue that the Prolog setting is suitable for combining statistical and symbolic learning methods. The complete toolkit is publicly released.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/EF15_003%2F0000466" target="_blank" >EF15_003/0000466: Umělá inteligence a uvažování</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2020

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Lecture Notes in Computer Science

ISBN

978-3-030-51053-4

ISSN

0302-9743

e-ISSN

1611-3349

Počet stran výsledku

19

Strana od-do

489-507

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Paris

Datum konání akce

29. 6. 2020

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000884319500033