flâneur

princeton-vl/CoqGym: A Learning Environment for Theorem Proving with the Coq proof assistant

github.com · 1,946 words · saved by 1 readers

Learning to Prove Theorems via Interacting with Proof Assistants Kaiyu Yang and Jia Deng International Conference on Machine Learning (ICML) 2019 For potential bugs, please open an issue. For any other questions, please ask in Discussions. We recommend using CoqGym in Docker, as CoqGym has many dependencies and is nontrivial to set up correctly. If Docker is not an option, below are steps to obtain the CoqGym dataset and build the interaction environment natively: Note: Coq, SerAPI, CoqHammer, and the Coq projects in coq_projects directory are independent software projects with their own code repositories, but please follow the instructions above to build the specific versions we need. We include the code for extracting CoqGym from Coq source code. However, it is not guaranteed to reproduce exactly the same data. The timeout and other miscellaneous errors during the data extraction may be machine-dependent. For example, a faster machine is likely to have fewer timeout errors and thus c

Code for the paper: Learning to Prove Theorems via Interacting with Proof Assistants Kaiyu Yang and Jia Deng International Conference on Machine Learning (ICML) 2019 @inproceedings{yang2019coqgym, title={Learning to Prove Theorems via Interacting with Proof Assistants}, author={Yang, Kaiyu and Deng, Jia}, booktitle={International Conference on Machine Learning (ICML)}, year={2019} } For potential bugs, please open an issue. For any other questions, please ask in Discussions. Table of Contents Installing CoqGym 1.1 Dependencies 1.2 Building Coq, SerAPI, CoqHammer, and the Coq…

saved by

related reading