Conference Proceedings
Online Machine Learning Techniques for Coq: A Comparison
L Zhang, L Blaauwbroek, B Piotrowski, P Černỳ, C Kaliszyk, J Urban
Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics | SPRINGER INTERNATIONAL PUBLISHING AG | Published : 2021
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 ..
View full abstractGrants
Awarded by Horizon 2020 Framework Programme
Funding Acknowledgements
This work was supported by the ERC grant no. 714034 SMART, by the European Regional Development Fund under the project AI&Reasoning (reg. no. CZ.02.1.01/0.0/0.0/15 003/0000466), and by the Ministry of Education, Youth and Sports within the dedicated program ERC CZ under the project POSTMAN no. LL1902.