Efficient Neural Clause-Selection Reinforcement

Result code in IS VaVaI

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

Result on the web

<a href="https://doi.org/10.1007/978-3-031-99984-0_22" target="_blank" >https://doi.org/10.1007/978-3-031-99984-0_22</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-031-99984-0_22" target="_blank" >10.1007/978-3-031-99984-0_22</a>

Result language

angličtina

Original language name

Efficient Neural Clause-Selection Reinforcement

Original language description

Clause selection is arguably the most important choice point in saturation-based theorem proving. Framing it as a reinforcement learning (RL) task is a way to challenge the human-designed heuristics of state-of-the-art provers and to instead automatically evolve—just from prover experiences—their potentially optimal replacement. In this work, we present a neural network architecture for scoring clauses for clause selection that is powerful yet efficient to evaluate. Following RL principles to make design decisions, we integrate the network into the Vampire theorem prover and train it from successful proof attempts. An experiment on the diverse TPTP benchmark finds the neurally guided prover improves over a baseline strategy, from which it initially learns—in terms of the number of in-training-unseen problems solved under a practically relevant, short CPU instruction limit—by 20%.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

<a href="/en/project/GA24-12759S" target="_blank" >GA24-12759S: Malleable Theorem Proving Architectures</a><br>

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ů

Article name in the collection

Automated Deduction – CADE 30: 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings

ISBN

978-3-031-99983-3

ISSN

0302-9743

e-ISSN

—

Number of pages

20

Pages from-to

403-422

Publisher name

Springer

Place of publication

Cham

Event location

Stuttgart

Event date

Jul 28, 2025

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—