Online Machine Learning Techniques for Coq: A Comparison

Understand

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.