Zulip Chat Archive

Stream: Machine Learning for Theorem Proving

Topic: CoqGym


view this post on Zulip Jason Rute (May 10 2020 at 12:35):

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).

view this post on Zulip Jason Rute (May 10 2020 at 12:37):

@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?

view this post on Zulip Jason Rute (May 10 2020 at 12:43):

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.

view this post on Zulip Jason Rute (May 10 2020 at 12:44):

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

view this post on Zulip Stanislas Polu (Aug 17 2020 at 12:44):

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!

view this post on Zulip Jason Rute (Aug 17 2020 at 16:38):

@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.)

view this post on Zulip Stanislas Polu (Aug 17 2020 at 17:10):

Thanks @Jason Rute will do so :+1:


Last updated: May 09 2021 at 22:13 UTC