Online Machine Learning Techniques for Coq: A Comparison
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Online Machine Learning Techniques for Coq: A Comparison
Original language description
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.
Czech name
—
Czech description
—
Classification
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)
Result continuities
Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2021
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Intelligent Computer Mathematics
ISBN
978-3-030-81096-2
ISSN
0302-9743
e-ISSN
1611-3349
Number of pages
17
Pages from-to
67-83
Publisher name
Springer
Place of publication
Cham
Event location
Timisoara
Event date
Jul 26, 2021
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000707054900005