Zulip Chat Archive

Stream: Machine Learning for Theorem Proving

Topic: Paper: Prolog Technology Reinforcement Learning Prover

Jason Rute (Apr 28 2020 at 23:30):

Prolog Technology Reinforcement Learning Prover (System Description), by Zsolt Zombori, Josef Urban, and Chad E. Brown

Jason Rute (Apr 28 2020 at 23:30):

I'll write more after I've read the paper.

Jason Rute (Apr 28 2020 at 23:40):

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.

Jason Rute (Apr 28 2020 at 23:42):

Code/Environment: https://github.com/zsoltzombori/plcop

Jason Rute (Apr 28 2020 at 23:43):

I think at first glance it is a gym-like environment. We need to start making a list of these.

Last updated: Dec 20 2023 at 11:08 UTC