< Back to main site

Comparison to other projects

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, we've 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