Cautious Specialization of Strategy Schedules (Extended Abstract)

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21230%2F24%3A00380249" target="_blank" >RIV/68407700:21230/24:00380249 - isvavai.cz</a>

Nalezeny alternativní kódy

RIV/68407700:21730/24:00380249

Výsledek na webu

<a href="https://ceur-ws.org/Vol-3717/short2.pdf" target="_blank" >https://ceur-ws.org/Vol-3717/short2.pdf</a>

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Cautious Specialization of Strategy Schedules (Extended Abstract)

Popis výsledku v původním jazyce

Combining theorem proving strategies into schedules is a well-known recipe for improving prover performance, as a well-chosen set of complementary strategies in practice covers many more problems within a predetermined time budget than a single strategy could. A strategy schedule can be a monolithic sequence, but may also consist of multiple schedule branches, intended to be selected based on certain problem’s features and thus to specialize in solving the corresponding problem classes. When allowing schedule branching, there is an intuitive trade-off between covering the known (training) problems quickly, by splitting them into many classes, and the generalization of the obtained branching schedule, i.e., its ability to solve previously unseen (test) problems. In this paper, we attempt to shed more light on this trade-off. Starting off with a large set of proving strategies of the automatic theorem prover Vampire evaluated on the first-order part of the TPTP library, we report on two preliminary experiments with building branching schedules while keeping track of how well they generalize to test problems. We hope to attract more attention to the exciting topic of schedule construction by this work-in-progress report.

Název v anglickém jazyce

Cautious Specialization of Strategy Schedules (Extended Abstract)

Popis výsledku anglicky

Combining theorem proving strategies into schedules is a well-known recipe for improving prover performance, as a well-chosen set of complementary strategies in practice covers many more problems within a predetermined time budget than a single strategy could. A strategy schedule can be a monolithic sequence, but may also consist of multiple schedule branches, intended to be selected based on certain problem’s features and thus to specialize in solving the corresponding problem classes. When allowing schedule branching, there is an intuitive trade-off between covering the known (training) problems quickly, by splitting them into many classes, and the generalization of the obtained branching schedule, i.e., its ability to solve previously unseen (test) problems. In this paper, we attempt to shed more light on this trade-off. Starting off with a large set of proving strategies of the automatic theorem prover Vampire evaluated on the first-order part of the TPTP library, we report on two preliminary experiments with building branching schedules while keeping track of how well they generalize to test problems. We hope to attract more attention to the exciting topic of schedule construction by this work-in-progress report.

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í

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

Practical Aspects of Automated Reasoning and Satisfiability Checking and Symbolic Computation Workshop 2024

ISBN

—

ISSN

1613-0073

e-ISSN

1613-0073

Počet stran výsledku

9

Strana od-do

28-36

Název nakladatele

CEUR Workshop Proceedings

Místo vydání

Aachen

Místo konání akce

Nancy

Datum konání akce

1. 7. 2024

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

WRD - Celosvětová akce

Kód UT WoS článku

—