Gym-saturation: an OpenAI Gym environment for saturation provers

2022-03-09 · Boris Shminke

gym-saturation is an OpenAI Gym environment for reinforcement learning (RL) agents capable of proving theorems. Currently, only theorems written in a formal language of the Thousands of Problems for Theorem Provers (TPTP) library in clausal normal form (CNF) are supported. gym-saturation implements the 'given clause' algorithm (similar to the one used in Vampire and E Prover). Being written in Python, gym-saturation was inspired by PyRes. In contrast to the monolithic architecture of a typical Automated Theorem Prover (ATP), gym-saturation gives different agents opportunities to select clauses themselves and train from their experience. Combined with a particular agent, gym-saturation can work as an ATP. Even with a non trained agent based on heuristics, gym-saturation can find refutations for 688 (of 8257) CNF problems from TPTP v7.5.0.

📄 PDF Abstract BibTeX arXiv:2203.04699

Code (0)

등록된 구현이 없습니다.

Tasks

OpenAI Gym Reinforcement Learning (RL)

Methods 이 논문이 사용한 방법론

NON 설명 없음

gym-saturation: Gymnasium environments for saturation provers (System description)

2023-09-16 · Boris Shminke

This work describes a new version of a previously published Python package - gym-saturation: a collection of OpenAI Gym environments for guiding saturation-style provers based on the given clause algorithm with reinforce…

OpenAI Gym reinforcement-learning Reinforcement Learning rllib+1

Project proposal: A modular reinforcement learning based automated theorem prover

2022-09-06 · Boris Shminke

We propose to build a reinforcement learning prover of independent components: a deductive system (an environment), the proof state representation (how an agent sees the environment), and an agent training algorithm. To …

OpenAI Gym reinforcement-learning Reinforcement Learning Reinforcement Learning (RL)+1

Learning to Guide a Saturation-Based Theorem Prover

2021-06-07 · Ibrahim Abdelaziz, Maxwell Crouse, Bassem Makni, Vernon Austil 외

Traditional automated theorem provers have relied on manually tuned heuristics to guide how they perform proof search. Recently, however, there has been a surge of interest in the design of learning mechanisms that can b…

Automated Theorem Proving Graph Neural Network reinforcement-learning Reinforcement Learning+1

Agent Island: A Saturation- and Contamination-Resistant Benchmark from Multiagent Games

2026-05-05 · Connacher Murphy arxiv

Static capabilities benchmarks suffer from saturation and contamination, making it difficult to track capabilities progress over time. We introduce Agent Island, a multiplayer simulation environment in which language-mod…

ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E

2019-03-07 · Karel Chvalovský, Jan Jakubův, Martin Suda, Josef Urban

We describe an efficient implementation of clause guidance in saturation-based automated theorem provers extending the ENIGMA approach. Unlike in the first ENIGMA implementation where fast linear classifier is trained an…

Automated Theorem Proving