Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

First Experiments with Neural cvc5

Jelle Piepenbrock, Mikoláš Janota, Jan Jakubův

TL;DR

The paper addresses the challenge of guiding instantiation in SMT by introducing a CPU-friendly graph neural network that integrates with cvc5 to score quantified expressions and candidate term substitutions during enumerative instantiation. The approach learns from e-matching proof data and demonstrates substantial real-time improvements over standard enumeration on unseen problems, including up to 72% faster CPU times and, with more aggressive instantiation, up to 109% gains on large datasets. The work provides evidence that real-time neural guidance for SMT solvers is feasible on commodity hardware and offers a path to extend guidance to theories and other proving environments. Overall, the study shows how learned heuristics can bias instantiation decisions to achieve meaningful speedups while remaining tightly coupled to an existing solver.

Abstract

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.

First Experiments with Neural cvc5

TL;DR

The paper addresses the challenge of guiding instantiation in SMT by introducing a CPU-friendly graph neural network that integrates with cvc5 to score quantified expressions and candidate term substitutions during enumerative instantiation. The approach learns from e-matching proof data and demonstrates substantial real-time improvements over standard enumeration on unseen problems, including up to 72% faster CPU times and, with more aggressive instantiation, up to 109% gains on large datasets. The work provides evidence that real-time neural guidance for SMT solvers is feasible on commodity hardware and offers a path to extend guidance to theories and other proving environments. Overall, the study shows how learned heuristics can bias instantiation decisions to achieve meaningful speedups while remaining tightly coupled to an existing solver.

Abstract

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.
Paper Structure (8 sections, 1 equation, 3 figures, 3 tables)

This paper contains 8 sections, 1 equation, 3 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Proving By Instantiation
  3. Neural Instantiation for cvc5
  4. Experiments
  5. Small Dataset
  6. Large Dataset (MPTP1147)
  7. Conclusion
  8. Acknowledgements

Figures (3)

  • Figure 1: High-level architecture of cvc5. The techniques explained in Section \ref{['sec:inst']}, as well as our neural method (Section \ref{['sec:mlinst']} and on), are particular cases of the top rectangle.
  • Figure 2: A schematic description of 1 instantiation within the enumerative instantiation procedure, which we heavily modify to create our neural solver. In the example a new ground lemma is created by instantiating the variables (A,B,C) in quantified expression 3 (QE3) with the ground terms (t7, t7, t1) respectively. In the default enumerative instantiation procedure, all quantified expressions are instantiated each round.
  • Figure 3: Violin plots of the number of instantiations performed in successful runs for Bcvc5 e-matching, Bcvc5 enumeration, dry run, the ML strategy with threshold 1e-5, and the ML strategy with 10x as many instantiations per quantifier per round. The white dots indicate the medians. The respective medians are 2235, 1026, 373.5, 250 and 1620.