Towards Finding Longer Proofs

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F21%3A00354752" target="_blank" >RIV/68407700:21730/21:00354752 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1007/978-3-030-86059-2_10" target="_blank" >https://doi.org/10.1007/978-3-030-86059-2_10</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-86059-2_10" target="_blank" >10.1007/978-3-030-86059-2_10</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Towards Finding Longer Proofs

Popis výsledku v původním jazyce

We present a reinforcement learning (RL) based guidance system for automated theorem proving geared towards Finding Longer Proofs (FLoP). Unlike most learning based approaches, we focus on generalising from very little training data and achieving near complete confidence. We use several simple, structured datasets with very long proofs to show that FLoP can successfully generalise a single training proof to a large class of related problems. On these benchmarks, FLoP is competitive with strong theorem provers despite using very limited search, due to its ability to solve problems that are prohibitively long for other systems.

Název v anglickém jazyce

Towards Finding Longer Proofs

Popis výsledku anglicky

We present a reinforcement learning (RL) based guidance system for automated theorem proving geared towards Finding Longer Proofs (FLoP). Unlike most learning based approaches, we focus on generalising from very little training data and achieving near complete confidence. We use several simple, structured datasets with very long proofs to show that FLoP can successfully generalise a single training proof to a large class of related problems. On these benchmarks, FLoP is competitive with strong theorem provers despite using very limited search, due to its ability to solve problems that are prohibitively long for other systems.

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/EF15_003%2F0000466" target="_blank" >EF15_003/0000466: Umělá inteligence a uvažování</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2021

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 Reasoning with Analytic Tableaux and Related Methods

ISBN

978-3-030-86058-5

ISSN

0302-9743

e-ISSN

1611-3349

Počet stran výsledku

20

Strana od-do

167-186

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Birmingham

Datum konání akce

6. 9. 2021

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

WRD - Celosvětová akce

Kód UT WoS článku

000711656700010