Solving Hard Mizar Problems with Instantiation and Strategy Invention

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F24%3A00379755" target="_blank" >RIV/68407700:21730/24:00379755 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1007/978-3-031-66997-2_18" target="_blank" >https://doi.org/10.1007/978-3-031-66997-2_18</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-031-66997-2_18" target="_blank" >10.1007/978-3-031-66997-2_18</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Solving Hard Mizar Problems with Instantiation and Strategy Invention

Popis výsledku v původním jazyce

In this work, we prove over 3000 previously ATP-unproved Mizar/MPTP problems by using several ATP and AI methods, raising the number of ATP-solved Mizar problems from 75% to above 80%. First, we start to experiment with the cvc5 SMT solver which uses several instantiation-based heuristics that differ from the superposition-based systems, that were previously applied to Mizar, and add many new solutions. Then we use automated strategy invention to develop cvc5 strategies that largely improve cvc5's performance on the hard problems. In particular, the best invented strategy solves over 14% more problems than the best previously available cvc5 strategy. We also show that different clausification methods have a high impact on such instantiation-based methods, again producing many new solutions. In total, the methods solve 3,021 (21.3%) of the 14,163 previously unsolved hard Mizar problems. This is a new milestone over the Mizar large-theory benchmark and a large strengthening of the hammer methods for Mizar.

Název v anglickém jazyce

Solving Hard Mizar Problems with Instantiation and Strategy Invention

Popis výsledku anglicky

In this work, we prove over 3000 previously ATP-unproved Mizar/MPTP problems by using several ATP and AI methods, raising the number of ATP-solved Mizar problems from 75% to above 80%. First, we start to experiment with the cvc5 SMT solver which uses several instantiation-based heuristics that differ from the superposition-based systems, that were previously applied to Mizar, and add many new solutions. Then we use automated strategy invention to develop cvc5 strategies that largely improve cvc5's performance on the hard problems. In particular, the best invented strategy solves over 14% more problems than the best previously available cvc5 strategy. We also show that different clausification methods have a high impact on such instantiation-based methods, again producing many new solutions. In total, the methods solve 3,021 (21.3%) of the 14,163 previously unsolved hard Mizar problems. This is a new milestone over the Mizar large-theory benchmark and a large strengthening of the hammer methods for Mizar.

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

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

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

Intelligent Computer Mathematics

ISBN

978-3-031-66996-5

ISSN

0302-9743

e-ISSN

1611-3349

Počet stran výsledku

19

Strana od-do

315-333

Název nakladatele

Springer, Cham

Místo vydání

—

Místo konání akce

Montréal, Québec

Datum konání akce

5. 8. 2024

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

WRD - Celosvětová akce

Kód UT WoS článku

001292779800018