inpefess/basic-rl-prover

An example of reinforcement learning based saturation prover

Basic Reinforcement Learning Prover

basic-rl-prover is an example of using the Ray Projects reinforcement learning library, ast2vec encoder for abstract syntax trees and a Gymnasium environment for saturation provers to train an automated theorem prover.

It's only a proof-of-concept now.

How to Install

The best way to install this package is to use pip:

pip install git+https://github.com/inpefess/basic-rl-prover.git

How to use

from basic_rl_prover.constants import TRAIN_PROBLEMS
from basic_rl_prover.test_prover import upload_and_test_agent
from basic_rl_prover.train_prover import train_a_prover

train_a_prover(TRAIN_PROBLEMS)
upload_and_test_agent(TRAIN_PROBLEMS)

How to Contribute

Pull requests are welcome. To start:

git clone https://github.com/inpefess/basic-rl-prover
cd basic-rl-prover
# activate python virtual environment with Python 3.8+ and poetry installed
poetry install
# recommended but not necessary
pre-commit install

To check the code quality before creating a pull request, one should run the script local-build.sh.

Reporting issues or problems with the software

Questions and bug reports are welcome on the tracker.

How to Cite

If you want to cite this project in your research paper, please use the following arXiv entry: https://arxiv.org/abs/2209.02562.