Machine-Learned Premise Selection for Lean

Kód výsledku v IS VaVaI

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

Výsledek na webu

<a href="https://doi.org/10.1007/978-3-031-43513-3_10" target="_blank" >https://doi.org/10.1007/978-3-031-43513-3_10</a>

DOI - Digital Object Identifier

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

Jazyk výsledku

angličtina

Název v původním jazyce

Machine-Learned Premise Selection for Lean

Popis výsledku v původním jazyce

We introduce a machine-learning-based tool for the Lean proof assistant that suggests relevant premises for theorems being proved by a user. The design principles for the tool are (1) tight integration with the proof assistant, (2) ease of use and installation, (3) a lightweight and fast approach. For this purpose, we designed a custom version of the random forest model, trained in an online fashion. It is implemented directly in Lean, which was possible thanks to the rich and efficient metaprogramming features of Lean 4. The random forest is trained on data extracted from mathlib – Lean’s mathematics library. We experiment with various options for producing training features and labels. The advice from a trained model is accessible to the user via the tactic which can be called in an editor while constructing a proof interactively.

Název v anglickém jazyce

Machine-Learned Premise Selection for Lean

Popis výsledku anglicky

We introduce a machine-learning-based tool for the Lean proof assistant that suggests relevant premises for theorems being proved by a user. The design principles for the tool are (1) tight integration with the proof assistant, (2) ease of use and installation, (3) a lightweight and fast approach. For this purpose, we designed a custom version of the random forest model, trained in an online fashion. It is implemented directly in Lean, which was possible thanks to the rich and efficient metaprogramming features of Lean 4. The random forest is trained on data extracted from mathlib – Lean’s mathematics library. We experiment with various options for producing training features and labels. The advice from a trained model is accessible to the user via the tactic which can be called in an editor while constructing a proof interactively.

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

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

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

Automated Reasoning with Analytic Tableaux and Related Methods

ISBN

978-3-031-43512-6

ISSN

0302-9743

e-ISSN

1611-3349

Počet stran výsledku

12

Strana od-do

175-186

Název nakladatele

Springer, Cham

Místo vydání

—

Místo konání akce

Praha

Datum konání akce

18. 9. 2023

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

WRD - Celosvětová akce

Kód UT WoS článku

001162233100010