The Role of Entropy in Guiding a Connection Prover

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F21%3A00354436" target="_blank" >RIV/68407700:21730/21:00354436 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1007/978-3-030-86059-2_13" target="_blank" >https://doi.org/10.1007/978-3-030-86059-2_13</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-86059-2_13" target="_blank" >10.1007/978-3-030-86059-2_13</a>

Jazyk výsledku

angličtina

Název v původním jazyce

The Role of Entropy in Guiding a Connection Prover

Popis výsledku v původním jazyce

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 behavior 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 regularization, i.e., training the GNN not to be overconfident, greatly improves plCoP ’s performance on a large mathematical corpus.

Název v anglickém jazyce

The Role of Entropy in Guiding a Connection Prover

Popis výsledku anglicky

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 behavior 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 regularization, i.e., training the GNN not to be overconfident, greatly improves plCoP ’s performance on a large mathematical corpus.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/EF15_003%2F0000466" target="_blank" >EF15_003/0000466: Umělá inteligence a uvažování</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2021

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Automated Reasoning with Analytic Tableaux and Related Methods

ISBN

978-3-030-86058-5

ISSN

0302-9743

e-ISSN

1611-3349

Počet stran výsledku

18

Strana od-do

218-235

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Birmingham

Datum konání akce

6. 9. 2021

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000711656700013