Zombori, Zsolt and Urban, J. and Brown, C.E. (2020) Prolog Technology Reinforcement Learning Prover: (System Description). In: 10th International Joint Conference on Automated Reasoning, IJCAR 2020. Springer, pp. 489-507. ISBN 9783030510534
|
Text
10.10072F978-3-030-51054-1_33.pdf Download (338kB) | Preview |
Abstract
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. © 2020, Springer Nature Switzerland AG.
| Item Type: | Book Section |
|---|---|
| Additional Information: | Conference code: 241679 Export Date: 17 August 2020 Correspondence Address: Zombori, Z.; Alfréd Rényi Institute of MathematicsHungary; email: zombori@renyi.hu Funding details: European Social Fund, ESF, 2018-1.2.1-NKP-00008, EFOP-3.6.3-VEKOP-16-2017-00002 Funding details: European Commission, EC Funding details: AI&Reasoning CZ.02.1.01/0.0/0.0/15 003/0000466, 649043 Funding details: European Regional Development Fund, FEDER Funding text 1: ZZ was supported by the European Union, co-financed by the European Social Fund (EFOP-3.6.3-VEKOP-16-2017-00002) and the Hungarian National Excellence Grant 2018-1.2.1-NKP-00008. JU and CB were funded by the AI4REASON ERC Consolidator grant nr. 649043, the Czech project AI&Reasoning CZ.02.1.01/0.0/0.0/15 003/0000466 and the European Regional Development Fund. |
| Uncontrolled Keywords: | Learning systems; reinforcement learning; reinforcement learning; automation; Calculations; Theorem proving; Logic programming; Automated theorem proving; Automated theorem proving; Symbolic learning; PROLOG (programming language); Connection tableau calculus; Automated theorem prover; Machine learners; Monte-Carlo tree searches; Prolog implementations; Python interfaces; System description; |
| Subjects: | Q Science / természettudomány > QA Mathematics / matematika Q Science / természettudomány > QA Mathematics / matematika > QA75 Electronic computers. Computer science / számítástechnika, számítógéptudomány |
| SWORD Depositor: | MTMT SWORD |
| Depositing User: | MTMT SWORD |
| Date Deposited: | 17 Aug 2020 12:29 |
| Last Modified: | 17 Aug 2020 12:29 |
| URI: | http://real.mtak.hu/id/eprint/112237 |
Actions (login required)
 |
Edit Item |
