he 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 instantiation 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.
@article{arxiv.2501.09379,
title = {First Experiments with Neural cvc5},
author = {Jelle Piepenbrock and Mikoláš Janota and Jan Jakubův},
journal= {arXiv preprint arXiv:2501.09379},
year = {2025}
}