Cautious Specialization of Strategy Schedules (Extended Abstract)

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

Alternative codes found

RIV/68407700:21730/24:00380249

Result on the web

<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

—

Result language

angličtina

Original language name

Cautious Specialization of Strategy Schedules (Extended Abstract)

Original language description

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.

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/GA24-12759S" target="_blank" >GA24-12759S: Malleable Theorem Proving Architectures</a><br>

Continuities

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

Publication year

2024

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

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

ISBN

—

ISSN

1613-0073

e-ISSN

1613-0073

Number of pages

9

Pages from-to

28-36

Publisher name

CEUR Workshop Proceedings

Place of publication

Aachen

Event location

Nancy

Event date

Jul 1, 2024

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—