Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban
Intelligent Computer Mathematics – 14th International Conference, CICM 2021, pp. 67-83, 2021.
pdf 
doi:10.1007/978-3-030-81097-9_5
Abstract
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.
BibTex
@inproceedings{lzlbbppcckju-cicm21, author = {Liao Zhang and Lasse Blaauwbroek and Bartosz Piotrowski and Prokop Cern{\'{y}} and Cezary Kaliszyk and Josef Urban}, editor = {Fairouz Kamareddine and Claudio Sacerdoti Coen}, title = {Online Machine Learning Techniques for {C}oq: {A} Comparison}, booktitle = {Intelligent Computer Mathematics - 14th International Conference, {CICM} 2021}, series = {LNCS}, volume = {12833}, pages = {67--83}, publisher = {Springer}, year = {2021}, url = {https://doi.org/10.1007/978-3-030-81097-9\_5}, doi = {10.1007/978-3-030-81097-9\_5},}