The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

I remember watching you live prove during DeepSpec 2017. It's quite possible that the example was manufactured since it was educational, but one thing that stood out was that in trying to extend program-specific custom tactics to handle changes, you first made changes within individual proofs, then figured out how to bubble those changes out into your tactic going forward.

LLMs I think could be very helpful for figuring out those changes within individual proofs, but as of now, it is likely that a human would still need to observe that such repetition is occurring, then figure out how to generalize it inside of the custom tactic implementation. Though, I'm not certain of that; I think it would be a really interesting exercise for you to find someone with Copilot access, pick a project you're working on, and just hack with Copilot on for a long time, and see what it's good at and what it struggles with for your own style (with an extremely open mind, remembering that it ought to get better over time).

I'd be interested in a more systematic exploration of this for different proving styles if you're interested; I think it’s important to know as we head toward a future where these language models for programming and proving become much more widespread.

Talia

On Sat, Aug 21, 2021, 7:06 PM Adam Chlipala <adamc AT csail.mit.edu> wrote:

On 8/21/21 7:18 PM, Talia Ringer wrote:
> Language models do really well with enough context, and this is often
> neglected when people try them out, so they often abandon them early.
> I recently tried Copilot with Joe Cutler in the middle of CompCert to
> see what it does, and I think even a naive large language model like
> Codex with no semantic understanding at all does really well at
> synthesizing proofs inside of a large project specifically when you
> are in a repetitive file with many similar, small lemmas and slight
> variations between them. The syntax often captures many of those
> variations, and the LLM picks up on them easily. We will post a
> YouTube video on this Monday.
That sounds really interesting, though I'm wondering about the
comparison point of an Ltac script written by someone very familiar with
the code base, which would be used for all lemmas.  That's kind of a way
of making a "style" first-class.