Learning to Reason in Large Theories without Imitation

Abstract

In this paper, we demonstrate how to do automated theorem proving in the presence of a large knowledge base of potential premises without learning from human proofs. We suggest an exploration mechanism that mixes in additional premises selected by a tf-idf (term frequency-inverse document frequency) based lookup in a deep reinforcement learning scenario. This helps with exploring and learning which premises are relevant for proving a new theorem. Our experiments show that the theorem prover trained with this exploration mechanism outperforms provers that are trained only on human proofs. It approaches the performance of a prover trained by a combination of imitation and reinforcement learning. We perform multiple experiments to understand the importance of the underlying assumptions that make our exploration approach work, thus explaining our design choices.

arXiv commentMajor revision

References in corpus (8)

• Adam: A Method for Stochastic Optimization
• Playing Atari with Deep Reinforcement Learning
• Large-Scale Study of Curiosity-Driven Learning
• Premise Selection for Mathematics by Corpus Analysis and Kernel Methods
• DeepMath - Deep Sequence Models for Premise Selection
• GamePad: A Learning Environment for Theorem Proving
• Holophrasm: a neural Automated Theorem Prover for higher-order logic
• HOList: An Environment for Machine Learning of Higher-Order Theorem Proving

Cited by in corpus (10)

• Generative Language Modeling for Automated Theorem Proving
• MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics
• Mathematical Reasoning in Latent Space
• LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning
• Learning Symbolic Rules for Reasoning in Quasi-Natural Language
• Learning to Prove Theorems by Learning to Generate Theorems
• TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning
• Proof Artifact Co-training for Theorem Proving with Language Models
• An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic
• BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving