Invariant neural architecture for learning term synthesis in instantiation proving

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F25%3A00379734" target="_blank" >RIV/68407700:21730/25:00379734 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1016/j.jsc.2024.102375" target="_blank" >https://doi.org/10.1016/j.jsc.2024.102375</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1016/j.jsc.2024.102375" target="_blank" >10.1016/j.jsc.2024.102375</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Invariant neural architecture for learning term synthesis in instantiation proving

Popis výsledku v původním jazyce

The development of strong CDCL-based propositional (SAT) solvers has greatly advanced several areas of automated reasoning (AR). One of the directions in AR is therefore to make use of SAT solvers in expressive formalisms such as first-order logic, for which large corpora of general mathematical problems exist today. This is possible due to Herbrand's theorem, which allows reduction of first-order problems to propositional problems by instantiation. The core challenge is synthesizing the appropriate instances from the typically infinite Herbrand universe. In this work, we develop a machine learning system targeting this task, addressing its combinatorial and invariance properties. In particular, we develop a GNN2RNN architecture based on a graph neural network (GNN) that learns from problems and their solutions independently of many symmetries and symbol names (addressing the abundance of Skolems), combined with a recurrent neural network (RNN) that proposes for each clause its instantiations. The architecture is then combined with an efficient ground solver and, starting with zero knowledge, iteratively trained on a large corpus of mathematical problems. We show that the system is capable of solving many problems by such educated guessing, finding proofs for 32.12% of the training set. The final trained system solves 19.74% of the unseen test data on its own. We also observe that the trained system finds solutions that the iProver and CVC5 systems did not find. (c) 2024 The Authors. Published by Elsevier Ltd.

Název v anglickém jazyce

Invariant neural architecture for learning term synthesis in instantiation proving

Popis výsledku anglicky

The development of strong CDCL-based propositional (SAT) solvers has greatly advanced several areas of automated reasoning (AR). One of the directions in AR is therefore to make use of SAT solvers in expressive formalisms such as first-order logic, for which large corpora of general mathematical problems exist today. This is possible due to Herbrand's theorem, which allows reduction of first-order problems to propositional problems by instantiation. The core challenge is synthesizing the appropriate instances from the typically infinite Herbrand universe. In this work, we develop a machine learning system targeting this task, addressing its combinatorial and invariance properties. In particular, we develop a GNN2RNN architecture based on a graph neural network (GNN) that learns from problems and their solutions independently of many symmetries and symbol names (addressing the abundance of Skolems), combined with a recurrent neural network (RNN) that proposes for each clause its instantiations. The architecture is then combined with an efficient ground solver and, starting with zero knowledge, iteratively trained on a large corpus of mathematical problems. We show that the system is capable of solving many problems by such educated guessing, finding proofs for 32.12% of the training set. The final trained system solves 19.74% of the unseen test data on its own. We also observe that the trained system finds solutions that the iProver and CVC5 systems did not find. (c) 2024 The Authors. Published by Elsevier Ltd.

Druh

J_imp - Článek v periodiku v databázi Web of Science

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í

2025

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 periodika

Journal of Symbolic Computation

ISSN

0747-7171

e-ISSN

1095-855X

Svazek periodika

128

Číslo periodika v rámci svazku

102375

Stát vydavatele periodika

GB - Spojené království Velké Británie a Severního Irska

Počet stran výsledku

21

Strana od-do

—

Kód UT WoS článku

001312643500001

EID výsledku v databázi Scopus

2-s2.0-85203064613