ray-prover#

CircleCIDocumentation Statuscodecov

ray-prover#

Generic saturation prover using Ray RLlib.

How to install#

ray-prover works with Python 3.8, 3.9, 3.10 or 3.11

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

How to use#

There are two scripts: for PPO and Thompson sampling.

--prover can be Vampire or iProver

Add --random_baseline for not learning anything. Thompson sampling works out of the box:

python ray_prover/thompson_sampling.py --prover Vampire \
--max_clause 20 --problem_filename \
~/data/TPTP-v8.1.2/Problems/SET/SET001-1.p --random_baseline

For PPO, one should launch clause representation Dockers first. See details for CodeBERT and ast2vec.

python ray_prover/ppo_prover.py --prover iProver --max_clause 15 \
--clause_representation CODEBERT --problem_filename \
~/data/TPTP-v8.1.2/Problems/SET/SET001-1.p