3
$\begingroup$

I'm trying to produce Coq and Lean code using a custom GPT but I want GPT to try running its proof scripts (and revising them if they fail) before suggesting them to me (via gpt actions).

Right now, LeanDojo seems to be the closest to being able to do this, but it can only attempt to prove theorems from .lean files hosted on Github. (Also, integrating it with a new Github repository is very slow.) Is there a better API for Lean?

Is there anything similar for Coq? I feel like Coq is easier to get running from scratch (no need for workspaces, coqtop seems flexible) so maybe there's an easy way to set up a Coq API?

Any suggestions welcome!

(Answers for Isabelle or other proof assistants are also welcome.)

Improve this question
$\endgroup$
7
  • $\begingroup$ The answer to your question really depends on how you are using GPT. For example, it is very different if you are using GPT as a code suggestion tool where it starts to autocomplete based on the code so far in the file, versus using it to suggest the next tactic based on the current proof state and then incorporate that tactic suggestion tool in a proof search. There are existing systems which do either approach. $\endgroup$
    – Jason Rute
    Commented Jan 6 at 9:59
  • $\begingroup$ Also it makes a big difference if this is for research (so you need a benchmark to know how good stuff is) or for practice (so you need a practical interface for users). $\endgroup$
    – Jason Rute
    Commented Jan 6 at 10:03
  • $\begingroup$ I'm not using it as a copilot. I want GPT-4 to try to generate a Coq or Lean proof, or even Coq or Lean file, given text input. It can already do that, but any complicated proof tends to be a laborious process of telling GPT-4 where its code failed, hence the desire for proper integration (so we don't need a human in that loop). $\endgroup$
    – Rand00
    Commented Jan 8 at 3:10
  • 1
    $\begingroup$ It is for research, but it's exploratory. I don't have a benchmark that I'm trying to beat, nor am I introducing a new one. The ability to depend on installed packages and other files is useful (particularly the first) but not strictly necessary. $\endgroup$
    – Rand00
    Commented Jan 8 at 3:11
  • $\begingroup$ There seems to be a discussion about this exact topic on the Coq Discourse site (possibly by the OP, but it is unclear): coq.discourse.group/t/… $\endgroup$
    – Jason Rute
    Commented Jan 11 at 2:56

2 Answers 2

Reset to default
4
$\begingroup$

The Lean REPL provides a simple JSON-based read-eval-print loop for Lean, which is probably sufficient for your needs (you'll need to write a simple wrapper around it so GPT can communicate).

Improve this answer
$\endgroup$
3
$\begingroup$

This isn't really a great question for this site. The problem is that your vision is quite vague, and answering it would require a back-and-forth which this site is not set up for. I recommend you continue the conversation on the Lean Zulip, or one of the Coq forums (and also be more specific). But nonetheless, to get you started, I'll list some resources.

I want GPT to try running its proof scripts (and revising them if they fail) before suggesting them to me

I think the challenge is what "running its proof scripts" means. Are you talking about GPT generating a complete file's worth of code including relevant imports, theorem statements, and proofs? Do you want a pre-built web API where you can pass it a file's worth of text, and get back a response?

While I don't know of any existing web APIs, you could easily make your own. If you just want to run a file, you could make an API which takes in the text, puts it into a file and runs Lean, Coq, or Isabelle on that file like so:

# lean4
lean myfile.lean

# coq
coqc myfile.v

And I'm sure Isabelle has something similar. Then you would take the output and manipulate it into whatever form is best for you and send it back. (But be really careful to sandbox this. Lean code is a full programming language and code can delete files or run command line tools. Don't blindly run code.)

If instead you want something more REPL like, you could use Lean REPL as in Scott's answer, or SerAPI for Coq. (Or the Coq REPL.) The challenge however with a REPL is that you have to know how to divide up the code into individual commands. Of course GPT might be smart enough for this. If you want to run tactics one at a time, REPLs could be good for this.

Both Coq and Lean have a language server, and in my humble opinion, this is the future of LM-code interaction. Language servers not only report errors, but also let you investigate proof states, definitions, and other properties of the code. They facilitate a rich back-and-forth experience. How to most productively hook up a language server and a language model is still an open engineering problem.

It also isn't clear what you even want out of such as system. Is this for research? If so, you likely want to benchmark the system by measuring how well it does on a set of theorems. Or is this for end users? In which case, maybe you want more of a copilot like experience where GPT tries out the code locally in the current file (using the author's existing definitions and imports). This would likely require good editor integration and possibly use the language server or the tactic framework.

Also, many works not only use language models to generate a complete proof, but one tactic at a time, and then use a symbolic tree search to find a proof. This would be a more complicated interface.

Here is a quick list of some existing works you could draw inspiration from (in no particular order):

  • Draft-Sketch-Prove uses Minerva+Codex to generate a natural language proof and convert it into a formal proof sketch in Isabelle which is completed with SledgeHammer.
  • Baldur uses Minerva in Isabelle and makes corrections based on error messages.
  • Segredo uses GPT-4 in Lean to try one tactic at a time and do a proof search. (It is usable by end users.)
  • Lean Copilot uses finetuned transformer models to make tactic suggests and find proofs. The proofs are found with a tree search which checks if a tactic is valid after running it. It is based on ReProver from LeanDojo. (It is usable by end users.)
  • CoqPilot is a vscode plugin for Coq which uses GPT-4 to suggest code inside your file. (It is usable by end users.)
  • The Llemma model paper has experiments where they use the language model to generate proofs with Draft-Sketch-Prove style and Lean
  • LeanDojo comes with ChatGPT plugin to interface with ChatGPT as you mentioned. (I think this is usable by end users.)
  • Copra uses GPT-4 to suggest next steps which are used in a tree search.

All of these works probably set up the interface with Lean/Coq/Isabelle differently. I don't think there is yet a one-size-fits-all approach, and it heavily depends on what you want to do.

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ Where did you find the code/instructions for using Sagredo? All I can find is a YouTube video, not any code or website. $\endgroup$
    – Rand00
    Commented Jan 8 at 3:36
  • 1
    $\begingroup$ @Rand00 It looks like it never got added to a Lean’s mathlib, but you can find it in a branch: github.com/leanprover-community/mathlib4/tree/sagredo-widget/… $\endgroup$
    – Jason Rute
    Commented Jan 8 at 11:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.