Both
the ASTactic (ICML 2019)
and TacTok (OOPSLA 2020)
projects run on the CoqGym dataset, making it easy to compare the
effectiveness of our work to theirs. Below, weve graphed the
number of proofs solved by each tool on various CoqGym benchmarks
in the testing dataset, when trained on the projects in the
training dataset.
The Proverbot9001 numbers above were run using our own infrastructure, not the extracted CoqGym data. As a result, we were only able to run on projects that supported Coq 8.10, 8.11, or 8.12; you can see a full list of the CoqGym testing projects, and notes on our ability to run on them, here