Learning Conjecturing from Scratch

Kód výsledku v IS VaVaI

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

Výsledek na webu

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

DOI - Digital Object Identifier

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

Jazyk výsledku

angličtina

Název v původním jazyce

Learning Conjecturing from Scratch

Popis výsledku v původním jazyce

We develop a self-learning approach for conjecturing of induction predicates on a dataset of 14,005 problems derived from the OEIS. These problems are hard for today’s SMT and ATP systems because they require a combination of inductive and arithmetical reasoning. Starting from scratch, our approach consists of a feedback loop that iterates between (i) training a neural translator to learn the correspondence between the problems solved so far and the induction predicates useful for them, (ii) using the trained neural system to generate many new induction predicates for the problems, (iii) fast runs of the Z3 prover attempting to prove the problems using the generated predicates, (iv) using heuristics such as predicate size and solution speed on the proved problems to choose the best predicates for the next iteration of training. The algorithm discovers on its own many interesting induction predicates, ultimately solving 3,590 problems, compared to 835 problems solved by CVC5, Vampire or Z3 in 60 s.

Název v anglickém jazyce

Learning Conjecturing from Scratch

Popis výsledku anglicky

We develop a self-learning approach for conjecturing of induction predicates on a dataset of 14,005 problems derived from the OEIS. These problems are hard for today’s SMT and ATP systems because they require a combination of inductive and arithmetical reasoning. Starting from scratch, our approach consists of a feedback loop that iterates between (i) training a neural translator to learn the correspondence between the problems solved so far and the induction predicates useful for them, (ii) using the trained neural system to generate many new induction predicates for the problems, (iii) fast runs of the Z3 prover attempting to prove the problems using the generated predicates, (iv) using heuristics such as predicate size and solution speed on the proved problems to choose the best predicates for the next iteration of training. The algorithm discovers on its own many interesting induction predicates, ultimately solving 3,590 problems, compared to 835 problems solved by CVC5, Vampire or Z3 in 60 s.

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

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

23

Strana od-do

423-445

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

—