Machine Learning of Coq Proof Guidance: First Experiments

TL;DR

This paper presents initial experiments on applying machine learning to predict proof dependencies in Coq formalizations, demonstrating promising results comparable to other large-theory corpora.

Contribution

It introduces a methodology for learning proof dependencies from Coq formalizations and compares various machine learning methods on a substantial dataset.

Findings

Best method predicts 75% of dependencies within 100 guesses

Comparable performance to other large-theory corpora

First experimental results on Coq proof dependency learning

Abstract

We report the results of the first experiments with learning proof dependencies from the formalizations done with the Coq system. We explain the process of obtaining the dependencies from the Coq proofs, the characterization of formulas that is used for the learning, and the evaluation method. Various machine learning methods are compared on a dataset of 5021 toplevel Coq proofs coming from the CoRN repository. The best resulting method covers on average 75% of the needed proof dependencies among the first 100 predictions, which is a comparable performance of such initial experiments on other large-theory corpora.