# Prolog Technology Reinforcement Learning Prover

arXiv: https://arxiv.org/abs/2004.06997 · HTML: https://mlsanity.com/paper/2004.06997/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 15 Apr 2020.

## Built on by (most cited first, 7 of 7)

- [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://mlsanity.com/paper/2102.09756/) (2021)
- [Beyond Games: A Systematic Review of Neural Monte Carlo Tree Search Applications](https://mlsanity.com/paper/2303.08060/) (2023)
- [Learning to Guide a Saturation-Based Theorem Prover](https://mlsanity.com/paper/2106.03906/) (2021)
- [Proving Theorems using Incremental Learning and Hindsight Experience Replay](https://mlsanity.com/paper/2112.10664/) (2021)
- [Abstract Visual Reasoning: An Algebraic Approach for Solving Raven's Progressive Matrices](https://mlsanity.com/paper/2303.11730/) (2023)
- [QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning](https://mlsanity.com/paper/2408.09237/) (2024)
- [Application of AI to formal methods - an analysis of current trends](https://mlsanity.com/paper/2411.14870/) (2024)

## Abstract (arXiv)

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.