First Experiments with Neural cvc5

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F24%3A00375287" target="_blank" >RIV/68407700:21730/24:00375287 - isvavai.cz</a>

Result on the web

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

DOI - Digital Object Identifier

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

Result language

angličtina

Original language name

First Experiments with Neural cvc5

Original language description

The cvc5 solver is today one of the strongest systems for solving first order problems with theories but also without them. In this work we equip its enumeration-based instan tiation with a neural network that guides the choice of the quantified formulas and their instances. For that we develop a relatively fast graph neural network that repeatedly scores all available instantiation options with respect to the available formulas. The network runs directly on a CPU without the need for any special hardware. We train the neural guidance on a large set of proofs generated by the e-matching instantiation strategy and evaluate its performance on a set of previously unseen problems.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

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

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

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

Publication year

2024

Confidentiality

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

Article name in the collection

Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning

ISBN

—

ISSN

2398-7340

e-ISSN

—

Number of pages

14

Pages from-to

264-277

Publisher name

EasyChair Publications

Place of publication

Manchester

Event location

Balaclava

Event date

May 26, 2024

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—