How Much Should This Symbol Weigh? A GNN-Advised Clause Selection

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21230%2F23%3A00367641" target="_blank" >RIV/68407700:21230/23:00367641 - isvavai.cz</a>

Nalezeny alternativní kódy

RIV/68407700:21730/23:00367641

Výsledek na webu

<a href="https://doi.org/10.29007/5f4r" target="_blank" >https://doi.org/10.29007/5f4r</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.29007/5f4r" target="_blank" >10.29007/5f4r</a>

Jazyk výsledku

angličtina

Název v původním jazyce

How Much Should This Symbol Weigh? A GNN-Advised Clause Selection

Popis výsledku v původním jazyce

Clause selection plays a crucial role in modern saturation-based automatic theorem provers. A commonly used heuristic suggests prioritizing small clauses, i.e., clauses with few symbol occurrences. More generally, we can give preference to clauses with a low weighted symbol occurrence count, where each symbol’s occurrence count is multiplied by a respective symbol weight. Traditionally, a human domain expert would supply the symbol weights. In this paper, we propose a system based on a graph neural network that learns to predict symbol weights with the aim of improving clause selection for arbitrary first-order logic problems. Our experiments demonstrate that by advising the automatic theorem prover Vampire on the first-order fragment of TPTP using a trained neural network, the prover’s problem solving capability improves by 6.6% compared to uniformly weighting symbols and by 2.1% compared to a goal-directed variant of the uniformly weighting strategy.

Název v anglickém jazyce

How Much Should This Symbol Weigh? A GNN-Advised Clause Selection

Popis výsledku anglicky

Clause selection plays a crucial role in modern saturation-based automatic theorem provers. A commonly used heuristic suggests prioritizing small clauses, i.e., clauses with few symbol occurrences. More generally, we can give preference to clauses with a low weighted symbol occurrence count, where each symbol’s occurrence count is multiplied by a respective symbol weight. Traditionally, a human domain expert would supply the symbol weights. In this paper, we propose a system based on a graph neural network that learns to predict symbol weights with the aim of improving clause selection for arbitrary first-order logic problems. Our experiments demonstrate that by advising the automatic theorem prover Vampire on the first-order fragment of TPTP using a trained neural network, the prover’s problem solving capability improves by 6.6% compared to uniformly weighting symbols and by 2.1% compared to a goal-directed variant of the uniformly weighting strategy.

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

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

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

Rok uplatnění

2023

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

Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR)

ISBN

—

ISSN

2398-7340

e-ISSN

2398-7340

Počet stran výsledku

16

Strana od-do

96-111

Název nakladatele

EasyChair Publications

Místo vydání

Manchester

Místo konání akce

Manizales

Datum konání akce

4. 6. 2023

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

WRD - Celosvětová akce

Kód UT WoS článku

—