홈 › Papers

Learning to Guide a Saturation-Based Theorem Prover

2021-06-07 · Ibrahim Abdelaziz, Maxwell Crouse, Bassem Makni, Vernon Austil, Cristina Cornelio, Shajith Ikbal, Pavan Kapanipathi, Ndivhuwo Makondo, Kavitha Srinivas, Michael Witbrock, Achille Fokoue

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 be integrated into theorem provers to improve their performance automatically. In this work, we introduce TRAIL, a deep learning-based approach to theorem proving that characterizes core elements of saturation-based theorem proving within a neural framework. TRAIL leverages (a) an effective graph neural network for representing logical formulas, (b) a novel neural representation of the state of a saturation-based theorem prover in terms of processed clauses and available actions, and (c) a novel representation of the inference selection process as an attention-based action policy. We show through a systematic analysis that these components allow TRAIL to significantly outperform previous reinforcement learning-based theorem provers on two standard benchmark datasets (up to 36% more theorems proved). In addition, to the best of our knowledge, TRAIL is the first reinforcement learning-based approach to exceed the performance of a state-of-the-art traditional theorem prover on a standard theorem proving benchmark (solving up to 17% more problems).

📄 PDF Abstract BibTeX arXiv:2106.03906

Code (0)

등록된 구현이 없습니다.

Tasks

Automated Theorem Proving Graph Neural Network reinforcement-learning Reinforcement Learning Reinforcement Learning (RL)

Methods 이 논문이 사용한 방법론

Graph Neural Network 설명 없음

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 (TP…

OpenAI Gym Reinforcement Learning (RL)

Training a First-Order Theorem Prover from Synthetic Data

2021-03-05 · Vlad Firoiu, Eser Aygun, Ankit Anand, Zafarali Ahmed 외

A major challenge in applying machine learning to automated theorem proving is the scarcity of training data, which is a key ingredient in training successful deep learning models. To tackle this problem, we propose an a…

Automated Theorem Proving BIG-bench Machine Learning

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

A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving

2019-11-05 · Maxwell Crouse, Ibrahim Abdelaziz, Bassem Makni, Spencer Whitehead 외

Automated theorem provers have traditionally relied on manually tuned heuristics to guide how they perform proof search. Deep reinforcement learning has been proposed as a way to obviate the need for such heuristics, how…

Automated Theorem Proving Deep Reinforcement Learning reinforcement-learning Reinforcement Learning+1

Efficient Neural Clause-Selection Reinforcement

2025-03-10 · Martin Suda

Clause selection is arguably the most important choice point in saturation-based theorem proving. Framing it as a reinforcement learning (RL) task is a way to challenge the human-designed heuristics of state-of-the-art p…

Automated Theorem Proving CPU Reinforcement Learning (RL)