Proving Theorems using Incremental Learning and Hindsight Experience Replay
Traditional automated theorem provers for first-order logic depend on speed-optimized search and many handcrafted heuristics that are designed to work best over a wide range of domains. Machine learning approaches in literature either depend on these traditional provers to bootstrap themselves or fall short on reaching comparable performance. In this paper, we propose a general incremental learning algorithm for training domain specific provers for first-order logic without equality, based only on a basic given-clause algorithm, but using a learned clause-scoring function. Clauses are represented as graphs and presented to transformer networks with spectral features. To address the sparsity and the initial lack of training data as well as the lack of a natural curriculum, we adapt hindsight experience replay to theorem proving, so as to be able to learn even when no proof can be found. We show that provers trained this way can match and sometimes surpass state-of-the-art traditional provers on the TPTP dataset in terms of both quantity and quality of the proofs.
Code (0)
등록된 구현이 없습니다.
Tasks
Automated Theorem ProvingIncremental LearningMethods 이 논문이 사용한 방법론
Similar Papers 제목 키워드 기반
Hindsight Curriculum Generation Based Multi-Goal Experience Replay
In multi-goal tasks with sparse rewards, it is challenging to learn from tons of experiences with zero rewards. Hindsight experience replay (HER), which replays past experiences with additional heuristic goals, has shown…
Reinforcement Learning (RL)HIGhER : Improving instruction following with Hindsight Generation for Experience Replay
Language creates a compact representation of the world and allows the description of unlimited situations and objectives through compositionality. While these characterizations may foster instructing, conditioning or str…
Instruction FollowingLanguage AcquisitionReinforcement LearningARCHER: Aggressive Rewards to Counter bias in Hindsight Experience Replay
Experience replay is an important technique for addressing sample-inefficiency in deep reinforcement learning (RL), but faces difficulty in learning from binary and sparse rewards due to disproportionately few successful…
continuous-controlContinuous ControlDeep Reinforcement LearningReinforcement Learning+1Hindsight Goal Ranking on Replay Buffer for Sparse Reward Environment
This paper proposes a method for prioritizing the replay experience referred to as Hindsight Goal Ranking (HGR) in overcoming the limitation of Hindsight Experience Replay (HER) that generates hindsight goals based on un…
Improvements on Hindsight Learning
Sparse reward problems are one of the biggest challenges in Reinforcement Learning. Goal-directed tasks are one such sparse reward problems where a reward signal is received only when the goal is reached. One promising w…
Policy Gradient Methodsreinforcement-learningReinforcement LearningReinforcement Learning (RL)