The Coq mailing list

[Lasse Blaauwbroek <lasse AT blaauwbroek.eu>]

Hi Adam,

Creating a battle-tested AI/ML/ATP/SMT system for Coq is not an easy task. There are several reasons for this.

(1) Coq is one of the more complex ITP's out there, which brings a lot of engineering challenges with it. Solving all of those, such that there are no corner-cases and performance issues left, is often not feasible in an academic setting.

(2) If one wants to use external solvers, neural networks and advanced external machine learning tool-kits, the infrastructure that needs to be set up for this becomes increasingly complex, and hence more complex to setup and manage by the end-user. Putting this on top of the already complex engineering issues that Coq users are tackling is usually too much of a burden. Setting up machine learning systems in such a way that they pose no burden to the end-user is a time-consuming (and non-academic) task.

(3) We actually face the opposite problem you face. While you are unable to find stable/usable systems to work with, we are (largely) unable to find end-users that are willing to give serious and recurring feedback on our systems while using it on complex developments. Part of the reason for this is the standard chicken/egg problem. Additionally, it seems that Coq users seem more unwilling to install/use plugins than users of other ITP's. For example, the Isabelle hammer is quite popular with it's users. One possible reason for this is that it is quite a barrier to install a plugin from Opam (especially when a user normally uses a version of Coq packaged by a unix distro or windows binary).

With Tactician, we are making a serious effort to put a machine-learning-based prover in the hands of end-users. Although I do not claim that the system is without any problems, we are certainly willing to work with people to resolve such problems. Similarly, at the moment we cannot guarantee that the system will be strong enough to be usable for your particular development (we are still in beta, and still working hard on improving Tactician's solving strength). However, any feedback is more than welcome.

We are working hard on integrating more complex learning technologies (neural architectures, ensemble learning, boosted trees, ...) than the current version of Tactician offers. Eventually, the goal is to create a platform that enables AI/ML researchers to easily access data from Coq's internals, build a predictive model and deploy it to end-users.  As stated above, making such technology fully seamless is hard work. Enthusiasm and buy-in from Coq's user base will certainly help us there.

We also have a version of Tactician that transmits usage telemetry. We have previously used this in introductory type theory courses to gather automated feedback. The introductory nature limits our ability to judge the system in an advanced setting, though. If you have access to a body of students that are, as you say, "willing to step outside the lines", we would love to gather telemetry from them, too.

Regards,
Lasse

On 8/21/21 9:16 PM, Adam Chlipala wrote:

On 8/18/21 11:24 PM, Talia Ringer wrote:

I'm thinking a bit ahead to the grad seminar I'll teach in the spring (starting in January) which I think I'll have complete freedom over. I really want to do a proof automation course, where one day every week is a deep dive on a single paper, and the other is hacking on the paper artifact. I was thinking this outline:

[...]

8, 9: ATP for ITP

10, 11: neural networks for proofs

I'm really curious on the community's thoughts regarding stable/usable artifacts in these categories.  My collaborators and I actually haven't found any!

There have been research papers on SMT bridges for Coq (heck, I think I built the first one myself as a student), but we find that they all fall over when used for significant program verification.  That is, we hit blocking issues (performance scaling or otherwise) that make the maintainers say "yeah, that would be really hard to fix."

The neural-networks angle has been a popular point of discussion since deep learning became hot, but I don't think I've yet come across someone using such a tool who isn't also one of its primary authors.

      You can carefully curate experiences using rickety tools in a
      course, but it would be nice if students could expect stepping
      outside the lines to go well.