Guiding an Instantiation Prover with Graph Neural Networks

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F23%3A00372206" target="_blank" >RIV/68407700:21730/23:00372206 - isvavai.cz</a>

Výsledek na webu

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

DOI - Digital Object Identifier

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

Jazyk výsledku

angličtina

Název v původním jazyce

Guiding an Instantiation Prover with Graph Neural Networks

Popis výsledku v původním jazyce

In this work we extend an instantiation-based theorem prover iProver with machine learning (ML) guidance based on graph neural networks. For this we implement an interactive mode in iProver, which allows communication with an external agent via network sockets. The external (ML-based) agent guides the proof search by scoring generated clauses in the given clause loop. Our evaluation on a large set of Mizar problems shows that the ML guidance outperforms iProver’s standard human-programmed priority queues, solving more than twice as many problems in the same time. To our knowledge, this is the first time the performance of a state-of-the-art instantiation-based system is doubled by ML guidance.

Název v anglickém jazyce

Guiding an Instantiation Prover with Graph Neural Networks

Popis výsledku anglicky

In this work we extend an instantiation-based theorem prover iProver with machine learning (ML) guidance based on graph neural networks. For this we implement an interactive mode in iProver, which allows communication with an external agent via network sockets. The external (ML-based) agent guides the proof search by scoring generated clauses in the given clause loop. Our evaluation on a large set of Mizar problems shows that the ML guidance outperforms iProver’s standard human-programmed priority queues, solving more than twice as many problems in the same time. To our knowledge, this is the first time the performance of a state-of-the-art instantiation-based system is doubled by ML guidance.

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

12

Strana od-do

112-123

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

—