First Experiments with Neural cvc5
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866915105595195392 |
|---|---|
| author | Piepenbrock, Jelle Janota, Mikoláš Jakubův, Jan |
| author_facet | Piepenbrock, Jelle Janota, Mikoláš Jakubův, Jan |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_09379 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | First Experiments with Neural cvc5 Piepenbrock, Jelle Janota, Mikoláš Jakubův, Jan Logic in Computer Science 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. |
| title | First Experiments with Neural cvc5 |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2501.09379 |