Reinforcement Learning of Theorem Proving
We introduce a theorem proving algorithm that uses practically no domain heuristics for guiding its connection-style proof search. Instead, it runs many Monte-Carlo simulations guided by reinforcement learning from previous proof attempts. We produce several versions of the prover, parameterized by different learning and guiding algorithms. The strongest version of the system is trained on a large corpus of mathematical problems and evaluated on previously unseen problems. The trained system solves within the same number of inferences over 40% more problems than a baseline prover, which is an unusually high improvement in this hard AI domain. To our knowledge this is the first time reinforcement learning has been convincingly applied to solving general mathematical problems on a large scale.
Code (0)
등록된 구현이 없습니다.
Tasks
Automated Theorem Provingreinforcement-learningReinforcement LearningReinforcement Learning (RL)Similar Papers 제목 키워드 기반
A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving
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 ProvingDeep Reinforcement Learningreinforcement-learningReinforcement Learning+1DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning
Theorem proving serves as a major testbed for evaluating complex reasoning abilities in large language models (LLMs). However, traditional automated theorem proving (ATP) approaches rely heavily on formal proof systems t…
Automated Theorem ProvingMathematical ReasoningLearning to Guide a Saturation-Based Theorem Prover
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 ProvingGraph Neural Networkreinforcement-learningReinforcement Learning+1A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation
Large language models (LLMs) have significantly advanced formal theorem proving, yet the scarcity of high-quality training data constrains their capabilities in complex mathematical domains. Combinatorics, a cornerstone …
Automated Theorem ProvingLanguage ModelingLanguage ModellingLarge Language ModelHOList: An Environment for Machine Learning of Higher-Order Theorem Proving
We present an environment, benchmark, and deep learning driven automated theorem prover for higher-order logic. Higher-order interactive theorem provers enable the formalization of arbitrary mathematical theories and the…
Automated Theorem ProvingBIG-bench Machine LearningDeep LearningDeep Reinforcement Learning+3