Current browse context:
cs.AI
Change to browse by:
References & Citations
Computer Science > Artificial Intelligence
Title: The Role of Entropy in Guiding a Connection Prover
(Submitted on 31 May 2021 (v1), last revised 16 Jul 2021 (this version, v2))
Abstract: In this work we study how to learn good algorithms for selecting reasoning steps in theorem proving. We explore this in the connection tableau calculus implemented by leanCoP where the partial tableau provides a clean and compact notion of a state to which a limited number of inferences can be applied. We start by incorporating a state-of-the-art learning algorithm -- a graph neural network (GNN) -- into the plCoP theorem prover. Then we use it to observe the system's behaviour in a reinforcement learning setting, i.e., when learning inference guidance from successful Monte-Carlo tree searches on many problems. Despite its better pattern matching capability, the GNN initially performs worse than a simpler previously used learning algorithm. We observe that the simpler algorithm is less confident, i.e., its recommendations have higher entropy. This leads us to explore how the entropy of the inference selection implemented via the neural network influences the proof search. This is related to research in human decision-making under uncertainty, and in particular the probability matching theory. Our main result shows that a proper entropy regularisation, i.e., training the GNN not to be overconfident, greatly improves plCoP's performance on a large mathematical corpus.
Submission history
From: Zsolt Zombori [view email][v1] Mon, 31 May 2021 04:57:44 GMT (39kb)
[v2] Fri, 16 Jul 2021 12:43:12 GMT (39kb)
Link back to: arXiv, form interface, contact.