experiments with copilot

Stream: Machine Learning for Theorem Proving

[Alex Kontorovich]

I'm not sure how many (if any) of you are experimenting with turning GitHub copilot on while you work in VS Code (splurging $10/month), but I've had it suggest some very useful things (and also many, many completely useless things). In offline discussions, it was suggested that if others were also messing around with copilot, and if we all logged and collated said interactions (that is, collecting both what copilot suggested, as well as what was eventually written there, given the proof/goal state, etc), that might make for a very interesting dataset for future experimentation/training... Just a thought...?

[Kaiyu Yang]

I've been using Copilot for about half a year and also find it really helpful. I don't explicitly adapt the way I code to help Copilot (e.g., writing detailed comments), but in many cases, it seems to be able to guess what I want to code. This experience is mostly for Python, but sometimes it can also produce sensible autocompletions for Lean.

[Siddhartha Gadgil]

I use copilot regularly with Lean 4 and it is helpful. It generates proofs and sometimes theorems as well correctly about half the time and nonsense the rest of the time (which I don't accept).

By the way, it is free for teachers and for sudents, so covers most of us.

[Junyan Xu]

if others were also messing around with copilot, and if we all logged and collated said interactions (that is, collecting both what copilot suggested, as well as what was eventually written there, given the proof/goal state, etc), that might make for a very interesting dataset for future experimentation/training...

Christian Szegedy retweeted this which says:

Introducing Rift 2.0 - the agentic IDE for working with your personal AI software engineer.

https://github.com/morph-labs/rift [works with VSCode]

With Rift 2.0, you can now:

• Request, review, and iterate on codebase-wide, multi-file edits
• Conversationally iterate on code edits which are streamed directly into your editor window
• Generate an entire workspace, or a module based on other parts of your codebase

You can now define your own agents that can run in your IDE and:

• Provide a conversational Git interface
• Run tools like typecheckers and static analyzers in the background and implement fixes based on their output
• Automated code review in your IDE with context from GitHub

Rift will soon support locally recording and storing training data from your coding sessions so that you can build your own team of truly personalized AI software engineers.

[Junyan Xu]

Two crowd-sourcing data collection tools are gpt4all-datalake and Open-Assistant, but these are not code specific and I'm not aware of a tool to log Copilot interaction data ...

[Jason Rute]

Rift is by @Jesse Michael Han

[Bolton Bailey]

#7307 copilot managed to produce a 5-line totally correct proof of this theorem on the first try. It was longer than it had to be, but still impressive.