Efficient Neural Clause-Selection Reinforcement

Kód výsledku v 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>

Výsledek na webu

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

Jazyk výsledku

angličtina

Název v původním jazyce

Efficient Neural Clause-Selection Reinforcement

Popis výsledku v původním jazyce

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

Název v anglickém jazyce

Efficient Neural Clause-Selection Reinforcement

Popis výsledku anglicky

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

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

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

Projekt

<a href="/cs/project/GA24-12759S" target="_blank" >GA24-12759S: Tvárné architektury pro automatické dokazování vět</a><br>

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 statě ve sborníku

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

—

Počet stran výsledku

20

Strana od-do

403-422

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Stuttgart

Datum konání akce

28. 7. 2025

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—