The ASTactic model in 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}
}
Please visit https://github.com/princeton-vl/CoqGym for details.
Inference Providers
NEW
This model is not currently available via any of the supported Inference Providers.
The model cannot be deployed to the HF Inference API:
The model has no library tag.