Stream: Coq users

Topic: GPT-3 -> Coq


view this post on Zulip Gurkenglas (Jun 19 2020 at 20:08):

I'm trying to make OpenAI's new text generator complete Coq proofs. First I tried to make it generate lines to feed into coqtop, but I ran into problems sending and receiving single lines at a time between process inputs and outputs. So now I'm trying to compile the whole file each time GPT-3 adds a line, but coqc throws an error when the last proof isn't complete. Is there a way to make coqc accept any proof that coqide would? Should I be using another API?

view this post on Zulip Karl Palmskog (Jun 19 2020 at 20:19):

if you're looking for a machine-friendly API to use for interacting with Coq, take a look at https://github.com/ejgallego/coq-serapi --- several applications in machine learning and similar are listed

view this post on Zulip Karl Palmskog (Jun 19 2020 at 20:22):

by the way, doesn't GPT-3 still need Coq-specific training? If so, since Coq code is close-to-impossible to parse ad-hoc externally, you may want to take a look at our machine-readable Coq dataset generated via SerAPI: https://github.com/EngineeringSoftware/math-comp-corpus

view this post on Zulip Gurkenglas (Jun 19 2020 at 21:28):

As I tried to opam install coq-serapi, I got [ERROR] The sources of the following couldn't be obtained, aborting: - ppx_import.1.4

view this post on Zulip Karl Palmskog (Jun 19 2020 at 21:31):

sounds like a downloading problem, you may want to just try again

view this post on Zulip Emilio Jesús Gallego Arias (Jun 19 2020 at 21:31):

@Gurkenglas are you using Opam 2?

view this post on Zulip Karl Palmskog (Jun 19 2020 at 21:32):

ah right, I thought 1.4 sounded old, indeed the latest version is 1.7.1 if one has the proper opam version (2.0.5 or later)


Last updated: Jan 29 2023 at 05:03 UTC