CoqGym

Stream: Machine Learning for Theorem Proving

[Jason Rute]

This is specifically to talk about CoqGym and its API for use in other projects. It is not so much about ASTactic (which is talked about in this thread here).

[Jason Rute]

@Brando Miranda told me (on GitHub) that he finds the CoqGym API very usable. I'd like to understand the API more. @Brando Miranda is the best documentation just the README on Github? Do you have any initial thoughts and commentary on this Gym?

[Jason Rute]

Also, how easy would it be to implement a Tactic-Toe style AI in Coq Gym? That would be a great baseline. Here is what I mean:

• Don't use neural networks. Instead, for the embeddings used a fixed hand-coded embedding using the techniques from the recent TacticToe for Coq paper. (These shouldn't be too hard to code and would be quite useful to anyone else using CoqGym.)
• For tactic selection, use k-nearest neighbors using the prerecorded CoqGym information.
• For premise selection, also use k-nearest neighbors (with both the goal and the premise to select).
• Look again at the CoqGym paper for some of the finer details, such as which tactics to use, how to use them, and how to fill in the non-theorem tactic arguments.

[Jason Rute]

Since it is not trained with neural networks or reinforcement learning, it should be much easier to reproduce.

[Stanislas Polu]

Hi everyone! I'm looking for references to theorems that were proved by CoqGym/ASTactic and whose proof was contributed back to the Coq libraries? Git commits or email threads are all welcome. Thanks thanks!

[Jason Rute]

@Stanislas Polu Coq now has their own Coq Zulip and they also have a stream for #Machine Learning and Automation. It would probably be best to ask there as well. (Also, there are other similar projects such as ProverBot9001 and Tactician. You may want to ask about those as well if I understand your motivation.)

[Stanislas Polu]

Thanks @Jason Rute will do so :+1: