Online Machine Learning Techniques for Coq: A Comparison

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F21%3A00354419" target="_blank" >RIV/68407700:21730/21:00354419 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1007/978-3-030-81097-9_5" target="_blank" >https://doi.org/10.1007/978-3-030-81097-9_5</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-81097-9_5" target="_blank" >10.1007/978-3-030-81097-9_5</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Online Machine Learning Techniques for Coq: A Comparison

Popis výsledku v původním jazyce

We present a comparison of several online machine learning techniques for tactical learning and proving in the Coq proof assistant. This work builds on top of Tactician, a plugin for Coq that learns from proofs written by the user to synthesize new proofs. Learning happens in an online manner, meaning that Tactician’s machine learning model is updated immediately every time the user performs a step in an interactive proof. This has important advantages compared to the more studied offline learning systems: (1) it provides the user with a seamless, interactive experience with Tactician and, (2) it takes advantage of locality of proof similarity, which means that proofs similar to the current proof are likely to be found close by. We implement two online methods, namely approximate k-nearest neighbors based on locality sensitive hashing forests and random decision forests. Additionally, we conduct experiments with gradient boosted trees in an offline setting using XGBoost. We compare the relative performance of Tactician using these three learning methods on Coq’s standard library.

Název v anglickém jazyce

Online Machine Learning Techniques for Coq: A Comparison

Popis výsledku anglicky

We present a comparison of several online machine learning techniques for tactical learning and proving in the Coq proof assistant. This work builds on top of Tactician, a plugin for Coq that learns from proofs written by the user to synthesize new proofs. Learning happens in an online manner, meaning that Tactician’s machine learning model is updated immediately every time the user performs a step in an interactive proof. This has important advantages compared to the more studied offline learning systems: (1) it provides the user with a seamless, interactive experience with Tactician and, (2) it takes advantage of locality of proof similarity, which means that proofs similar to the current proof are likely to be found close by. We implement two online methods, namely approximate k-nearest neighbors based on locality sensitive hashing forests and random decision forests. Additionally, we conduct experiments with gradient boosted trees in an offline setting using XGBoost. We compare the relative performance of Tactician using these three learning methods on Coq’s standard library.

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í

2021

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-030-81096-2

ISSN

0302-9743

e-ISSN

1611-3349

Počet stran výsledku

17

Strana od-do

67-83

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Timisoara

Datum konání akce

26. 7. 2021

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

WRD - Celosvětová akce

Kód UT WoS článku

000707054900005