Learning Guided Automated Reasoning: A Brief Survey

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F24%3A00584859" target="_blank" >RIV/67985807:_____/24:00584859 - isvavai.cz</a>

Nalezeny alternativní kódy

RIV/68407700:21730/24:00380966

Výsledek na webu

<a href="https://doi.org/10.1007/978-3-031-61716-4_4" target="_blank" >https://doi.org/10.1007/978-3-031-61716-4_4</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-031-61716-4_4" target="_blank" >10.1007/978-3-031-61716-4_4</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Learning Guided Automated Reasoning: A Brief Survey

Popis výsledku v původním jazyce

Automated theorem provers and formal proof assistants are general reasoning systems that are in theory capable of proving arbitrarily hard theorems, thus solving arbitrary problems reducible to mathematics and logical reasoning. In practice, such systems however face large combinatorial explosion, and therefore include many heuristics and choice points that considerably influence their performance. This is an opportunity for trained machine learning predictors, which can guide the work of such reasoning systems. Conversely, deductive search supported by the notion of logically valid proof allows one to train machine learning systems on large reasoning corpora. Such bodies of proof are usually correct by construction and when combined with more and more precise trained guidance they can be boostrapped into very large corpora, with increasingly long reasoning chains and possibly novel proof ideas. In this paper we provide an overview of several automated reasoning and theorem proving domains and the learning and AI methods that have been so far developed for them. These include premise selection, proof guidance in several settings, AI systems and feedback loops iterating between reasoning and learning, and symbolic classification problems.

Název v anglickém jazyce

Learning Guided Automated Reasoning: A Brief Survey

Popis výsledku anglicky

Automated theorem provers and formal proof assistants are general reasoning systems that are in theory capable of proving arbitrarily hard theorems, thus solving arbitrary problems reducible to mathematics and logical reasoning. In practice, such systems however face large combinatorial explosion, and therefore include many heuristics and choice points that considerably influence their performance. This is an opportunity for trained machine learning predictors, which can guide the work of such reasoning systems. Conversely, deductive search supported by the notion of logically valid proof allows one to train machine learning systems on large reasoning corpora. Such bodies of proof are usually correct by construction and when combined with more and more precise trained guidance they can be boostrapped into very large corpora, with increasingly long reasoning chains and possibly novel proof ideas. In this paper we provide an overview of several automated reasoning and theorem proving domains and the learning and AI methods that have been so far developed for them. These include premise selection, proof guidance in several settings, AI systems and feedback loops iterating between reasoning and learning, and symbolic classification problems.

Druh

C - Kapitola v odborné knize

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

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2024

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 knihy nebo sborníku

Logics and Type Systems in Theory and Practice. Essays in Honor of the 60th Birthday of Herman Geuvers

ISBN

978-3-031-61715-7

Počet stran výsledku

30

Strana od-do

54-83

Počet stran knihy

273

Název nakladatele

Springer

Místo vydání

Cham

Kód UT WoS kapitoly

001283291600005