Learning Proof Transformations and Its Applications in Interactive Theorem Proving

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F23%3A00372165" target="_blank" >RIV/68407700:21730/23:00372165 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1007/978-3-031-43369-6_13" target="_blank" >https://doi.org/10.1007/978-3-031-43369-6_13</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-031-43369-6_13" target="_blank" >10.1007/978-3-031-43369-6_13</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Learning Proof Transformations and Its Applications in Interactive Theorem Proving

Popis výsledku v původním jazyce

Interactive theorem provers are today increasingly used to certify mathematical theories. To formally prove a theorem, reasoning procedures called tactics are invoked successively on the proof states starting with the initial theorem statement, transforming them into subsequent intermediate goals, and ultimately discharging all proof obligations. In this work, we develop and experimentally evaluate approaches that predict the most likely tactics that will achieve particular desired transformations of proof states. First, we design several characterizations to efficiently capture the semantics of the proof transformations. Then we use them to create large datasets on which we train state-of-the-art random forests and language models. The trained models are evaluated experimentally, and we show that our best model is able to guess the right tactic for a given proof transformation in 74% of the cases. Finally, we use the trained methods in two applications: proof shortening and tactic suggesting. To the best of our knowledge, this is the first time that tactic synthesis is trained on proof transformations and assists interactive theorem proving in these ways.

Název v anglickém jazyce

Learning Proof Transformations and Its Applications in Interactive Theorem Proving

Popis výsledku anglicky

Interactive theorem provers are today increasingly used to certify mathematical theories. To formally prove a theorem, reasoning procedures called tactics are invoked successively on the proof states starting with the initial theorem statement, transforming them into subsequent intermediate goals, and ultimately discharging all proof obligations. In this work, we develop and experimentally evaluate approaches that predict the most likely tactics that will achieve particular desired transformations of proof states. First, we design several characterizations to efficiently capture the semantics of the proof transformations. Then we use them to create large datasets on which we train state-of-the-art random forests and language models. The trained models are evaluated experimentally, and we show that our best model is able to guess the right tactic for a given proof transformation in 74% of the cases. Finally, we use the trained methods in two applications: proof shortening and tactic suggesting. To the best of our knowledge, this is the first time that tactic synthesis is trained on proof transformations and assists interactive theorem proving in these ways.

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í

2023

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

Frontiers of Combining Systems

ISBN

978-3-031-43368-9

ISSN

2945-9133

e-ISSN

1611-3349

Počet stran výsledku

19

Strana od-do

236-254

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Praha

Datum konání akce

20. 9. 2023

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

WRD - Celosvětová akce

Kód UT WoS článku

001156327100013