Learning to Prove Theorems via Interacting with Proof Assistants
Authors: Kaiyu Yang, Jia Deng
ICML 2019 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experiments show that ASTactic trained on Coq Gym can generate effective tactics and can be used to prove new theorems not previously provable by automated methods. We evaluate ASTactic on the task of fully-automated theorem proving in Coq, using the 13,137 testing theorems in Coq Gym. |
| Researcher Affiliation | Academia | Kaiyu Yang 1 Jia Deng 1 Department of Computer Science, Princeton University. |
| Pseudocode | No | The paper describes the architecture and processes of ASTactic but does not contain structured pseudocode or algorithm blocks with formal labels. |
| Open Source Code | Yes | Code is available at https://github.com/ princeton-vl/Coq Gym. |
| Open Datasets | Yes | We construct Coq Gym, a large-scale dataset and learning environment containing 71K human-written proofs from 123 projects developed with the Coq proof assistant. |
| Dataset Splits | Yes | These projects are split into a training set, a validation set, and a test set. ... There are 43,844 proofs for training, 13,875 proofs for validation and 13,137 proofs for testing. |
| Hardware Specification | Yes | The training goes for 5 epochs, which takes a few days on a single Ge Force GTX 1080 GPU. We run all testing experiments on machines with 16GB RAM and two Intel Xeon Silver 4114 CPU Cores. |
| Software Dependencies | No | The paper mentions software like Coq and Ser API, but does not provide specific version numbers for these or other relevant software components (e.g., Python, deep learning frameworks/libraries) used in the experiments. |
| Experiment Setup | Yes | We use 256-dimensional vectors for all embeddings in ASTactic... We train the model using RMSProp ... with a learning rate of 3 x 10^-5 and weight decay of 10^-6. The training goes for 5 epochs... During testing, our system performs beam search with a beam width of 20 to generate the top 20 tactics at each proof step. And we set a depth limit of 50 during DFS. |