Jason Rute (Jan 16 2024 at 02:03): Jason Rute (Jan 16 2024 at 02:03):I'm continuing part of the discussion of this topic in a new thread:
Robert Rand said:
Following up from the StackExchange discussion (https://proofassistants.stackexchange.com/questions/2660/coq-lean-endpoint-for-gpt-actions):
Can I use (part of) this to integrate GPT-4 with Coq, in such a way that GPT-4 can execute Coq code? Has anyone built a custom GPT action on top of this?
I don't think this question is specific to the Tactician API for Graph2Tac. As I mention in my answer to the PA SX question, there are many approaches to communicating between LLMs and Coq (or Lean/Isabelle/etc) and it is worth having a broader discussion on them and how they might be implemented in practice.
Bas Spitters (Jan 17 2024 at 12:38):Incidentally, I found this tutorial at POPL quite enlightening:
https://popl24.sigplan.org/details/POPL-2024-tutorialfest/6/Machine-Learning-Meets-Program-Synthesis
I believe it has been recorded. The presenter mentioned the slides would be on his website.
Last updated: Oct 13 2024 at 01:02 UTC