Invariant neural architecture for learning term synthesis in instantiation proving

Result code in 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>

Result on the web

<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>

Result language

angličtina

Original language name

Invariant neural architecture for learning term synthesis in instantiation proving

Original language description

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.

Czech name

—

Czech description

—

Type

J_imp - Article in a specialist periodical, which is included in the Web of Science database

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

2025

Confidentiality

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

Name of the periodical

Journal of Symbolic Computation

ISSN

0747-7171

e-ISSN

1095-855X

Volume of the periodical

128

Issue of the periodical within the volume

102375

Country of publishing house

GB - UNITED KINGDOM

Number of pages

21

Pages from-to

—

UT code for WoS article

001312643500001

EID of the result in the Scopus database

2-s2.0-85203064613