Towards Finding Longer Proofs

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

Result on the web

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

Result language

angličtina

Original language name

Towards Finding Longer Proofs

Original language description

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.

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/EF15_003%2F0000466" target="_blank" >EF15_003/0000466: Artificial Intelligence and Reasoning</a><br>

Continuities

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

Publication year

2021

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

ISBN

978-3-030-86058-5

ISSN

0302-9743

e-ISSN

1611-3349

Number of pages

20

Pages from-to

167-186

Publisher name

Springer

Place of publication

Cham

Event location

Birmingham

Event date

Sep 6, 2021

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

000711656700010