2019/05/25 by Kshitij Bansal, Christian Szegedy, Bansal, Kshitij +7 · 4 citations
Computer Science · #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Machine Learning (cs.LG) #Machine Learning (stat.ML) #Machine Learning and Algorithms #Software Engineering Research
paper · pdf · doi:10.48550/arxiv.1905.10501
openalex publication_date 2019/05/25 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.